Go to the documentation of this file.
12 #ifndef CPROVER_LANGAPI_LANGUAGE_H
13 #define CPROVER_LANGAPI_LANGUAGE_H
19 #include <unordered_set>
33 #define OPT_FUNCTIONS \
36 #define HELP_FUNCTIONS \
37 " --function name set main function name\n"
50 std::istream &instream,
51 const std::string &path,
52 std::ostream &outstream)
62 std::istream &instream,
63 const std::string &path)=0;
79 const std::string &module,
80 std::set<std::string> &modules);
125 const std::string &module)=0;
144 const std::string &module,
145 const bool keep_file_local)
149 "three-argument typecheck should only be called for files written"
150 " in a language that allows file-local symbols, like C");
155 virtual std::string
id()
const = 0;
202 const std::string &code,
203 const std::string &module,
215 #endif // CPROVER_UTIL_LANGUAGE_H
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void show_parse(std::ostream &out)=0
virtual std::string id() const =0
The type of an expression, extends irept.
virtual bool can_keep_file_local()
Is it possible to call three-argument typecheck() on this object?
virtual std::string description() const =0
Base class for all expressions.
virtual std::set< std::string > extensions() const =0
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Requests this languaget should populate the body of method function_id in symbol_table.
virtual std::unique_ptr< languaget > new_language()=0
virtual void set_language_options(const optionst &)
Set language-specific options.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual void modules_provided(std::set< std::string > &modules)
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
The symbol table base class interface.
virtual bool parse(std::istream &instream, const std::string &path)=0
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local)
typecheck without removing specified entries from the symbol table
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 interfaces(symbol_tablet &symbol_table)
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
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 methods_provided(std::unordered_set< irep_idt > &methods) const
Should fill methods with the symbol identifiers of all methods this languaget can provide a body for,...