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 #include <util/std_types.h>
12 #include <util/cprover_prefix.h>
13 #include <util/c_types.h>
14 
16 {
17  // add __CPROVER_rounding_mode
18 
19  {
20  symbolt symbol;
21  symbol.base_name="__CPROVER_rounding_mode";
22  symbol.name=CPROVER_PREFIX "rounding_mode";
23  symbol.type=signed_int_type();
24  symbol.mode=ID_C;
25  symbol.is_lvalue=true;
26  symbol.is_state_var=true;
27  symbol.is_thread_local=true;
28  dest.add(symbol);
29  }
30 
31  // add __CPROVER_malloc_object
32 
33  {
34  symbolt symbol;
35  symbol.base_name="__CPROVER_malloc_object";
36  symbol.name=CPROVER_PREFIX "malloc_object";
37  symbol.type=pointer_type(empty_typet());
38  symbol.mode=ID_C;
39  symbol.is_lvalue=true;
40  symbol.is_state_var=true;
41  symbol.is_thread_local=true;
42  dest.add(symbol);
43  }
44 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
bool is_thread_local
Definition: symbol.h:70
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:55
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
The empty type.
Definition: std_types.h:53
The symbol table.
Definition: symbol_table.h:52
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
bool is_state_var
Definition: symbol.h:66
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
void java_internal_additions(symbol_tablet &dest)
signedbv_typet signed_int_type()
Definition: c_types.cpp:29
bool is_lvalue
Definition: symbol.h:71