cprover
goto_check_java.cpp File Reference

Checks for Errors in Java Programs. More...

#include "goto_check_java.h"
#include <algorithm>
#include <util/arith_tools.h>
#include <util/array_name.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/expr_util.h>
#include <util/find_symbols.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/message.h>
#include <util/options.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <langapi/language.h>
#include <langapi/mode.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <analyses/local_bitvector_analysis.h>
+ Include dependency graph for goto_check_java.cpp:

Go to the source code of this file.

Classes

class  goto_check_javat
 
struct  goto_check_javat::conditiont
 

Functions

void goto_check_java (const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
 
void goto_check_java (const namespacet &ns, const optionst &options, goto_functionst &goto_functions, message_handlert &message_handler)
 
void goto_check_java (const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)
 

Detailed Description

Checks for Errors in Java Programs.

Definition in file goto_check_java.cpp.

Function Documentation

◆ goto_check_java() [1/3]

void goto_check_java ( const irep_idt function_identifier,
goto_functionst::goto_functiont goto_function,
const namespacet ns,
const optionst options,
message_handlert message_handler 
)

Definition at line 1607 of file goto_check_java.cpp.

◆ goto_check_java() [2/3]

void goto_check_java ( const namespacet ns,
const optionst options,
goto_functionst goto_functions,
message_handlert message_handler 
)

Definition at line 1618 of file goto_check_java.cpp.

◆ goto_check_java() [3/3]

void goto_check_java ( const optionst options,
goto_modelt goto_model,
message_handlert message_handler 
)

Definition at line 1632 of file goto_check_java.cpp.