cprover
java_entry_point.cpp File Reference
#include "java_entry_point.h"
#include <algorithm>
#include <set>
#include <iostream>
#include <util/arith_tools.h>
#include <util/prefix.h>
#include <util/std_types.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/cprover_prefix.h>
#include <util/message.h>
#include <util/config.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/suffix.h>
#include <util/c_types.h>
#include <ansi-c/string_constant.h>
#include <goto-programs/remove_exceptions.h>
#include "java_object_factory.h"
#include "java_types.h"
Include dependency graph for java_entry_point.cpp:

Go to the source code of this file.

Macros

#define INITIALIZE   CPROVER_PREFIX "initialize"
 

Functions

static void create_initialize (symbol_tablet &symbol_table)
 
static bool should_init_symbol (const symbolt &sym)
 
void java_static_lifetime_init (symbol_tablet &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, unsigned max_nondet_array_length)
 
exprt::operandst java_build_arguments (const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table, bool assume_init_pointers_not_null, unsigned max_nondet_array_length)
 
void java_record_outputs (const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_tablet &symbol_table)
 
main_function_resultt get_main_symbol (symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool allow_no_body)
 
bool java_entry_point (symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length)
 find entry point and create initialization code for function symbol_table main class message_handler More...
 

Macro Definition Documentation

◆ INITIALIZE

#define INITIALIZE   CPROVER_PREFIX "initialize"

Function Documentation

◆ create_initialize()

◆ get_main_symbol()

◆ java_build_arguments()

exprt::operandst java_build_arguments ( const symbolt function,
code_blockt init_code,
symbol_tablet symbol_table,
bool  assume_init_pointers_not_null,
unsigned  max_nondet_array_length 
)

◆ java_entry_point()

◆ java_record_outputs()

◆ java_static_lifetime_init()

◆ should_init_symbol()

static bool should_init_symbol ( const symbolt sym)
static