Merge pull request #8094 from tautschnig/bugfixes/dfcc-allocated-memory

Dynamic frames: don't instrument __CPROVER_allocated_memory
diffblue · Dec 5, 2023 · 64fe4d0 · 64fe4d0
2 parents 42225bc + 89d5387
commit 64fe4d0
Showing 1 changed file with 1 addition and 0 deletions.
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");