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
9
#include "
java_bytecode_internal_additions.h
"
10
11
#include <
util/std_types.h
>
12
#include <
util/cprover_prefix.h
>
13
#include <
util/c_types.h
>
14
15
void
java_internal_additions
(
symbol_tablet
&dest)
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
}
symbolt::name
irep_idt name
The unique identifier.
Definition:
symbol.h:46
c_types.h
symbolt::is_thread_local
bool is_thread_local
Definition:
symbol.h:70
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition:
c_types.cpp:296
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition:
cprover_prefix.h:13
symbolt::mode
irep_idt mode
Language mode.
Definition:
symbol.h:55
symbolt
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition:
symbol.h:33
empty_typet
The empty type.
Definition:
std_types.h:53
symbol_tablet
The symbol table.
Definition:
symbol_table.h:52
symbol_tablet::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition:
symbol_table.cpp:18
symbolt::type
typet type
Type of symbol.
Definition:
symbol.h:37
std_types.h
API to type classes.
cprover_prefix.h
symbolt::is_state_var
bool is_state_var
Definition:
symbol.h:66
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition:
symbol.h:52
java_bytecode_internal_additions.h
java_internal_additions
void java_internal_additions(symbol_tablet &dest)
Definition:
java_bytecode_internal_additions.cpp:15
signed_int_type
signedbv_typet signed_int_type()
Definition:
c_types.cpp:29
symbolt::is_lvalue
bool is_lvalue
Definition:
symbol.h:71
java_bytecode
java_bytecode_internal_additions.cpp
Generated by
1.8.14