[SV-COMP'18 7/19] Ensure that local declarations do not introduce spurious dead warnings #1996
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
smowton and
thk123
as code owners
| state.level2.current_names.end()) | ||
| state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0); | ||
| state.level2.current_names.insert( | ||
| std::make_pair(l1_identifier, std::make_pair(ssa, 0))); |
There was a problem hiding this comment.
Nitpick: might as well emplace, rather than make pair then insert
| ^SIGNAL=0$ | ||
| ^VERIFICATION SUCCESSFUL$ | ||
| -- | ||
| ^warning: ignoring |
There was a problem hiding this comment.
Add an extra no-match line for the particular warning you were seeing?
| { | ||
| if(enable_pointer_check) | ||
| { | ||
| assert(i.code.operands().size()==1); |
| // reset the dead marker | ||
| goto_programt::targett t=new_code.add_instruction(ASSIGN); | ||
| exprt address_of_expr=address_of_exprt(variable); | ||
| exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); |
There was a problem hiding this comment.
If "dead_object" is a magic string, is it already defined somewhere else? (A quick search of the code says no - it'd be nice to pull it out rather than introduce another duplication of it)
There was a problem hiding this comment.
Ignorant of this code, is this somehow the point where the variable that's declared goes out of scope? If you do pull out the "dead_object" string, it'd be great to document there what this variable is.
| exprt rhs= | ||
| if_exprt( | ||
| equal_exprt(lhs, address_of_expr), | ||
| null_pointer_exprt(to_pointer_type(address_of_expr.type())), |
There was a problem hiding this comment.
might be clearer to use lhs.type() (since either equal or typecast and therefore equal?)
| @@ -1666,6 +1666,34 @@ void goto_checkt::goto_check( | |||
| } | |||
| } | |||
| } | |||
| else if(i.is_decl()) | |||
| { | |||
| if(enable_pointer_check) | |||
There was a problem hiding this comment.
I am unfamiliar with this code so non-blocking (I don't understand why dead statements need this instrumentation), but some documentation of why a deceleration statement needs to be instrumented when enable_pointer_check is on would be appreciated
|
This problem has been solved by #3980. |
No description provided.