cprover
java_bytecode_internal_additions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 // For INFLIGHT_EXCEPTION_VARIABLE_NAME
12 #include "java_types.h"
13 #include "remove_exceptions.h"
14 
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/pointer_expr.h>
18 #include <util/std_types.h>
19 #include <util/symbol_table_base.h>
20 
22 
24 {
25  // add __CPROVER_rounding_mode
26 
27  {
28  symbolt symbol;
29  symbol.name = rounding_mode_identifier();
30  symbol.base_name = symbol.name;
31  symbol.type=signed_int_type();
32  symbol.mode=ID_C;
33  symbol.is_lvalue=true;
34  symbol.is_state_var=true;
35  symbol.is_thread_local=true;
36  dest.add(symbol);
37  }
38 
39  {
40  auxiliary_symbolt symbol;
43  symbol.mode = ID_java;
44  symbol.type = pointer_type(java_void_type());
45  symbol.type.set(ID_C_no_nondet_initialization, true);
46  symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
47  symbol.is_file_local = false;
48  symbol.is_static_lifetime = true;
49  dest.add(symbol);
50  }
51 }
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
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
The null pointer constant.
Definition: pointer_expr.h:723
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
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
bool is_static_lifetime
Definition: symbol.h:65
bool is_thread_local
Definition: symbol.h:65
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
void java_internal_additions(symbol_table_baset &dest)
empty_typet java_void_type()
Definition: java_types.cpp:37
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
Remove function exceptional returns.
#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Pre-defined types.
Author: Diffblue Ltd.