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({
code_typet::parametert
(
typet
())},
empty_typet
());
60
61
symbolt
symbol;
62
symbol.
base_name
=
"eval"
;
63
symbol.name=
"eval"
;
64
symbol.type=eval_type;
65
symbol.mode=
"jsil"
;
66
dest.
add
(symbol);
67
}
68
69
// add nan
70
71
{
72
symbolt
symbol;
73
symbol.
base_name
=
"nan"
;
74
symbol.
name
=
"nan"
;
75
symbol.
type
=
floatbv_typet
();
76
symbol.
mode
=
"jsil"
;
77
// mark as already typechecked
78
symbol.
is_extern
=
true
;
79
dest.
add
(symbol);
80
}
81
82
// add empty symbol used for decl statements
83
84
{
85
symbolt
symbol;
86
symbol.
base_name
=
"decl_symbol"
;
87
symbol.
name
=
"decl_symbol"
;
88
symbol.
type
=
empty_typet
();
89
symbol.
mode
=
"jsil"
;
90
// mark as already typechecked
91
symbol.
is_extern
=
true
;
92
dest.
add
(symbol);
93
}
94
95
// add builtin objects
96
const
std::vector<std::string> builtin_objects=
97
{
98
"#lg"
,
"#lg_isNan"
,
"#lg_isFinite"
,
"#lop"
,
"#lop_toString"
,
99
"#lop_valueOf"
,
"#lop_isPrototypeOf"
,
"#lfunction"
,
"#lfp"
,
100
"#leval"
,
"#lerror"
,
"#lep"
,
"#lrerror"
,
"#lrep"
,
"#lterror"
,
101
"#ltep"
,
"#lserror"
,
"#lsep"
,
"#levalerror"
,
"#levalerrorp"
,
102
"#lrangeerror"
,
"#lrangeerrorp"
,
"#lurierror"
,
"#lurierrorp"
,
103
"#lobject"
,
"#lobject_get_prototype_of"
,
"#lboolean"
,
"#lbp"
,
104
"#lbp_toString"
,
"#lbp_valueOf"
,
"#lnumber"
,
"#lnp"
,
105
"#lnp_toString"
,
"#lnp_valueOf"
,
"#lmath"
,
"#lstring"
,
"#lsp"
,
106
"#lsp_toString"
,
"#lsp_valueOf"
,
"#larray"
,
"#lap"
,
"#ljson"
107
};
108
109
for
(
const
auto
&identifier : builtin_objects)
110
{
111
symbolt
new_symbol;
112
new_symbol.
name
=identifier;
113
new_symbol.
type
=
jsil_builtin_object_type
();
114
new_symbol.
base_name
=identifier;
115
new_symbol.
mode
=
"jsil"
;
116
new_symbol.
is_type
=
false
;
117
new_symbol.
is_lvalue
=
false
;
118
// mark as already typechecked
119
new_symbol.
is_extern
=
true
;
120
dest.
add
(new_symbol);
121
}
122
}
symbolt::is_state_var
bool is_state_var
Definition:
symbol.h:62
symbol_tablet
The symbol table.
Definition:
symbol_table.h:20
jsil_internal_additions
void jsil_internal_additions(symbol_tablet &dest)
Definition:
jsil_internal_additions.cpp:22
typet
The type of an expression, extends irept.
Definition:
type.h:29
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:1379
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition:
symbol.h:46
jsil_types.h
Jsil Language.
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:46
signed_int_type
signedbv_typet signed_int_type()
Definition:
c_types.cpp:30
jsil_internal_additions.h
Jsil Language.
std_types.h
Pre-defined types.
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition:
c_types.cpp:243
code_typet
Base type of functions.
Definition:
std_types.h:736
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:28
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:753
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.20