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 
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 
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;
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