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_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_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 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
Base type of functions.
Definition: std_types.h:764
bool is_thread_local
Definition: symbol.h:67
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
#define CPROVER_PREFIX
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1351
irep_idt mode
Language mode.
Definition: symbol.h:52
Jsil Language.
void jsil_internal_additions(symbol_tablet &dest)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:73
The empty type.
Definition: std_types.h:54
The symbol table.
Definition: symbol_table.h:19
Author: Diffblue Ltd.
bool is_extern
Definition: symbol.h:68
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
bool is_state_var
Definition: symbol.h:63
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
bool is_type
Definition: symbol.h:63
bool is_lvalue
Definition: symbol.h:68