CBMC
json_symtab_language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: 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 
7 Author: 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 <util/json.h>
15 #include <util/symbol_table_base.h>
16 
18 
19 #include <langapi/language.h>
20 
21 #include <set>
22 #include <string>
23 
25 {
26 public:
27  bool parse(
28  std::istream &instream,
29  const std::string &path,
30  message_handlert &message_handler) override;
31 
32  bool typecheck(
33  symbol_table_baset &symbol_table,
34  const std::string &module,
35  message_handlert &message_handler) override;
36 
37  void show_parse(std::ostream &out, message_handlert &) override;
38 
39  bool to_expr(
40  const std::string &,
41  const std::string &,
42  exprt &,
43  const namespacet &,
44  message_handlert &) override
45  {
47  }
48 
49  std::string id() const override
50  {
51  return "json_symtab";
52  }
53  std::string description() const override
54  {
55  return "JSON symbol table";
56  }
57 
58  std::set<std::string> extensions() const override
59  {
60  return {"json_symtab"};
61  }
62 
63  std::unique_ptr<languaget> new_language() override
64  {
65  return std::make_unique<json_symtab_languaget>();
66  }
67 
69  symbol_table_baset &symbol_table,
70  message_handlert &) override
71  {
72  // check if entry point is already there
73  bool entry_point_exists =
74  symbol_table.symbols.find(goto_functionst::entry_point()) !=
75  symbol_table.symbols.end();
76  return !entry_point_exists;
77  }
78 
79  ~json_symtab_languaget() override = default;
80 
81 protected:
83 };
84 
85 inline std::unique_ptr<languaget> new_json_symtab_language()
86 {
87  return std::make_unique<json_symtab_languaget>();
88 }
89 
90 #endif
Base class for all expressions.
Definition: expr.h:56
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...
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:94
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.
#define UNIMPLEMENTED
Definition: invariant.h:558
Author: Diffblue Ltd.