Skip to content

Commit 7783420

Browse files
author
Enrico Steffinlongo
committed
Better remove_returns for shadow_memory functions
Improve stub function detection for shadow memory intrinsics in remove_returns.
1 parent 2074039 commit 7783420

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

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);

0 commit comments

Comments
 (0)