10#ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
11#define CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
23#define OPT_ANSI_C_LANGUAGE \
24 "(max-nondet-tree-depth):" \
25 "(min-null-tree-depth):"
27#define HELP_ANSI_C_LANGUAGE \
28 " {y--max-nondet-tree-depth} {uN} \t " \
29 "limit size of nondet (e.g. input) object tree; at level {uN} pointers are " \
31 " {y--min-null-tree-depth} {uN} \t " \
32 "minimum level at which a pointer can first be NULL in a recursively " \
33 "nondet initialized struct\n" \
46 const std::string &path,
51 const std::string &path)
override;
58 const bool keep_file_local)
override;
63 const bool keep_file_local,
64 const std::set<irep_idt> &
keep);
98 const std::string &code,
106 std::string
id()
const override {
return "C"; }
108 std::set<std::string>
extensions()
const override;
std::unique_ptr< languaget > new_ansi_c_language()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
~ansi_c_languaget() override
std::set< std::string > extensions() const override
void show_parse(std::ostream &out) override
bool parse(std::istream &instream, const std::string &path) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
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
bool typecheck(symbol_table_baset &symbol_table, const std::string &module) override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void set_language_options(const optionst &options) override
Set language-specific options.
std::string description() const override
void modules_provided(std::set< std::string > &modules) override
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
bool can_keep_file_local() override
Is it possible to call three-argument typecheck() on this object?
ansi_c_parse_treet parse_tree
c_object_factory_parameterst object_factory_params
std::unique_ptr< languaget > new_language() override
bool generate_support_functions(symbol_table_baset &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::string id() const override
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The symbol table base class interface.
The type of an expression, extends irept.
Abstract interface to support a programming language.
void set(const optionst &)
Assigns the parameters from given options.