CBMC
replace_java_nondet.h File Reference

Replace Java Nondet expressions. More...

+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void replace_java_nondet (goto_modelt &)
 Replace calls to nondet library functions with an internal nondet representation. More...
 
void replace_java_nondet (goto_functionst &)
 
void replace_java_nondet (goto_model_functiont &function)
 Replace calls to nondet library functions with an internal nondet representation in a single function. More...
 

Detailed Description

Replace Java Nondet expressions.

Definition in file replace_java_nondet.h.

Function Documentation

◆ replace_java_nondet() [1/3]

void replace_java_nondet ( goto_functionst goto_functions)

Definition at line 331 of file replace_java_nondet.cpp.

◆ replace_java_nondet() [2/3]

void replace_java_nondet ( goto_model_functiont function)

Replace calls to nondet library functions with an internal nondet representation in a single function.

Parameters
functionThe goto program to modify.

Definition at line 323 of file replace_java_nondet.cpp.

◆ replace_java_nondet() [3/3]

void replace_java_nondet ( goto_modelt goto_model)

Replace calls to nondet library functions with an internal nondet representation.

Parameters
goto_modelThe goto program to modify.

Definition at line 344 of file replace_java_nondet.cpp.