cprover
Loading...
Searching...
No Matches
java_bytecode_internal_additions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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/pointer_expr.h>
17#include <util/std_types.h>
19
21
23{
24 // add __CPROVER_rounding_mode
25
26 {
28 symbol.base_name = symbol.name;
29 symbol.is_lvalue=true;
30 symbol.is_state_var=true;
31 symbol.is_thread_local=true;
32 dest.add(symbol);
33 }
34
35 {
36 auxiliary_symbolt symbol{
39 ID_java};
41 symbol.type.set(ID_C_no_nondet_initialization, true);
43 symbol.is_static_lifetime = true;
44 dest.add(symbol);
45 }
46}
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:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
The null pointer constant.
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_static_lifetime
Definition symbol.h:70
bool is_thread_local
Definition symbol.h:71
bool is_state_var
Definition symbol.h:66
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:72
exprt value
Initial value of symbol.
Definition symbol.h:34
void java_internal_additions(symbol_table_baset &dest)
empty_typet java_void_type()
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Remove function exceptional returns.
#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Pre-defined types.
Author: Diffblue Ltd.