cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
17
#include <
goto-programs/goto_functions.h
>
18
19
#include <
langapi/language.h
>
20
21
#include <set>
22
#include <string>
23
24
class
json_symtab_languaget
:
public
languaget
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
{
46
UNIMPLEMENTED
;
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
68
bool
generate_support_functions
(
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
:
82
jsont
parsed_json_file
;
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
exprt
Base class for all expressions.
Definition
expr.h:57
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition
goto_functions.h:97
json_symtab_languaget
Definition
json_symtab_language.h:25
json_symtab_languaget::id
std::string id() const override
Definition
json_symtab_language.h:49
json_symtab_languaget::~json_symtab_languaget
~json_symtab_languaget() override=default
json_symtab_languaget::extensions
std::set< std::string > extensions() const override
Definition
json_symtab_language.h:58
json_symtab_languaget::new_language
std::unique_ptr< languaget > new_language() override
Definition
json_symtab_language.h:63
json_symtab_languaget::parse
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
Parse a goto program in json form.
Definition
json_symtab_language.cpp:25
json_symtab_languaget::generate_support_functions
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...
Definition
json_symtab_language.h:68
json_symtab_languaget::typecheck
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override
Typecheck a goto program in json form.
Definition
json_symtab_language.cpp:38
json_symtab_languaget::to_expr
bool to_expr(const std::string &, const std::string &, exprt &, const namespacet &, message_handlert &) override
Parses the given string into an expression.
Definition
json_symtab_language.h:39
json_symtab_languaget::description
std::string description() const override
Definition
json_symtab_language.h:53
json_symtab_languaget::parsed_json_file
jsont parsed_json_file
Definition
json_symtab_language.h:82
json_symtab_languaget::show_parse
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_symtab_language.cpp:64
jsont
Definition
json.h:27
languaget::languaget
languaget()
Definition
language.h:219
message_handlert
Definition
message.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition
symbol_table_base.h:31
goto_functions.h
Goto Programs with Functions.
json.h
new_json_symtab_language
std::unique_ptr< languaget > new_json_symtab_language()
Definition
json_symtab_language.h:85
language.h
Abstract interface to support a programming language.
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition
invariant.h:558
symbol_table_base.h
Author: Diffblue Ltd.
json-symtab-language
json_symtab_language.h
Generated by
1.17.0