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