cprover
json_symtab_language.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JSON symbol table language. Accepts a JSON format symbol
4 table that has been produced out-of-process, e.g. by using
5 a compiler's front-end.
6
7Author: Chris Smowton, chris.smowton@diffblue.com
8
9\*******************************************************************/
10
11#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H
12#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H
13
14#include <set>
15#include <string>
16
18#include <langapi/language.h>
19
20#include <util/json.h>
21#include <util/make_unique.h>
22#include <util/symbol_table.h>
23
25{
26public:
27 bool parse(std::istream &instream, const std::string &path) override;
28
29 bool
30 typecheck(symbol_tablet &symbol_table, const std::string &module) override;
31
32 void show_parse(std::ostream &out) override;
33
34 bool
35 to_expr(const std::string &, const std::string &, exprt &, const namespacet &)
36 override
37 {
39 }
40
41 std::string id() const override
42 {
43 return "json_symtab";
44 }
45 std::string description() const override
46 {
47 return "JSON symbol table";
48 }
49
50 std::set<std::string> extensions() const override
51 {
52 return {"json_symtab"};
53 }
54
55 std::unique_ptr<languaget> new_language() override
56 {
57 return util_make_unique<json_symtab_languaget>();
58 }
59
60 bool generate_support_functions(symbol_tablet &symbol_table) override
61 {
62 // check if entry point is already there
63 bool entry_point_exists =
64 symbol_table.symbols.find(goto_functionst::entry_point()) !=
65 symbol_table.symbols.end();
66 return !entry_point_exists;
67 }
68
69 ~json_symtab_languaget() override = default;
70
71protected:
73};
74
75inline std::unique_ptr<languaget> new_json_symtab_language()
76{
77 return util_make_unique<json_symtab_languaget>();
78}
79
80#endif
Base class for all expressions.
Definition: expr.h:54
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::string id() const override
void show_parse(std::ostream &out) override
Output the result of the parsed json file to the output stream passed as a parameter to this function...
~json_symtab_languaget() override=default
std::set< std::string > extensions() const override
std::unique_ptr< languaget > new_language() override
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Typecheck a goto program in json form.
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool parse(std::istream &instream, const std::string &path) override
Parse a goto program in json form.
std::string description() const override
bool to_expr(const std::string &, const std::string &, exprt &, const namespacet &) override
Parses the given string into an expression.
Definition: json.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
Goto Programs with Functions.
std::unique_ptr< languaget > new_json_symtab_language()
Abstract interface to support a programming language.
#define UNIMPLEMENTED
Definition: invariant.h:525
Author: Diffblue Ltd.