property_monitors.cpp File Reference

#include <ac_config.h>
#include <esbmc/esbmc_parseoptions.h>
#include <util/lang/c_types.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>
#include <util/irep/irep.h>
#include <util/message/message.h>
#include <util/base/prefix.h>
#include <util/irep/std_code.h>
#include <util/symtab/symbol.h>
#include <algorithm>
#include <iostream>
#include <map>
#include <set>
#include <string>
#include <utility>
#include <vector>

Include dependency graph for property_monitors.cpp:

Functions
static void	warn_if_monitor_never_switches_back (const goto_functionst &goto_functions)
static void	step_monitor_at_sample_points (goto_programt &prog)
static void	collect_symbol_names (const expr2tc &e, const std::string &prefix, std::set< std::string > &used_syms)
static unsigned int	calc_globals_used (const namespacet &ns, const expr2tc &expr)

Function Documentation

calc_globals_used()

unsigned int calc_globals_used ( const namespacet & ns, const expr2tc & expr )

static

collect_symbol_names()

void collect_symbol_names ( const expr2tc & e, const std::string & prefix, std::set< std::string > & used_syms )

static

step_monitor_at_sample_points()

void step_monitor_at_sample_points ( goto_programt & prog )

static

warn_if_monitor_never_switches_back()

void warn_if_monitor_never_switches_back ( const goto_functionst & goto_functions )

static