cprover
convert_java_nondet.h File Reference

Convert side_effect_expr_nondett expressions. More...

#include <cstddef>
#include <util/irep.h>
Include dependency graph for convert_java_nondet.h:
This graph shows which files directly or indirectly include this file:

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...
 

Detailed Description

Convert side_effect_expr_nondett expressions.

Definition in file convert_java_nondet.h.

Function Documentation

◆ convert_nondet() [1/3]

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.

Parameters
goto_functionsThe set of goto programs to modify.
symbol_tableThe symbol table to query/update.
message_handlerFor error logging.
object_factory_parametersParameters 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().

◆ convert_nondet() [2/3]

void convert_nondet ( goto_modelt ,
message_handlert ,
const object_factory_parameterst object_factory_parameters 
)

◆ convert_nondet() [3/3]

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.

Parameters
functiongoto program to modify
message_handlerFor error logging.
object_factory_parametersParameters 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.