Skip to content

Commit daea9f4

Browse files
Do not remove __CPROVER_get_field returns
We are going to interpret them in goto-symex, which is going to assign the return values.
1 parent f1d3489 commit daea9f4

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/goto-programs/remove_returns.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,10 @@ void remove_returnst::operator()(goto_functionst &goto_functions)
225225
findit != goto_functions.function_map.end(),
226226
"called function `" + id2string(function_id) +
227227
"' should have an entry in the function map");
228-
return !findit->second.body_available();
228+
return !findit->second.body_available() &&
229+
function_id != CPROVER_PREFIX "field_decl" &&
230+
function_id != CPROVER_PREFIX "get_field" &&
231+
function_id != CPROVER_PREFIX "set_field";
229232
};
230233

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

0 commit comments

Comments
 (0)