File tree Expand file tree Collapse file tree 2 files changed +23
-16
lines changed
Expand file tree Collapse file tree 2 files changed +23
-16
lines changed Original file line number Diff line number Diff line change @@ -44,21 +44,5 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
4444 constant_interval_exprt::bitwise_xor (five, nine) ==
4545 constant_interval_exprt (from_integer (12 , unsigned_int)));
4646 }
47-
48- THEN (" Left shift on the 5 should produce 10" )
49- {
50- REQUIRE (
51- constant_interval_exprt::left_shift (
52- five, constant_interval_exprt (from_integer (1 , unsigned_int))) ==
53- constant_interval_exprt (from_integer (10 , unsigned_int)));
54- }
55-
56- THEN (" Right shift on the 5 should produce 2" )
57- {
58- REQUIRE (
59- constant_interval_exprt::right_shift (
60- five, constant_interval_exprt (from_integer (1 , unsigned_int))) ==
61- constant_interval_exprt (from_integer (2 , unsigned_int)));
62- }
6347 }
6448}
Original file line number Diff line number Diff line change @@ -19,13 +19,36 @@ TEST_CASE("shift interval domain", "[core][analyses][interval][shift]")
1919{
2020 SECTION (" Left shift" )
2121 {
22+ REQUIRE (
23+ constant_interval_exprt::left_shift (
24+ constant_interval_exprt (CEV (5 )), constant_interval_exprt (CEV (1 ))) ==
25+ constant_interval_exprt (CEV (10 )));
26+
2227 const constant_interval_exprt four_to_eight (CEV (4 ), CEV (8 ));
2328 const constant_interval_exprt one (CEV (1 ));
2429 REQUIRE (
2530 constant_interval_exprt::left_shift (four_to_eight, one) ==
2631 constant_interval_exprt (CEV (8 ), CEV (16 )));
32+
33+ const constant_interval_exprt negative_one (CEV (-1 ));
34+ REQUIRE (constant_interval_exprt::left_shift (four_to_eight, negative_one)
35+ .is_top ());
2736 }
2837 SECTION (" Right shift" )
2938 {
39+ REQUIRE (
40+ constant_interval_exprt::right_shift (
41+ constant_interval_exprt (CEV (5 )), constant_interval_exprt (CEV (1 ))) ==
42+ constant_interval_exprt (CEV (2 )));
43+
44+ const constant_interval_exprt four_to_eight (CEV (4 ), CEV (8 ));
45+ const constant_interval_exprt one (CEV (1 ));
46+ REQUIRE (
47+ constant_interval_exprt::right_shift (four_to_eight, one) ==
48+ constant_interval_exprt (CEV (2 ), CEV (4 )));
49+
50+ const constant_interval_exprt negative_one (CEV (-1 ));
51+ REQUIRE (constant_interval_exprt::right_shift (four_to_eight, negative_one)
52+ .is_top ());
3053 }
3154}
You can’t perform that action at this time.
0 commit comments