Skip to content

Commit cd9a7b7

Browse files
committed
Fixes based on PR to tidy up code and improve error messages
Fixes based on PR feedback to improve code clarity, use of correct lookup function, and improve error output.
1 parent 2085c91 commit cd9a7b7

File tree

3 files changed

+9
-14
lines changed

3 files changed

+9
-14
lines changed

regression/cbmc/enum_is_in_range/enum_test10.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ enum_test10.c
33

44
^EXIT=6$
55
^SIGNAL=0$
6-
^file enum_test10.c line \d+ function main: __enum_is_in_range expects enum argument type$
6+
^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum argument type$
77
--
88
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$
99
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$

regression/cbmc/enum_is_in_range/enum_test3.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ int main()
1515
enum my_enum ev2;
1616
ev1 = first;
1717
ev2 = fifth;
18-
while(!(ev1 == ev2))
18+
while(ev1 != ev2)
1919
{
2020
ev1++;
2121
assert(__CPROVER_enum_is_in_range(ev1));

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2847,12 +2847,9 @@ exprt c_typecheck_baset::do_special_functions(
28472847
if(expr.arguments().size() != 1)
28482848
{
28492849
error().source_location = expr.source_location();
2850-
error() << "__enum_is_in_range expects one argument" << eom;
2851-
std::ostringstream error_message;
2852-
error_message << expr.source_location().as_string() << ": "
2853-
<< "__enum_is_in_range expects one argument, "
2854-
<< expr.arguments().size() << " were provided";
2855-
throw invalid_source_file_exceptiont{error_message.str()};
2850+
error() << identifier << " expects one argument, " <<
2851+
expr.arguments().size() << " were provided" << eom;
2852+
throw 0;
28562853
}
28572854
// Replace expr with giant boolean that checks all the values
28582855
// of the enumeration as disjunction
@@ -2863,8 +2860,7 @@ exprt c_typecheck_baset::do_special_functions(
28632860
auto c_enum_tag_type =
28642861
type_try_dynamic_cast<c_enum_tag_typet>(arg1.type()))
28652862
{
2866-
symbolt enum_type = this->lookup(c_enum_tag_type->get_identifier());
2867-
const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
2863+
const c_enum_typet &c_enum_type = follow_tag(*c_enum_tag_type);
28682864
const c_enum_typet::memberst enum_values = c_enum_type.members();
28692865

28702866
std::vector<exprt> disjuncts;
@@ -2879,10 +2875,9 @@ exprt c_typecheck_baset::do_special_functions(
28792875
else
28802876
{
28812877
// Can't enum range check a non-enum
2882-
std::ostringstream error_message;
2883-
error_message << expr.source_location().as_string() << ": "
2884-
<< "__enum_is_in_range expects enum argument type";
2885-
throw invalid_source_file_exceptiont{error_message.str()};
2878+
error().source_location = expr.source_location();
2879+
error() << identifier << " expects enum argument type" << eom;
2880+
throw 0;
28862881
}
28872882
}
28882883
else if(

0 commit comments

Comments
 (0)