Dynamic frames: don't instrument __CPROVER_allocated_memory

tautschnig · tautschnig · commit 89d5387439a4 · 2023-12-05T13:51:38.000Z
Doing so (rightly) yields an invariant failure in goto_check_ct.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
@@ -23,6 +23,7 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
   if(function_symbols.empty())
   {
     function_symbols.insert(CPROVER_PREFIX "_start");
+    function_symbols.insert(CPROVER_PREFIX "allocated_memory");
     function_symbols.insert(CPROVER_PREFIX "array_copy");
     function_symbols.insert(CPROVER_PREFIX "array_replace");
     function_symbols.insert(CPROVER_PREFIX "array_set");

Original file line number	Diff line number	Diff line change
`@@ -23,6 +23,7 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)`
`23`	`23`	`if(function_symbols.empty())`
`24`	`24`	`{`
`25`	`25`	`function_symbols.insert(CPROVER_PREFIX "_start");`
	`26`	`+ function_symbols.insert(CPROVER_PREFIX "allocated_memory");`
`26`	`27`	`function_symbols.insert(CPROVER_PREFIX "array_copy");`
`27`	`28`	`function_symbols.insert(CPROVER_PREFIX "array_replace");`
`28`	`29`	`function_symbols.insert(CPROVER_PREFIX "array_set");`