File tree Expand file tree Collapse file tree 1 file changed +10
-16
lines changed
Expand file tree Collapse file tree 1 file changed +10
-16
lines changed Original file line number Diff line number Diff line change 1515#define V_ (X ) (bvrep2integer(X.c_str(), 32 , true ))
1616#define CEV (X ) (from_integer(mp_integer(X), signedbv_typet(32 )))
1717
18- SCENARIO (" shift interval domain" , " [core][analyses][interval][shift]" )
18+ TEST_CASE (" shift interval domain" , " [core][analyses][interval][shift]" )
1919{
20- GIVEN (" Two simple signed intervals" )
20+ SECTION (" Left shift" )
21+ {
22+ const constant_interval_exprt four_to_eight (CEV (4 ), CEV (8 ));
23+ const constant_interval_exprt one (CEV (1 ));
24+ REQUIRE (
25+ constant_interval_exprt::left_shift (four_to_eight, one) ==
26+ constant_interval_exprt (CEV (8 ), CEV (16 )));
27+ }
28+ SECTION (" Right shift" )
2129 {
22- symbol_tablet symbol_table;
23- namespacet ns (symbol_table);
24-
25- WHEN (" Something" )
26- {
27- THEN (" Something else" )
28- {
29- REQUIRE (
30- constant_interval_exprt::left_shift (
31- constant_interval_exprt (CEV (4 ), CEV (8 )),
32- constant_interval_exprt (CEV (1 ))) ==
33- constant_interval_exprt (CEV (8 ), CEV (16 )));
34- }
35- }
3630 }
3731}
You can’t perform that action at this time.
0 commit comments