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"
131 <<
" unsigned next=0u;\n"
134 <<
" char arg_string[4096];\n"
136 <<
" for(int i=0; i<ARGC && i<" << max_argc <<
"; ++i)\n"
138 <<
" unsigned len;\n"
142 <<
" ARGV[i]=&(arg_string[next]);\n"
149 oss <<
"int ARGC = " << argc <<
";\n"
150 <<
"char *ARGV[" << argc <<
"];\n"
153 <<
"int ARGC = " << argc <<
";\n";
155 for(
auto &arg : argv_args)
168 std::istringstream iss(oss.str());
174 ansi_c_language.
parse(iss,
"");
178 ansi_c_language.
typecheck(tmp_symbol_table,
"<built-in-library>");
185 for(
const auto &symbol_pair : tmp_symbol_table.
symbols)
194 value = symbol_pair.second.value;
218 instruction.source_location_nonconst().set_file(
"<built-in-library>");
220 goto_functionst::function_mapt::iterator start_entry=
226 start_entry->second.body_available(),
227 "entry point expected to have a body");
236 if (main_call->is_other() &&
237 main_call->get_other().get_statement() == ID_input &&
240 main_call->turn_into_skip();
244 if(main_call->is_assume() &&
248 main_call->turn_into_skip();
251 if(main_call->is_function_call())
253 const exprt &func = main_call->call_function();
254 if(func.
id()==ID_symbol &&
bool parse(std::istream &instream, const std::string &path) override
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
std::vector< parametert > parameterst
const parameterst & parameters() const
optionalt< std::string > main
struct configt::ansi_ct ansi_c
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
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)
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.
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
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)
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)
preprocessort preprocessor