cprover
Loading...
Searching...
No Matches
model_argc_argv.cpp File Reference

Initialize command line arguments. More...

#include "model_argc_argv.h"
#include <sstream>
#include <util/cprover_prefix.h>
#include <util/invariant.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/config.h>
#include <util/replace_symbol.h>
#include <util/symbol_table.h>
#include <util/prefix.h>
#include <ansi-c/ansi_c_language.h>
#include <goto-programs/goto_convert.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
+ Include dependency graph for model_argc_argv.cpp:

Go to the source code of this file.

Functions

std::string escape_char (std::string input_string, std::string find_substring, std::string replace_substring)
 
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 argv with up to max_argc pointers into a char array of 4096 bytes.
 

Detailed Description

Initialize command line arguments.

Definition in file model_argc_argv.cpp.

Function Documentation

◆ escape_char()

std::string escape_char ( std::string input_string,
std::string find_substring,
std::string replace_substring )

Definition at line 38 of file model_argc_argv.cpp.

◆ model_argc_argv()

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 argv with up to max_argc pointers into a char array of 4096 bytes.

Parameters
goto_modelContains the input program's symbol table and intermediate representation
argv_argsUser-specified cmd-line arguments (ARGV), when model_argv is TRUE then size of argv_args represents the maximum number of arguments to be modelled
model_argvIf set to TRUE then modelling argv with up to max_argc pointers
message_handlermessage logging
Returns
True, if and only if modelling succeeded

Definition at line 74 of file model_argc_argv.cpp.