File tree Expand file tree Collapse file tree 3 files changed +35
-3
lines changed
regression/cbmc/enum_is_in_range Expand file tree Collapse file tree 3 files changed +35
-3
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+
3
+ enum my_enum
4
+ {
5
+ first ,
6
+ second ,
7
+ third ,
8
+ fourth ,
9
+ fifth
10
+ };
11
+
12
+ int main ()
13
+ {
14
+ enum my_enum ev1 ;
15
+ enum my_enum ev2 ;
16
+ ev1 = first ;
17
+ ev2 = fifth ;
18
+ assert (__CPROVER_enum_is_in_range (ev1 , ev2 ));
19
+ return 0 ;
20
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ enum_test12.c
3
+
4
+ ^EXIT=6$
5
+ ^SIGNAL=0$
6
+ ^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range expects 1 argument, 2 were provided$
7
+ --
8
+ ^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$
9
+ ^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$
10
+ ^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
11
+ --
12
+ This test the type checking of argument for __CPROVER_num_is_in_range
Original file line number Diff line number Diff line change @@ -2847,7 +2847,7 @@ exprt c_typecheck_baset::do_special_functions(
2847
2847
if (expr.arguments ().size () != 1 )
2848
2848
{
2849
2849
error ().source_location = expr.source_location ();
2850
- error () << identifier << " expects one argument, "
2850
+ error () << identifier << " expects 1 argument, "
2851
2851
<< expr.arguments ().size () << " were provided" << eom;
2852
2852
throw 0 ;
2853
2853
}
@@ -2866,8 +2866,8 @@ exprt c_typecheck_baset::do_special_functions(
2866
2866
std::vector<exprt> disjuncts;
2867
2867
for (const auto &enum_value : enum_values)
2868
2868
{
2869
- const constant_exprt val{enum_value.get_value (), *c_enum_tag_type};
2870
- disjuncts.push_back (equal_exprt (arg1, val));
2869
+ constant_exprt val{enum_value.get_value (), *c_enum_tag_type};
2870
+ disjuncts.push_back (equal_exprt (arg1, std::move ( val) ));
2871
2871
}
2872
2872
2873
2873
return disjunction (disjuncts);
You can’t perform that action at this time.
0 commit comments