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 
13 
15 
16 #include <util/std_types.h>
17 #include <util/cprover_prefix.h>
18 #include <util/symbol_table.h>
19 
20 #include <util/c_types.h>
21 
22 #include "jsil_types.h"
23 
25 {
26  // add __CPROVER_rounding_mode
27 
28  {
29  symbolt symbol;
30  symbol.name = rounding_mode_identifier();
31  symbol.base_name = symbol.name;
32  symbol.type=signed_int_type();
33  symbol.mode=ID_C;
34  symbol.is_lvalue=true;
35  symbol.is_state_var=true;
36  symbol.is_thread_local=true;
37  // mark as already typechecked
38  symbol.is_extern=true;
39  dest.add(symbol);
40  }
41 
42  // add __CPROVER_malloc_object
43 
44  {
45  symbolt symbol;
46  symbol.base_name = CPROVER_PREFIX "malloc_object";
47  symbol.name=CPROVER_PREFIX "malloc_object";
48  symbol.type=pointer_type(empty_typet());
49  symbol.mode=ID_C;
50  symbol.is_lvalue=true;
51  symbol.is_state_var=true;
52  symbol.is_thread_local=true;
53  // mark as already typechecked
54  symbol.is_extern=true;
55  dest.add(symbol);
56  }
57 
58  // add eval
59 
60  {
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:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
jsil_internal_additions
void jsil_internal_additions(symbol_tablet &dest)
Definition: jsil_internal_additions.cpp:24
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: bitvector_types.h:322
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:75
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:51
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:539
rounding_mode_identifier
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Definition: adjust_float_expressions.cpp:24
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:556
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
symbol_table.h
Author: Diffblue Ltd.
adjust_float_expressions.h
Symbolic Execution.
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40