Convert assert calls to INVARIANTs #4
Conversation
|
|
||
| // identify the file name, inlined functions aren't properly | ||
| // accounted for | ||
| goto_programt::const_targett end_function= | ||
| --gf_it->second.body.instructions.end(); | ||
| assert(end_function->is_end_function()); | ||
| INVARIANT(end_function->is_end_function(), |
| file_name=end_function->source_location.get_file(); | ||
| assert(!file_name.empty()); | ||
| INVARIANT(!file_name.empty(), |
| @@ -34,7 +34,8 @@ Author: Daniel Kroening, [email protected] | |||
| /// \return An smt2_dect::solvert giving the solver to use. | |||
| smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const | |||
| { | |||
| assert(options.get_bool_option("smt2")); | |||
| // we shouldn't get here if this option isn't set | |||
| PRECONDITION(options.get_bool_option("smt2")); | |||
There was a problem hiding this comment.
Hm this is not really a precondition of the function. I think in general it is fine to use INVARIANT even as the first statement in a function. But in the rest of the cbmc code base there are lots of PRECONDITION statements too that IMO should be INVARIANTSs instead.
There was a problem hiding this comment.
Can you explain what you mean by "not a precondition"? While the value in here isn't really needed for anything in the function, it's certainly something that should be true when we enter this function right?
There was a problem hiding this comment.
Hm I'm probably interpreting preconditions to narrowly. I basically took the view that a precondition is something that absolutely needs to hold when calling a function for it not to crash or produce garbage output. Like a function that unconditionally dereferences a pointer would have ptr != nullptr as a precondition, or a function that converts a string representing a binary number to an integer needs to get a string that contains only characters '0' and '1' (if it does not have built-in checks for this).
But currently in the codebase we have several preconditions that are more of the kind "here's something that happens to hold when we enter this function as it's currently used but it's not necessarily related to the function itself". Technically the functions could be used in different ways in the future and for those uses the preconditions might not apply anymore.
But the present case above seems somewhat like a corner case so I don't mind if we leave it as a PRECONDITION.
There was a problem hiding this comment.
Yeah, but we should probably dig up what the intended meaning is and get everyone to agree to it.
This global name map will be used to check what generation is currently available for each level1 name, and shared across all states. This will only be used when a particular state tries to find out what the next free generation is. The main draw of this is that all branches will now assign unique generations that won't clash with assignments done across other branches. One minor downside is that in VCC's the generation number might jump sporadically (say from #4 to diffblue#40).
Convert asserts in the cbmc directory to invariant style. Some of the messages I'm not sure about (especially the coverage related things).