|
| 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 % 32 | 31 >> 32 - 3 % 32"); |
| 26 | +} |
| 27 | + |
| 28 | +TEST_CASE("rol_2_c_conversion_signed", "[core][ansi-c][expr2c]") |
| 29 | +{ |
| 30 | + // The config lines are necessary since when we do casting from signed |
| 31 | + // to unsigned in the rol/ror bit twiddling we need to output a |
| 32 | + // suitable cast type (e.g. "unsigned int" and not |
| 33 | + // "unsigned __CPROVER_bitvector"). |
| 34 | + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; |
| 35 | + config.ansi_c.set_arch_spec_i386(); |
| 36 | + auto lhs = from_integer(31, signedbv_typet(8)); |
| 37 | + auto rhs = from_integer(3, signedbv_typet(8)); |
| 38 | + auto rol = shift_exprt(lhs, ID_rol, rhs); |
| 39 | + CHECK( |
| 40 | + expr2c(rol, namespacet{symbol_tablet{}}) == |
| 41 | + "(unsigned char)31 << 3 % 8 | (unsigned char)31 >> 8 - 3 % 8"); |
| 42 | +} |
| 43 | + |
| 44 | +TEST_CASE("ror_2_c_conversion_unsigned", "[core][ansi-c][expr2c]") |
| 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 % 32 | 31 << 32 - 3 % 32"); |
| 52 | +} |
| 53 | + |
| 54 | +TEST_CASE("ror_2_c_conversion_signed", "[core][ansi-c][expr2c]") |
| 55 | +{ |
| 56 | + // The config lines are necessary since when we do casting from signed |
| 57 | + // to unsigned in the rol/ror bit twiddling we need to output a |
| 58 | + // suitable cast type (e.g. "unsigned int" and not |
| 59 | + // "unsigned __CPROVER_bitvector"). |
| 60 | + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; |
| 61 | + config.ansi_c.set_arch_spec_i386(); |
| 62 | + auto lhs = from_integer(31, integer_bitvector_typet(ID_signedbv, 32)); |
| 63 | + auto rhs = from_integer(3, integer_bitvector_typet(ID_signedbv, 32)); |
| 64 | + auto ror = shift_exprt(lhs, ID_ror, rhs); |
| 65 | + CHECK( |
| 66 | + expr2c(ror, namespacet{symbol_tablet{}}) == |
| 67 | + "(unsigned int)31 >> 3 % 32 | (unsigned int)31 << 32 - 3 % 32"); |
| 68 | +} |
0 commit comments