11 #ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H
12 #define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H
28 std::istream &instream,
29 const std::string &path,
34 const std::string &module,
49 std::string
id()
const override
55 return "JSON symbol table";
60 return {
"json_symtab"};
65 return std::make_unique<json_symtab_languaget>();
73 bool entry_point_exists =
76 return !entry_point_exists;
87 return std::make_unique<json_symtab_languaget>();
Base class for all expressions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::string id() const override
std::unique_ptr< languaget > new_language() override
~json_symtab_languaget() override=default
std::set< std::string > extensions() const override
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
Parse a goto program in json form.
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override
Typecheck a goto program in json form.
bool to_expr(const std::string &, const std::string &, exprt &, const namespacet &, message_handlert &) override
Parses the given string into an expression.
std::string description() const override
void show_parse(std::ostream &out, message_handlert &) override
Output the result of the parsed json file to the output stream passed as a parameter to this function...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Goto Programs with Functions.
std::unique_ptr< languaget > new_json_symtab_language()
Abstract interface to support a programming language.