@@ -54,7 +54,6 @@ class goto_check_ct
5454 message_handlert &_message_handler)
5555 : ns(_ns), local_bitvector_analysis(nullptr ), log(_message_handler)
5656 {
57- no_enum_check = false ;
5857 enable_bounds_check = _options.get_bool_option (" bounds-check" );
5958 enable_pointer_check = _options.get_bool_option (" pointer-check" );
6059 enable_memory_leak_check = _options.get_bool_option (" memory-leak-check" );
@@ -103,8 +102,6 @@ class goto_check_ct
103102 goto_programt::const_targett current_target;
104103 messaget log;
105104
106- bool no_enum_check;
107-
108105 using guardt = std::function<exprt(exprt)>;
109106 const guardt identity = [](exprt expr) { return expr; };
110107
@@ -440,7 +437,7 @@ void goto_check_ct::div_by_zero_check(
440437
441438void goto_check_ct::enum_range_check (const exprt &expr, const guardt &guard)
442439{
443- if (!enable_enum_range_check || no_enum_check )
440+ if (!enable_enum_range_check)
444441 return ;
445442
446443 const c_enum_tag_typet &c_enum_tag_type = to_c_enum_tag_type (expr.type ());
@@ -2110,11 +2107,11 @@ void goto_check_ct::goto_check(
21102107 const exprt &assign_lhs = i.assign_lhs ();
21112108 const exprt &assign_rhs = i.assign_rhs ();
21122109
2113- // Reset the no_enum_check with the flag reset for exception
2114- // safety
2110+ // Disable enum range checks for left-hand sides as their values are yet
2111+ // to be set (by this assignment).
21152112 {
21162113 flag_resett resetter (i);
2117- resetter.set_flag (no_enum_check, true , " no_enum_check " );
2114+ resetter.disable_flag (enable_enum_range_check, " enum_range_check " );
21182115 check (assign_lhs);
21192116 }
21202117
0 commit comments