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/std_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/c_types.h>
18 
20 {
21  // add __CPROVER_rounding_mode
22 
23  {
24  symbolt symbol;
25  symbol.base_name = CPROVER_PREFIX "rounding_mode";
26  symbol.name=CPROVER_PREFIX "rounding_mode";
27  symbol.type=signed_int_type();
28  symbol.mode=ID_C;
29  symbol.is_lvalue=true;
30  symbol.is_state_var=true;
31  symbol.is_thread_local=true;
32  dest.add(symbol);
33  }
34 
35  // add __CPROVER_malloc_object
36 
37  {
38  symbolt symbol;
39  symbol.base_name = CPROVER_PREFIX "malloc_object";
40  symbol.name=CPROVER_PREFIX "malloc_object";
41  symbol.type = pointer_type(java_void_type());
42  symbol.mode=ID_C;
43  symbol.is_lvalue=true;
44  symbol.is_state_var=true;
45  symbol.is_thread_local=true;
46  dest.add(symbol);
47  }
48 
49  {
50  auxiliary_symbolt symbol;
53  symbol.mode = ID_java;
54  symbol.type = pointer_type(java_void_type());
55  symbol.type.set(ID_C_no_nondet_initialization, true);
56  symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
57  symbol.is_file_local = false;
58  symbol.is_static_lifetime = true;
59  dest.add(symbol);
60  }
61 }
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
INFLIGHT_EXCEPTION_VARIABLE_BASENAME
#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME
Definition: remove_exceptions.h:22
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
std_types.h
Pre-defined types.
INFLIGHT_EXCEPTION_VARIABLE_NAME
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Definition: remove_exceptions.h:23
java_bytecode_internal_additions.h
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
cprover_prefix.h
remove_exceptions.h
Remove function exceptional returns.
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
java_internal_additions
void java_internal_additions(symbol_table_baset &dest)
Definition: java_bytecode_internal_additions.cpp:19
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
java_types.h
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40