@@ -21,11 +21,16 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
2121 constant_interval_exprt nine =
2222 constant_interval_exprt (from_integer (9 , unsigned_int));
2323
24+ constant_interval_exprt five_to_nine (
25+ from_integer (5 , unsigned_int), from_integer (9 , unsigned_int));
26+
2427 THEN (" Bitwise or should yield bitwise representation of 13" )
2528 {
2629 REQUIRE (
2730 constant_interval_exprt::bitwise_or (five, nine) ==
2831 constant_interval_exprt (from_integer (13 , unsigned_int)));
32+
33+ REQUIRE (constant_interval_exprt::bitwise_or (five_to_nine, nine).is_top ());
2934 }
3035
3136 THEN (" Bitwise and should yield bitwise representation of 1" )
@@ -36,13 +41,19 @@ SCENARIO("bitwise interval domain", "[core][analyses][interval][bitwise]")
3641 REQUIRE (
3742 (five & nine) ==
3843 constant_interval_exprt (from_integer (1 , unsigned_int)));
44+
45+ REQUIRE (
46+ constant_interval_exprt::bitwise_and (five_to_nine, nine).is_top ());
3947 }
4048
4149 THEN (" Bitwise xor should yield bitwise representation of 12" )
4250 {
4351 REQUIRE (
4452 constant_interval_exprt::bitwise_xor (five, nine) ==
4553 constant_interval_exprt (from_integer (12 , unsigned_int)));
54+
55+ REQUIRE (
56+ constant_interval_exprt::bitwise_xor (five_to_nine, nine).is_top ());
4657 }
4758 }
4859}
0 commit comments