cprover
java_object_factory.cpp File Reference
#include "java_object_factory.h"
#include <unordered_set>
#include <sstream>
#include <util/arith_tools.h>
#include <util/fresh_symbol.h>
#include <util/c_types.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/prefix.h>
#include <linking/zero_initializer.h>
#include <goto-programs/goto_functions.h>
#include "java_types.h"
#include "java_utils.h"
Include dependency graph for java_object_factory.cpp:

Go to the source code of this file.

Classes

class  java_object_factoryt
 

Functions

static symboltnew_tmp_symbol (symbol_tablet &symbol_table, const source_locationt &loc, const typet &type, const std::string &prefix="tmp_object_factory")
 
static exprt get_nondet_bool (const typet &type)
 
exprt object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, const source_locationt &loc)
 

Function Documentation

§ get_nondet_bool()

static exprt get_nondet_bool ( const typet type)
static
parameters: Desired type (C_bool or plain bool)
Returns
nondet expr of that type

Definition at line 47 of file java_object_factory.cpp.

Referenced by java_object_factoryt::gen_nondet_init().

§ new_tmp_symbol()

static symbolt& new_tmp_symbol ( symbol_tablet symbol_table,
const source_locationt loc,
const typet type,
const std::string &  prefix = "tmp_object_factory" 
)
static

§ object_factory()