Skip to content

Commit b8585bf

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: diffblue#6586, diffblue#6451 Co-authored-by: Ilia Levin <[email protected]>
1 parent b634e11 commit b8585bf

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

@@ -2125,7 +2124,13 @@ void goto_check_ct::goto_check(
21252124
}
21262125
else if(i.is_function_call())
21272126
{
2128-
check(i.call_lhs());
2127+
// Reset the no_enum_check with the flag reset for exception
2128+
// safety
2129+
{
2130+
flag_resett resetter(i);
2131+
resetter.set_flag(no_enum_check, true, "no_enum_check");
2132+
check(i.call_lhs());
2133+
}
21292134
check(i.call_function());
21302135

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

0 commit comments

Comments
 (0)