cprover
jsil_internal_additions.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Jsil Language
4
5
Author: Michael Tautschnig, tautschn@amazon.com
6
7
\*******************************************************************/
8
11
12
#include "
jsil_internal_additions.h
"
13
14
#include <
util/std_types.h
>
15
#include <
util/cprover_prefix.h
>
16
#include <
util/symbol_table.h
>
17
18
#include <
util/c_types.h
>
19
20
#include "
jsil_types.h
"
21
22
void
jsil_internal_additions
(
symbol_tablet
&dest)
23
{
24
// add __CPROVER_rounding_mode
25
26
{
27
symbolt
symbol;
28
symbol.
base_name
=
CPROVER_PREFIX
"rounding_mode"
;
29
symbol.
name
=
CPROVER_PREFIX
"rounding_mode"
;
30
symbol.
type
=
signed_int_type
();
31
symbol.
mode
=ID_C;
32
symbol.
is_lvalue
=
true
;
33
symbol.
is_state_var
=
true
;
34
symbol.
is_thread_local
=
true
;
35
// mark as already typechecked
36
symbol.
is_extern
=
true
;
37
dest.
add
(symbol);
38
}
39
40
// add __CPROVER_malloc_object
41
42
{
43
symbolt
symbol;
44
symbol.
base_name
=
CPROVER_PREFIX
"malloc_object"
;
45
symbol.
name
=
CPROVER_PREFIX
"malloc_object"
;
46
symbol.
type
=
pointer_type
(
empty_typet
());
47
symbol.
mode
=ID_C;
48
symbol.
is_lvalue
=
true
;
49
symbol.
is_state_var
=
true
;
50
symbol.
is_thread_local
=
true
;
51
// mark as already typechecked
52
symbol.
is_extern
=
true
;
53
dest.
add
(symbol);
54
}
55
56
// add eval
57
58
{
59
code_typet
eval_type;
60
code_typet::parametert
p;
61
eval_type.
parameters
().push_back(p);
62
63
symbolt
symbol;
64
symbol.
base_name
=
"eval"
;
65
symbol.
name
=
"eval"
;
66
symbol.
type
=eval_type;
67
symbol.
mode
=
"jsil"
;
68
dest.
add
(symbol);
69
}
70
71
// add nan
72
73
{
74
symbolt
symbol;
75
symbol.
base_name
=
"nan"
;
76
symbol.
name
=
"nan"
;
77
symbol.
type
=
floatbv_typet
();
78
symbol.
mode
=
"jsil"
;
79
// mark as already typechecked
80
symbol.
is_extern
=
true
;
81
dest.
add
(symbol);
82
}
83
84
// add empty symbol used for decl statements
85
86
{
87
symbolt
symbol;
88
symbol.
base_name
=
"decl_symbol"
;
89
symbol.
name
=
"decl_symbol"
;
90
symbol.
type
=
empty_typet
();
91
symbol.
mode
=
"jsil"
;
92
// mark as already typechecked
93
symbol.
is_extern
=
true
;
94
dest.
add
(symbol);
95
}
96
97
// add builtin objects
98
const
std::vector<std::string> builtin_objects=
99
{
100
"#lg"
,
"#lg_isNan"
,
"#lg_isFinite"
,
"#lop"
,
"#lop_toString"
,
101
"#lop_valueOf"
,
"#lop_isPrototypeOf"
,
"#lfunction"
,
"#lfp"
,
102
"#leval"
,
"#lerror"
,
"#lep"
,
"#lrerror"
,
"#lrep"
,
"#lterror"
,
103
"#ltep"
,
"#lserror"
,
"#lsep"
,
"#levalerror"
,
"#levalerrorp"
,
104
"#lrangeerror"
,
"#lrangeerrorp"
,
"#lurierror"
,
"#lurierrorp"
,
105
"#lobject"
,
"#lobject_get_prototype_of"
,
"#lboolean"
,
"#lbp"
,
106
"#lbp_toString"
,
"#lbp_valueOf"
,
"#lnumber"
,
"#lnp"
,
107
"#lnp_toString"
,
"#lnp_valueOf"
,
"#lmath"
,
"#lstring"
,
"#lsp"
,
108
"#lsp_toString"
,
"#lsp_valueOf"
,
"#larray"
,
"#lap"
,
"#ljson"
109
};
110
111
for
(
const
auto
&identifier : builtin_objects)
112
{
113
symbolt
new_symbol;
114
new_symbol.
name
=identifier;
115
new_symbol.
type
=
jsil_builtin_object_type
();
116
new_symbol.
base_name
=identifier;
117
new_symbol.
mode
=
"jsil"
;
118
new_symbol.
is_type
=
false
;
119
new_symbol.
is_lvalue
=
false
;
120
// mark as already typechecked
121
new_symbol.
is_extern
=
true
;
122
dest.
add
(new_symbol);
123
}
124
}
symbolt::is_state_var
bool is_state_var
Definition:
symbol.h:61
symbol_tablet
The symbol table.
Definition:
symbol_table.h:19
jsil_internal_additions
void jsil_internal_additions(symbol_tablet &dest)
Definition:
jsil_internal_additions.cpp:22
symbolt::type
typet type
Type of symbol.
Definition:
symbol.h:31
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition:
std_types.h:1398
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition:
symbol.h:46
jsil_types.h
jsil_builtin_object_type
typet jsil_builtin_object_type()
Definition:
jsil_types.cpp:73
symbolt::is_thread_local
bool is_thread_local
Definition:
symbol.h:65
symbolt::mode
irep_idt mode
Language mode.
Definition:
symbol.h:49
empty_typet
The empty type.
Definition:
std_types.h:48
signed_int_type
signedbv_typet signed_int_type()
Definition:
c_types.cpp:30
jsil_internal_additions.h
std_types.h
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition:
c_types.cpp:243
code_typet
Base type of functions.
Definition:
std_types.h:751
code_typet::parameters
const parameterst & parameters() const
Definition:
std_types.h:893
cprover_prefix.h
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition:
symbol_table_base.cpp:18
symbolt::is_extern
bool is_extern
Definition:
symbol.h:66
symbolt
Symbol table entry.
Definition:
symbol.h:27
symbolt::is_type
bool is_type
Definition:
symbol.h:61
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition:
cprover_prefix.h:14
code_typet::parametert
Definition:
std_types.h:788
symbolt::is_lvalue
bool is_lvalue
Definition:
symbol.h:66
symbol_table.h
Author: Diffblue Ltd.
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition:
symbol.h:40
jsil
jsil_internal_additions.cpp
Generated by
1.8.16