|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Unit test for expr2c |
| 4 | +
|
| 5 | +Author: Diffblue |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#include <ansi-c/expr2c.h> |
| 10 | +#include <testing-utils/use_catch.h> |
| 11 | +#include <util/arith_tools.h> |
| 12 | +#include <util/bitvector_expr.h> |
| 13 | +#include <util/bitvector_types.h> |
| 14 | +#include <util/config.h> |
| 15 | +#include <util/namespace.h> |
| 16 | +#include <util/symbol_table.h> |
| 17 | + |
| 18 | +TEST_CASE("rol_2_c_conversion_unsigned", "[core][ansi-c][expr2c]") |
| 19 | +{ |
| 20 | + auto lhs = from_integer(31, unsignedbv_typet(32)); |
| 21 | + auto rhs = from_integer(3, unsignedbv_typet(32)); |
| 22 | + auto rol = shift_exprt(lhs, ID_rol, rhs); |
| 23 | + CHECK( |
| 24 | + expr2c(rol, namespacet{symbol_tablet{}}) == |
| 25 | + "31 << 3 % 50 | 31 >> 50 - 3 % 50"); |
| 26 | +} |
| 27 | + |
| 28 | +TEST_CASE( |
| 29 | + "rol_2_c_conversion_signed", |
| 30 | + "[core][ansi-c][expr2c][convert_with_precedence]") |
| 31 | +{ |
| 32 | + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; |
| 33 | + config.ansi_c.set_arch_spec_i386(); |
| 34 | + auto lhs = from_integer(31, signedbv_typet(8)); |
| 35 | + auto rhs = from_integer(3, signedbv_typet(8)); |
| 36 | + auto rol = shift_exprt(lhs, ID_rol, rhs); |
| 37 | + CHECK( |
| 38 | + expr2c(rol, namespacet{symbol_tablet{}}) == |
| 39 | + "(unsigned char)31 << 3 % 8 | (unsigned char)31 >> 8 - 3 % 8"); |
| 40 | +} |
| 41 | + |
| 42 | +TEST_CASE( |
| 43 | + "ror_2_c_conversion_unsigned", |
| 44 | + "[core][ansi-c][expr2c][convert_with_precedence]") |
| 45 | +{ |
| 46 | + auto lhs = from_integer(31, unsignedbv_typet(32)); |
| 47 | + auto rhs = from_integer(3, unsignedbv_typet(32)); |
| 48 | + auto ror = shift_exprt(lhs, ID_ror, rhs); |
| 49 | + CHECK( |
| 50 | + expr2c(ror, namespacet{symbol_tablet{}}) == |
| 51 | + "31 >> 3 % 50 | 31 << 50 - 3 % 50"); |
| 52 | +} |
| 53 | + |
| 54 | +TEST_CASE( |
| 55 | + "ror_2_c_conversion_signed", |
| 56 | + "[core][ansi-c][expr2c][convert_with_precedence]") |
| 57 | +{ |
| 58 | + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; |
| 59 | + config.ansi_c.set_arch_spec_i386(); |
| 60 | + auto lhs = from_integer(31, integer_bitvector_typet(ID_signedbv, 32)); |
| 61 | + auto rhs = from_integer(3, integer_bitvector_typet(ID_signedbv, 32)); |
| 62 | + auto ror = shift_exprt(lhs, ID_ror, rhs); |
| 63 | + CHECK( |
| 64 | + expr2c(ror, namespacet{symbol_tablet{}}) == |
| 65 | + "(unsigned int)31 >> 3 % 50 | (unsigned int)31 << 50 - 3 % 50"); |
| 66 | +} |
0 commit comments