CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_set_return_value.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_symex.h"
13
15 statet &state,
16 const exprt &return_value)
17{
18 // we must be inside a function that was called
19 PRECONDITION(!state.call_stack().empty());
20
21 framet &frame = state.call_stack().top();
22 if(frame.return_value_symbol.has_value())
23 {
24 symex_assign(state, frame.return_value_symbol.value(), return_value);
25 }
26}
framet & top()
Definition call_stack.h:17
Base class for all expressions.
Definition expr.h:56
Stack frames – these are used for function calls and for exceptions.
std::optional< symbol_exprt > return_value_symbol
Definition frame.h:39
Central data structure: state.
call_stackt & call_stack()
void symex_set_return_value(statet &state, const exprt &return_value)
Symbolically execute a SET_RETURN_VALUE instruction.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Symbolic Execution.
#define PRECONDITION(CONDITION)
Definition invariant.h:463