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
14#include <util/c_types.h>
15#include <util/std_types.h>
17
19
20#include "jsil_types.h"
21
23{
24 // add __CPROVER_rounding_mode
25
26 {
28 symbol.base_name = symbol.name;
29 symbol.is_lvalue=true;
30 symbol.is_state_var=true;
31 symbol.is_thread_local=true;
32 // mark as already typechecked
33 symbol.is_extern=true;
34 dest.add(symbol);
35 }
36
37 // add eval
38
39 {
41
42 symbolt symbol{"eval", eval_type, "jsil"};
43 symbol.base_name="eval";
44 dest.add(symbol);
45 }
46
47 // add nan
48
49 {
50 symbolt symbol{"nan", floatbv_typet(), "jsil"};
51 symbol.base_name="nan";
52 // mark as already typechecked
53 symbol.is_extern=true;
54 dest.add(symbol);
55 }
56
57 // add empty symbol used for decl statements
58
59 {
60 symbolt symbol{"decl_symbol", empty_typet(), "jsil"};
61 symbol.base_name="decl_symbol";
62 // mark as already typechecked
63 symbol.is_extern=true;
64 dest.add(symbol);
65 }
66
67 // add builtin objects
68 const std::vector<std::string> builtin_objects=
69 {
70 "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString",
71 "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp",
72 "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror",
73 "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp",
74 "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp",
75 "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp",
76 "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp",
77 "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp",
78 "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson"
79 };
80
81 for(const auto &identifier : builtin_objects)
82 {
83 symbolt new_symbol{identifier, jsil_builtin_object_type(), "jsil"};
84 new_symbol.base_name=identifier;
85 // mark as already typechecked
86 new_symbol.is_extern=true;
87 dest.add(new_symbol);
88 }
89}
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:27
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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.
The symbol table base class interface.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
void jsil_internal_additions(symbol_table_baset &dest)
typet jsil_builtin_object_type()
Jsil Language.
Pre-defined types.
Author: Diffblue Ltd.