Go to the documentation of this file.
27 initialize.
mode=
"jsil";
41 initialize.
value=init_code;
43 if(symbol_table.
add(initialize))
61 std::list<irep_idt> matches;
67 symbol_tablet::symbolst::const_iterator s_it=
68 symbol_table.
symbols.find(it->second);
70 if(s_it==symbol_table.
symbols.end())
73 if(s_it->second.type.id()==ID_code)
74 matches.push_back(it->second);
93 main_symbol=matches.front();
99 symbol_tablet::symbolst::const_iterator s_it=
100 symbol_table.
symbols.find(main_symbol);
102 if(s_it==symbol_table.
symbols.end())
110 const symbolt &symbol=s_it->second;
116 message.error() <<
"main symbol '" << main_symbol <<
"' has no body"
128 symbol_tablet::symbolst::const_iterator init_it=
131 if(init_it==symbol_table.
symbols.end())
136 init_code.
add(call_init);
145 init_code.
add(call_main);
154 if(!symbol_table.
insert(std::move(new_symbol)).second)
157 message.set_message_handler(message_handler);
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
typet type
Type of symbol.
optionalt< std::string > main
irep_idt base_name
Base (non-scoped) name.
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
irep_idt mode
Language mode.
const std::string & id2string(const irep_idt &d)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define INITIALIZE_FUNCTION
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
void add(const codet &code)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
exprt value
Initial value of symbol.
bool jsil_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
source_locationt location
Source code location of definition of symbol.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
#define forall_symbol_base_map(it, expr, base_name)
Goto Programs with Functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
source_locationt & add_source_location()
A codet representing an assignment in the program.
irep_idt name
The unique identifier.
static void create_initialize(symbol_tablet &symbol_table)