43 initialize.value=init_code;
45 if(symbol_table.
add(initialize))
63 std::list<irep_idt> matches;
65 for(
const auto &symbol_name_entry :
69 symbol_table_baset::symbolst::const_iterator s_it =
70 symbol_table.
symbols.find(symbol_name_entry.second);
72 if(s_it==symbol_table.
symbols.end())
75 if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
76 matches.push_back(symbol_name_entry.second);
82 message.
error() <<
"main symbol '" <<
config.
main.value() <<
"' not found"
95 main_symbol=matches.front();
101 symbol_table_baset::symbolst::const_iterator s_it =
102 symbol_table.
symbols.find(main_symbol);
104 if(s_it==symbol_table.
symbols.end())
112 const symbolt &symbol=s_it->second;
118 message.
error() <<
"main symbol '" << main_symbol <<
"' has no body"
130 symbol_table_baset::symbolst::const_iterator init_it =
133 if(init_it==symbol_table.
symbols.end())
138 init_code.
add(call_init);
147 init_code.
add(call_main);
153 new_symbol.value.swap(init_code);
155 if(!symbol_table.
insert(std::move(new_symbol)).second)
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
goto_instruction_codet representation of a function call statement.
optionalt< std::string > main
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Class that provides messages with a built-in verbosity 'level'.
virtual void set_message_handler(message_handlert &_message_handler)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
The symbol table base class interface.
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
exprt value
Initial value of symbol.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
bool jsil_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler)
static void create_initialize(symbol_table_baset &symbol_table)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
#define INITIALIZE_FUNCTION