12 #ifndef CPROVER_LANGAPI_LANGUAGE_H 13 #define CPROVER_LANGAPI_LANGUAGE_H 15 #include <unordered_set> 33 #define OPT_FUNCTIONS \ 36 #define HELP_FUNCTIONS \ 37 " --function name set main function name\n" 48 std::istream &instream,
49 const std::string &path,
50 std::ostream &outstream) {
return false; }
53 std::istream &instream,
54 const std::string &path)=0;
70 const std::string &module,
71 std::set<std::string> &modules);
102 const std::string &module)=0;
106 virtual std::string
id()
const {
return ""; }
109 {
return std::set<std::string>(); }
154 const std::string &code,
155 const std::string &module,
175 const symbolt &function_symbol,
176 size_t parameter_index,
192 #endif // CPROVER_UTIL_LANGUAGE_H
The type of an expression.
bool is_symbol_opaque_function(const symbolt &symbol)
To identify if a given symbol is an opaque function and hence needs to be stubbed.
virtual std::set< std::string > extensions() const
virtual std::string description() const
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
virtual void get_language_options(const cmdlinet &)
virtual bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
Encodes the given type in a language-specific way.
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual irep_idt generate_opaque_stub_body(symbolt &symbol, symbol_tablet &symbol_table)
To generate the stub function for the opaque function in question.
virtual void modules_provided(std::set< std::string > &modules)
static irep_idt get_stub_return_symbol_name(const irep_idt &function_id)
To get the name of the symbol to be used for the return value of the function.
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
virtual bool interfaces(symbol_tablet &symbol_table)
virtual std::string id() const
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0
Parses the given string into an expression.
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual std::unique_ptr< languaget > new_language()=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool language_options_initialized
void generate_opaque_parameter_symbols(symbolt &function_symbol, symbol_tablet &symbol_table)
To create stub parameter symbols for each parameter the function has and assign their IDs into the pa...
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
virtual void show_parse(std::ostream &out)=0
Base class for all expressions.
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
The symbol table base class interface.
virtual parameter_symbolt build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert ¶meter)
To build the parameter symbol and choose its name.
bool generate_opaque_stubs
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
virtual bool parse(std::istream &instream, const std::string &path)=0
system_library_symbolst system_symbols
void generate_opaque_method_stubs(symbol_tablet &symbol_table)
When there are opaque methods (e.g.
void set_should_generate_opaque_method_stubs(bool should_generate_stubs)
Turn on or off stub generation.