Skip to content

Commit 2daecc3

Browse files
author
Enrico Steffinlongo
authored
Merge pull request #7875 from esteffin/esteffin/fix-shadow-memory-trace
Fix shadow memory trace generation
2 parents 42a876f + 7783420 commit 2daecc3

File tree

4 files changed

+11
-4
lines changed

4 files changed

+11
-4
lines changed

regression/cbmc-shadow-memory/trace1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--stop-on-fail --unwind 5
44
^EXIT=10$

src/goto-programs/remove_returns.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,9 @@ Date: September 2009
1717
#include <util/std_expr.h>
1818
#include <util/suffix.h>
1919

20-
#include "goto_model.h"
20+
#include <goto-symex/shadow_memory.h>
2121

22+
#include "goto_model.h"
2223
#include "remove_skip.h"
2324

2425
#define RETURN_VALUE_SUFFIX "#return_value"
@@ -225,7 +226,10 @@ void remove_returnst::operator()(goto_functionst &goto_functions)
225226
findit != goto_functions.function_map.end(),
226227
"called function `" + id2string(function_id) +
227228
"' should have an entry in the function map");
228-
return !findit->second.body_available();
229+
return !findit->second.body_available() &&
230+
function_id != CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL &&
231+
function_id != CPROVER_PREFIX SHADOW_MEMORY_GET_FIELD &&
232+
function_id != CPROVER_PREFIX SHADOW_MEMORY_SET_FIELD;
229233
};
230234

231235
replace_returns(gf_entry.first, gf_entry.second);

src/goto-symex/shadow_memory.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Peter Schrammel
2323
#define SHADOW_MEMORY_LOCAL_SCOPE "_local"
2424
#define SHADOW_MEMORY_GET_FIELD "get_field"
2525
#define SHADOW_MEMORY_SET_FIELD "set_field"
26+
#define SHADOW_MEMORY_SYMBOL_PREFIX "__SM"
2627

2728
class code_function_callt;
2829
class abstract_goto_modelt;

src/goto-symex/symex_assign.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,9 @@ void symex_assignt::assign_non_struct_symbol(
228228
state.record_events.pop();
229229

230230
auto current_assignment_type =
231-
ns.lookup(l2_lhs.get_object_name()).is_auxiliary
231+
ns.lookup(l2_lhs.get_object_name()).is_auxiliary &&
232+
id2string(l2_lhs.get_object_name()).find(SHADOW_MEMORY_SYMBOL_PREFIX) !=
233+
std::string::npos
232234
? symex_targett::assignment_typet::HIDDEN
233235
: assignment_type;
234236

0 commit comments

Comments
 (0)