CBMC
|
Replace Java Nondet expressions. More...
#include "replace_java_nondet.h"
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <util/std_code.h>
#include <algorithm>
#include <regex>
Go to the source code of this file.
Classes | |
class | nondet_instruction_infot |
Holds information about any discovered nondet methods, with extreme type- safety. More... | |
Functions | |
static nondet_instruction_infot | is_nondet_returning_object (const code_function_callt &function_call) |
Checks whether the function call is one of our nondet library functions. More... | |
static nondet_instruction_infot | get_nondet_instruction_info (const goto_programt::const_targett &instr) |
Check whether the instruction is a function call which matches one of the recognised nondet library methods, and return some information about it. More... | |
static bool | is_symbol_with_id (const exprt &expr, const irep_idt &identifier) |
Return whether the expression is a symbol with the specified identifier. More... | |
static bool | is_typecast_with_id (const exprt &expr, const irep_idt &identifier) |
Return whether the expression is a typecast with the specified identifier. More... | |
static bool | is_assignment_from (const goto_programt::instructiont &instr, const irep_idt &identifier) |
Return whether the instruction is an assignment, and the rhs is a symbol or typecast expression with the specified identifier. More... | |
static bool | is_return_with_variable (const goto_programt::instructiont &instr, const irep_idt &identifier) |
Return whether the instruction is a return, and the rhs is a symbol or typecast expression with the specified identifier. More... | |
static goto_programt::targett | check_and_replace_target (goto_programt &goto_program, const goto_programt::targett &target) |
Given an iterator into a list of instructions, modify the list to replace 'nondet' library functions with CBMC-native nondet expressions, and return an iterator to the next instruction to check. More... | |
static void | replace_java_nondet (goto_programt &goto_program) |
Checks each instruction in the goto program to see whether it is a method returning nondet. More... | |
void | replace_java_nondet (goto_model_functiont &function) |
Replace calls to nondet library functions with an internal nondet representation in a single function. More... | |
void | replace_java_nondet (goto_functionst &goto_functions) |
void | replace_java_nondet (goto_modelt &goto_model) |
Replace calls to nondet library functions with an internal nondet representation. More... | |
Replace Java Nondet expressions.
Definition in file replace_java_nondet.cpp.
|
static |
Given an iterator into a list of instructions, modify the list to replace 'nondet' library functions with CBMC-native nondet expressions, and return an iterator to the next instruction to check.
It's important to note that this method also deals with the fact that in the GOTO program it assigns function return values to temporary variables, performs validation and then assigns the value into the actual variable.
Example:
return_tmp0=org.cprover.CProver.nondetWithoutNull:()Ljava/lang/Object;(); ... Various validations of type and value here. obj = (<type-of-obj>)return_tmp0;
We're going to replace all of these lines with obj = NONDET(<type-of-obj>)
In the situation of a direct return, the end result should be: return NONDET(<type-of-obj>)
goto_program | The goto program to modify. |
target | A single step of the goto program which may be erased and replaced. |
Definition at line 196 of file replace_java_nondet.cpp.
|
static |
Check whether the instruction is a function call which matches one of the recognised nondet library methods, and return some information about it.
instr | A goto-program instruction to check. |
Definition at line 90 of file replace_java_nondet.cpp.
|
static |
Return whether the instruction is an assignment, and the rhs is a symbol or typecast expression with the specified identifier.
instr | A goto program instruction. |
identifier | Some identifier. |
Definition at line 141 of file replace_java_nondet.cpp.
|
static |
Checks whether the function call is one of our nondet library functions.
function_call | The function call declaration to check. |
Definition at line 68 of file replace_java_nondet.cpp.
|
static |
Return whether the instruction is a return, and the rhs is a symbol or typecast expression with the specified identifier.
instr | A goto program instruction. |
identifier | Some identifier. |
Definition at line 161 of file replace_java_nondet.cpp.
Return whether the expression is a symbol with the specified identifier.
expr | The expression which may be a symbol. |
identifier | Some identifier. |
Definition at line 108 of file replace_java_nondet.cpp.
Return whether the expression is a typecast with the specified identifier.
expr | The expression which may be a typecast. |
identifier | Some identifier. |
Definition at line 119 of file replace_java_nondet.cpp.
void replace_java_nondet | ( | goto_functionst & | goto_functions | ) |
Definition at line 331 of file replace_java_nondet.cpp.
void replace_java_nondet | ( | goto_model_functiont & | function | ) |
Replace calls to nondet library functions with an internal nondet representation in a single function.
function | The goto program to modify. |
Definition at line 323 of file replace_java_nondet.cpp.
void replace_java_nondet | ( | goto_modelt & | goto_model | ) |
Replace calls to nondet library functions with an internal nondet representation.
goto_model | The goto program to modify. |
Definition at line 344 of file replace_java_nondet.cpp.
|
static |
Checks each instruction in the goto program to see whether it is a method returning nondet.
If it is, replaces the function call with an irep representing a nondet side effect with an appropriate type.
goto_program | The goto program to modify. |
Definition at line 309 of file replace_java_nondet.cpp.