39 std::string input_string,
40 std::string find_substring,
41 std::string replace_substring){
45 index = input_string.find(find_substring, index);
47 if (index == std::string::npos)
break;
50 input_string.replace(index,
51 replace_substring.size(),
56 index += replace_substring.size();
76 const std::list<std::string> &argv_args,
86 message.
error() <<
"Linking not done, missing "
95 if(main_symbol.
mode!=ID_C)
97 message.
error() <<
"argc/argv modelling is C specific"
104 if(parameters.size()!=2 &&
105 parameters.size()!=3)
107 message.
warning() <<
"main expected to take 2 or 3 arguments,"
108 <<
" argc/argv instrumentation skipped"
121 std::ostringstream oss;
122 unsigned max_argc = argv_args.size();
123 unsigned argc = argv_args.size();
128 <<
"char *ARGV[1];\n"
132 <<
" unsigned next=0u;\n"
137 <<
" for(int i=0; i<ARGC && i<" << max_argc <<
"; ++i)\n"
139 <<
" unsigned len;\n"
151 oss <<
"int ARGC = " << argc <<
";\n"
152 <<
"char *ARGV[" << argc <<
"];\n"
155 <<
"int ARGC = " << argc <<
";\n";
157 for(
auto &arg : argv_args)
170 std::istringstream iss(oss.str());
175 ansi_c_language.
parse(iss,
"", message_handler);
176 config.ansi_c.preprocessor=pp;
180 tmp_symbol_table,
"<built-in-library>", message_handler);
187 for(
const auto &symbol_pair : tmp_symbol_table.
symbols)
199 value = symbol_pair.second.value;
223 instruction.source_location_nonconst().set_file(
"<built-in-library>");
225 goto_functionst::function_mapt::iterator start_entry=
231 start_entry->second.body_available(),
232 "entry point expected to have a body");
241 if (main_call->is_other() &&
242 main_call->get_other().get_statement() == ID_input &&
245 main_call->turn_into_skip();
249 if(main_call->is_assume() &&
253 main_call->turn_into_skip();
256 if(main_call->is_function_call())
258 const exprt &func = main_call->call_function();
259 if(func.
id()==ID_symbol &&
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
std::vector< parametert > parameterst
const parameterst & parameters() const
Base class for all expressions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
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)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
bool has_prefix(const std::string &s, const std::string &prefix)
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
const std::string & id2string(const irep_idt &d)
bool model_argc_argv(goto_modelt &goto_model, const std::list< std::string > &argv_args, bool model_argv, message_handlert &message_handler)
Set up argv to user-specified values (when model_argv is FALSE) or (when model_argv is TRUE) set up a...
std::string escape_char(std::string input_string, std::string find_substring, std::string replace_substring)
Escape selected character in specified string with backslashes.
Initialize command line arguments.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define POSTCONDITION(CONDITION)
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)