Skip to content

Commit 5949dc9

Browse files
tautschnigilvn
andcommitted
Do not generate enum-value checks for function call left-hand sides
We already disabled these checks for assignment left-hand sides, but need to do the same for function calls. Else we'd be asserting validity before the value has been assigned. Fixes: #6586 Co-authored-by: Ilia Levin <[email protected]>
1 parent 1e0fa76 commit 5949dc9

File tree

2 files changed

+16
-3
lines changed

2 files changed

+16
-3
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
no_duplicate.c
3+
--enum-range-check
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--

src/analyses/goto_check_c.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -444,8 +444,7 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
444444
return;
445445

446446
const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
447-
symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
448-
const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
447+
const c_enum_typet &c_enum_type = ns.follow_tag(c_enum_tag_type);
449448

450449
const c_enum_typet::memberst enum_values = c_enum_type.members();
451450

@@ -2141,7 +2140,13 @@ void goto_check_ct::goto_check(
21412140
}
21422141
else if(i.is_function_call())
21432142
{
2144-
check(i.call_lhs());
2143+
// Reset the no_enum_check with the flag reset for exception
2144+
// safety
2145+
{
2146+
flag_resett resetter(i);
2147+
resetter.set_flag(no_enum_check, true, "no_enum_check");
2148+
check(i.call_lhs());
2149+
}
21452150
check(i.call_function());
21462151

21472152
for(const auto &arg : i.call_arguments())

0 commit comments

Comments
 (0)