Account for replaced functions in exceptions_map
Invariant in `uncaught_exceptions_analysist::output` expects all functions in the GOTO model to be present in the exceptions_map. However, functions like __CPROVER_assert(...) get replaced by explicit GOTO instructions and will not occur as function calls, thus not be in the map. This fix addresses this issue, which only occurs in a debug output produced with -DDEBUG.
This commit is contained in:
parent
2816b80de5
commit
0496142cd7
|
@ -0,0 +1,7 @@
|
|||
int main(void)
|
||||
{
|
||||
int x;
|
||||
__CPROVER_assume(x < 10);
|
||||
__CPROVER_assert(x != 0, "");
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,14 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=10$
|
||||
^SIGNAL=0$
|
||||
VERIFICATION FAILED
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
When compiling CBMC with -DDEBUG uncaught exception analysis prints an
|
||||
exceptions map per function. This test ensures that meta-functions which are
|
||||
replaced by explicit GOTO instructions (e.g. __CPROVER_assert, __CPROVER_assume)
|
||||
and thus do not occur as explicit function calls in the final GOTO program are
|
||||
handled correctly.
|
|
@ -193,9 +193,11 @@ void uncaught_exceptions_analysist::output(
|
|||
{
|
||||
const auto fn=it->first;
|
||||
const exceptions_mapt::const_iterator found=exceptions_map.find(fn);
|
||||
INVARIANT(
|
||||
found!=exceptions_map.end(),
|
||||
"each function expected to be recorded in `exceptions_map`");
|
||||
// Functions like __CPROVER_assert and __CPROVER_assume are replaced by
|
||||
// explicit GOTO instructions and will not show up in exceptions_map.
|
||||
if(found==exceptions_map.end())
|
||||
continue;
|
||||
|
||||
const auto &fs=found->second;
|
||||
if(!fs.empty())
|
||||
{
|
||||
|
|
Loading…
Reference in New Issue