execution_state.cpp File Reference

#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <goto-symex/symex_invariant.h>
#include <langapi/language_ui.h>
#include <langapi/languages.h>
#include <langapi/mode.h>
#include <sstream>
#include <string>
#include <util/base/breakpoint.h>
#include <util/lang/c_types.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>
#include <util/expr/type_byte_size.h>
#include <util/base/i2string.h>
#include <irep2/irep2.h>
#include <util/irep/migrate.h>
#include <util/irep/std_expr.h>
#include <vector>
#include <util/base/yaml_parser.h>

Include dependency graph for execution_state.cpp:

Functions
static bool	is_pthread_sync_type (type2tc t)
static expr2tc	mpor_lock_array_key (const expr2tc &array, const BigInt &elem)
static bool	is_lock_array (const expr2tc &e)
static bool	mpor_keys_may_alias (const expr2tc &a, const expr2tc &b)
static bool	mpor_set_conflicts (const std::set< expr2tc > &s, const expr2tc &key)
static bool	exit_code_follows (goto_programt::const_targett call)
	Whether __ESBMC_main has exit-time code (atexit handlers, static destructors) to run between main's return at call and the end hook.
static bool	mpor_transitions_conflict (const std::set< expr2tc > &reads_j, const std::set< expr2tc > &writes_j, const std::set< expr2tc > &reads_l, const std::set< expr2tc > &writes_l)
static void	check_chain_points_forward (const std::vector< std::vector< int > > &chain, const std::vector< unsigned int > &last_transition, unsigned int active_thread, unsigned int j)
	The inductive step of A6.4: every 1 in the chain points forward in run order.

Function Documentation

check_chain_points_forward()

void check_chain_points_forward ( const std::vector< std::vector< int > > & chain, const std::vector< unsigned int > & last_transition, unsigned int active_thread, unsigned int j )

static

The inductive step of A6.4: every 1 in the chain points forward in run order.

Only the active thread's row and column change meaning when it takes a transition – every other entry keeps both its endpoints – so checking those two is checking the step.

exit_code_follows()

bool exit_code_follows ( goto_programt::const_targett call )

static

Whether __ESBMC_main has exit-time code (atexit handlers, static destructors) to run between main's return at call and the end hook.

is_lock_array()

bool is_lock_array ( const expr2tc & e )

static

is_pthread_sync_type()

bool is_pthread_sync_type ( type2tc t )

static

mpor_keys_may_alias()

bool mpor_keys_may_alias ( const expr2tc & a, const expr2tc & b )

static

mpor_lock_array_key()

expr2tc mpor_lock_array_key ( const expr2tc & array, const BigInt & elem )

static

mpor_set_conflicts()

bool mpor_set_conflicts ( const std::set< expr2tc > & s, const expr2tc & key )

static

mpor_transitions_conflict()

bool mpor_transitions_conflict ( const std::set< expr2tc > & reads_j, const std::set< expr2tc > & writes_j, const std::set< expr2tc > & reads_l, const std::set< expr2tc > & writes_l )

static