26{

27public:

35

38

40

43

44protected:

48 const std::string &name,

50

53

57

58

63

65};

68{

69public:

74

76

77protected:

80};

83{

84public:

89

91

92protected:

95};

100{

101public:

105

106

107

108 std::set<goto_programt::targett, goto_programt::target_less_than> &

112

113protected:

114 std::set<goto_programt::targett, goto_programt::target_less_than>

116};

122{

123public:

130

131

132

135

136protected:

140};

143{

144public:

148

152};

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Base class for all expressions.

Predicate to be used with the exprt::visit() function.

void operator()(goto_programt &prog)

std::set< goto_programt::targett, goto_programt::target_less_than > & is_fresh_calls()

std::set< goto_programt::targett, goto_programt::target_less_than > function_set

find_is_fresh_calls_visitort()

void operator()(const exprt &exp) override

function_binding_visitort()

Predicate to be used with the exprt::visit() function.

void operator()(const goto_programt &prog)

const goto_functionst & goto_functions

std::set< irep_idt > & function_calls()

std::set< irep_idt > function_set

functions_in_scope_visitort(const goto_functionst &goto_functions, message_handlert &message_handler)

message_handlert & message_handler

A collection of goto functions.

A generic container class for the GOTO intermediate representation of one function.

instructionst::iterator targett

virtual void create_ensures_fn_call(goto_programt::targett &target)=0

void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)

std::string ensures_fn_name

message_handlert & message_handler

std::string requires_fn_name

void add_memory_map_decl(goto_programt &program)

void update_requires(goto_programt &requires_)

void add_memory_map_dead(goto_programt &program)

virtual void create_declarations()=0

array_typet get_memmap_type()

void add_declarations(const std::string &decl_string)

is_fresh_baset(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)

void update_ensures(goto_programt &ensures)

virtual void create_requires_fn_call(goto_programt::targett &target)=0

virtual void create_ensures_fn_call(goto_programt::targett &target)

virtual void create_requires_fn_call(goto_programt::targett &target)

virtual void create_declarations()

virtual void create_ensures_fn_call(goto_programt::targett &target)

virtual void create_declarations()

virtual void create_requires_fn_call(goto_programt::targett &target)