cprover
|
Convert side_effect_expr_nondett expressions. More...
Go to the source code of this file.
Functions | |
void | convert_nondet (goto_functionst &, symbol_table_baset &, message_handlert &, const object_factory_parameterst &object_factory_parameters) |
Replace calls to nondet library functions with an internal nondet representation. More... | |
void | convert_nondet (goto_modelt &, message_handlert &, const object_factory_parameterst &object_factory_parameters) |
void | convert_nondet (goto_model_functiont &function, message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters, const irep_idt &mode) |
Replace calls to nondet library functions with an internal nondet representation. More... | |
Convert side_effect_expr_nondett expressions.
Definition in file convert_java_nondet.h.
void convert_nondet | ( | goto_functionst & | , |
symbol_table_baset & | , | ||
message_handlert & | , | ||
const object_factory_parameterst & | object_factory_parameters | ||
) |
Replace calls to nondet library functions with an internal nondet representation.
goto_functions | The set of goto programs to modify. |
symbol_table | The symbol table to query/update. |
message_handler | For error logging. |
object_factory_parameters | Parameters for the generation of nondet objects. |
Definition at line 218 of file convert_java_nondet.cpp.
References goto_functionst::compute_location_numbers(), convert_nondet(), object_factory_parameterst::function_id, goto_functionst::function_map, namespacet::lookup(), message_handler, symbolt::mode, and remove_skip().
void convert_nondet | ( | goto_modelt & | , |
message_handlert & | , | ||
const object_factory_parameterst & | object_factory_parameters | ||
) |
Definition at line 248 of file convert_java_nondet.cpp.
References convert_nondet(), goto_modelt::goto_functions, message_handler, and goto_modelt::symbol_table.
void convert_nondet | ( | goto_model_functiont & | function, |
message_handlert & | message_handler, | ||
const object_factory_parameterst & | object_factory_parameters, | ||
const irep_idt & | mode | ||
) |
Replace calls to nondet library functions with an internal nondet representation.
function | goto program to modify |
message_handler | For error logging. |
object_factory_parameters | Parameters for the generation of nondet objects. |
Definition at line 200 of file convert_java_nondet.cpp.
References convert_nondet(), object_factory_parameterst::function_id, and message_handler.