From 632b4d133e44ae246c63225470bd1eb5ac71ac52 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jan 2022 22:06:25 +0000 Subject: [PATCH] CONTRACTS: is_fresh declarations are handled via the symbol table Update the symbol table and auto-generate __CPROVER_initialize instead of hand-tweaking the function. This will ensure that any further rebuilding of __CPROVER_initialize preserves those changes. --- .../contracts/memory_predicates.cpp | 29 +++++++++---------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index 5fe30bc793e..37a5b6e7a0d 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -16,6 +16,8 @@ Date: July 2021 #include #include +#include + #include #include @@ -188,21 +190,18 @@ void is_fresh_baset::add_declarations(const std::string &decl_string) } } - // We have to set the global memory map array to - // all zeros for this to work properly - const array_typet ty = - to_array_type(tmp_symbol_table.lookup_ref(memmap_name).type); - constant_exprt initial_value(irep_idt(dstringt("0")), ty.subtype()); - array_of_exprt memmap_init(initial_value, ty); - goto_programt::instructiont a = - goto_programt::make_assignment(symbol_exprt(memmap_name, ty), memmap_init); - - // insert the assignment into the initialize function. - auto called_func = - parent.get_goto_functions().function_map.find(INITIALIZE_FUNCTION); - goto_programt &body = called_func->second.body; - auto target = body.get_end_function(); - body.insert_before(target, a); + if(parent.get_goto_functions().function_map.erase(INITIALIZE_FUNCTION) != 0) + { + static_lifetime_init( + parent.get_symbol_table(), + parent.get_symbol_table().lookup_ref(INITIALIZE_FUNCTION).location); + goto_convert( + INITIALIZE_FUNCTION, + parent.get_symbol_table(), + parent.get_goto_functions(), + log.get_message_handler()); + parent.get_goto_functions().update(); + } } void is_fresh_baset::update_fn_call(