@@ -107,9 +107,13 @@ SCENARIO("subtract interval domain",
107
107
108
108
SCENARIO (" Subtracting unsigned integers" )
109
109
{
110
+ auto get_value = [](int x) {
111
+ return from_integer (x, signedbv_typet (32 ));
112
+ };
113
+
110
114
WHEN (" Subtracting two constant intervals" ) {
111
- auto lhs = constant_interval_exprt (constant_exprt ( " 1010 " , unsignedbv_typet ( 32 ) ));
112
- auto rhs = constant_interval_exprt (constant_exprt ( " 0011 " , unsignedbv_typet ( 32 ) ));
115
+ auto lhs = constant_interval_exprt (get_value ( 10 ));
116
+ auto rhs = constant_interval_exprt (get_value ( 3 ));
113
117
THEN (" it should work" ) {
114
118
auto result = lhs.minus (rhs);
115
119
REQUIRE (result.is_single_value_interval ());
@@ -121,8 +125,8 @@ SCENARIO("Subtracting unsigned integers")
121
125
122
126
WHEN (" Subtracting zero from something" )
123
127
{
124
- auto lhs = constant_interval_exprt (constant_exprt ( " 1010 " , unsignedbv_typet ( 32 ) ));
125
- auto rhs = constant_interval_exprt (constant_exprt ( " 0 " , unsignedbv_typet ( 32 ) ));
128
+ auto lhs = constant_interval_exprt (get_value ( 10 ));
129
+ auto rhs = constant_interval_exprt (get_value ( 0 ));
126
130
127
131
THEN (" it should not give a completely crazy result" )
128
132
{
@@ -136,9 +140,8 @@ SCENARIO("Subtracting unsigned integers")
136
140
137
141
WHEN (" Subtracting an non-constant interval containing zero" )
138
142
{
139
- auto lhs = constant_interval_exprt (constant_exprt (" 1010" , unsignedbv_typet (32 )));
140
- auto rhs = constant_interval_exprt (constant_exprt (" 0" , unsignedbv_typet (32 )),
141
- constant_exprt (" 1" , unsignedbv_typet (32 )));
143
+ auto lhs = constant_interval_exprt (get_value (10 ));
144
+ auto rhs = constant_interval_exprt (get_value (0 ), get_value (1 ));
142
145
THEN (" it should not give a completely crazy result" )
143
146
{
144
147
auto result = lhs.minus (rhs);
0 commit comments