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 "remove_exceptions.h"
13 
14 #include <util/std_types.h>
15 #include <util/cprover_prefix.h>
16 #include <util/c_types.h>
17 
19 {
20  // add __CPROVER_rounding_mode
21 
22  {
23  symbolt symbol;
24  symbol.base_name="__CPROVER_rounding_mode";
25  symbol.name=CPROVER_PREFIX "rounding_mode";
26  symbol.type=signed_int_type();
27  symbol.mode=ID_C;
28  symbol.is_lvalue=true;
29  symbol.is_state_var=true;
30  symbol.is_thread_local=true;
31  dest.add(symbol);
32  }
33 
34  // add __CPROVER_malloc_object
35 
36  {
37  symbolt symbol;
38  symbol.base_name="__CPROVER_malloc_object";
39  symbol.name=CPROVER_PREFIX "malloc_object";
40  symbol.type=pointer_type(empty_typet());
41  symbol.mode=ID_C;
42  symbol.is_lvalue=true;
43  symbol.is_state_var=true;
44  symbol.is_thread_local=true;
45  dest.add(symbol);
46  }
47 
48  {
49  auxiliary_symbolt symbol;
52  symbol.mode = ID_java;
53  symbol.type = pointer_type(empty_typet());
54  symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
55  symbol.is_file_local = false;
56  symbol.is_static_lifetime = true;
57  dest.add(symbol);
58  }
59 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool is_thread_local
Definition: symbol.h:67
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Remove function exceptional returns.
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:52
The null pointer constant.
Definition: std_expr.h:4520
exprt value
Initial value of symbol.
Definition: symbol.h:37
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool is_static_lifetime
Definition: symbol.h:67
The empty type.
Definition: std_types.h:54
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
bool is_file_local
Definition: symbol.h:68
void java_internal_additions(symbol_table_baset &dest)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
bool is_lvalue
Definition: symbol.h:68