Skip to content

Commit 7597f90

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 8c0644d commit 7597f90

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
@@ -517,8 +517,7 @@ void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
517517
return;
518518

519519
const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type(expr.type());
520-
symbolt enum_type = ns.lookup(c_enum_tag_type.get_identifier());
521-
const c_enum_typet &c_enum_type = to_c_enum_type(enum_type.type);
520+
const c_enum_typet &c_enum_type = ns.follow_tag(c_enum_tag_type);
522521

523522
const c_enum_typet::memberst enum_values = c_enum_type.members();
524523

@@ -2148,7 +2147,13 @@ void goto_check_ct::goto_check(
21482147
}
21492148
else if(i.is_function_call())
21502149
{
2151-
check(i.call_lhs());
2150+
// Disable enum range checks for left-hand sides as their values are yet
2151+
// to be set (by this function call).
2152+
{
2153+
flag_overridet resetter(i.source_location());
2154+
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2155+
check(i.call_lhs());
2156+
}
21522157
check(i.call_function());
21532158

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

0 commit comments

Comments
 (0)