CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bmc_util.cpp Source File

18 void java_setup_symex(

19 const optionst &options,

20 abstract_goto_modelt &goto_model,

21 symex_bmct &symex)

22{

23 // unwinds <clinit> loops to number of enum elements

24 if(options.get_bool_option("java-unwind-enum-static"))

25 {

26 // clang-format off

27 // (it asks for the body to be at the same indent level as the parameters

28 // for some reason)

29 symex.add_loop_unwind_handler(

30 [&goto_model](

31 const call_stackt &context,

32 unsigned loop_num,

33 unsigned unwind,

34 unsigned &max_unwind)

35 { // NOLINT (*)

36 return java_enum_static_init_unwind_handler(

37 context, loop_num, unwind, max_unwind, goto_model.get_symbol_table());

38 });

39 // clang-format on

40 }

41}

abstract_goto_model.h

Abstract interface to eager or lazy GOTO models.

abstract_goto_modelt

Abstract interface to eager or lazy GOTO models.

Definition abstract_goto_model.h:22

abstract_goto_modelt::get_symbol_table

virtual const symbol_tablet & get_symbol_table() const =0

Accessor to get the symbol table.

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

call_stackt

Definition call_stack.h:15

optionst

Definition options.h:23

optionst::get_bool_option

bool get_bool_option(const std::string &option) const

Definition options.cpp:44

symex_bmct

Definition symex_bmc.h:24

symex_bmct::add_loop_unwind_handler

void add_loop_unwind_handler(loop_unwind_handlert handler)

Add a callback function that will be called to determine whether to unwind loops.

Definition symex_bmc.h:61

java_setup_symex

void java_setup_symex(const optionst &options, abstract_goto_modelt &goto_model, symex_bmct &symex)

Registers Java-specific preprocessing handlers with goto-symex.

Definition java_bmc_util.cpp:18

java_bmc_util.h

Bounded Model Checking Utils for Java.

java_enum_static_init_unwind_handler

tvt java_enum_static_init_unwind_handler(const call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)

Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes,...

Definition java_enum_static_init_unwind_handler.cpp:70

java_enum_static_init_unwind_handler.h

Unwind loops in static initializers.

symex_bmc.h

Bounded Model Checking for ANSI-C.