cprover
Loading...
Searching...
No Matches
jsil_internal_additions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: 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;
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 eval
43
44 {
46
47 symbolt symbol;
48 symbol.base_name="eval";
49 symbol.name="eval";
50 symbol.type=eval_type;
51 symbol.mode="jsil";
52 dest.add(symbol);
53 }
54
55 // add nan
56
57 {
58 symbolt symbol;
59 symbol.base_name="nan";
60 symbol.name="nan";
61 symbol.type=floatbv_typet();
62 symbol.mode="jsil";
63 // mark as already typechecked
64 symbol.is_extern=true;
65 dest.add(symbol);
66 }
67
68 // add empty symbol used for decl statements
69
70 {
71 symbolt symbol;
72 symbol.base_name="decl_symbol";
73 symbol.name="decl_symbol";
74 symbol.type=empty_typet();
75 symbol.mode="jsil";
76 // mark as already typechecked
77 symbol.is_extern=true;
78 dest.add(symbol);
79 }
80
81 // add builtin objects
82 const std::vector<std::string> builtin_objects=
83 {
84 "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString",
85 "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp",
86 "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror",
87 "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp",
88 "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp",
89 "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp",
90 "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp",
91 "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp",
92 "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson"
93 };
94
95 for(const auto &identifier : builtin_objects)
96 {
97 symbolt new_symbol;
98 new_symbol.name=identifier;
99 new_symbol.type=jsil_builtin_object_type();
100 new_symbol.base_name=identifier;
101 new_symbol.mode="jsil";
102 new_symbol.is_type=false;
103 new_symbol.is_lvalue=false;
104 // mark as already typechecked
105 new_symbol.is_extern=true;
106 dest.add(new_symbol);
107 }
108}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
Base type of functions.
Definition: std_types.h:539
The empty type.
Definition: std_types.h:51
Fixed-width bit-vector with IEEE floating-point interpretation.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_thread_local
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
bool is_state_var
Definition: symbol.h:62
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
void jsil_internal_additions(symbol_tablet &dest)
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:75
Jsil Language.
Pre-defined types.
Author: Diffblue Ltd.