cprover
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 <set>
15 #include <string>
16 
18 #include <langapi/language.h>
19 #include <util/json.h>
20 #include <util/make_unique.h>
21 
23 {
24 public:
25  bool parse(std::istream &instream, const std::string &path) override;
26 
27  bool
28  typecheck(symbol_tablet &symbol_table, const std::string &module) override;
29 
30  void show_parse(std::ostream &out) override;
31 
32  bool
33  to_expr(const std::string &, const std::string &, exprt &, const namespacet &)
34  override
35  {
37  }
38 
39  std::set<std::string> extensions() const override
40  {
41  return {"json_symtab"};
42  }
43 
44  std::unique_ptr<languaget> new_language() override
45  {
46  return util_make_unique<json_symtab_languaget>();
47  }
48 
49  bool generate_support_functions(symbol_tablet &symbol_table) override
50  {
51  // check if entry point is already there
52  bool entry_point_exists =
53  symbol_table.symbols.find(goto_functionst::entry_point()) !=
54  symbol_table.symbols.end();
55  return !entry_point_exists;
56  }
57 
58  ~json_symtab_languaget() override = default;
59 
60 protected:
62 };
63 
64 inline std::unique_ptr<languaget> new_json_symtab_language()
65 {
66  return util_make_unique<json_symtab_languaget>();
67 }
68 
69 #endif
bool parse(std::istream &instream, const std::string &path) override
Parse a goto program in json form.
std::unique_ptr< languaget > new_language() override
Goto Programs with Functions.
Definition: json.h:23
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
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...
std::set< std::string > extensions() const override
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Abstract interface to support a programming language.
~json_symtab_languaget() override=default
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Typecheck a goto program in json form.
bool to_expr(const std::string &, const std::string &, exprt &, const namespacet &) override
Parses the given string into an expression.
std::unique_ptr< languaget > new_json_symtab_language()
const symbolst & symbols
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define UNIMPLEMENTED
Definition: invariant.h:497
Base class for all expressions.
Definition: expr.h:54