CBMC
|
This class rewrites GOTO functions that use the built-ins: More...
#include <dfcc_spec_functions.h>
Public Member Functions | |
dfcc_spec_functionst (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library) | |
void | generate_havoc_function (const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets) |
From a function: More... | |
void | generate_havoc_instructions (const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets) |
Translates original_program that specifies assignable targets into a program that havocs the targets. More... | |
void | to_spec_assigns_function (const irep_idt &function_id, std::size_t &nof_targets) |
Transforms (in place) a function. More... | |
void | to_spec_assigns_instructions (const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets) |
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively using __CPROVER_assignable , __CPROVER_object_whole , __CPROVER_object_from , __CPROVER_object_upto into a program populating write_set_to_fill . More... | |
void | to_spec_frees_function (const irep_idt &function_id, std::size_t &nof_targets) |
Transforms (in place) a function. More... | |
void | to_spec_frees_instructions (const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets) |
Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively using __CPROVER_freeable into a program populating write_set_to_fill . More... | |
Protected Member Functions | |
const typet & | get_target_type (const exprt &expr) |
Extracts the type of an assigns clause target expression The expression must be of the form: expr = cast(address_of(target), empty*) More... | |
Protected Attributes | |
goto_modelt & | goto_model |
message_handlert & | message_handler |
messaget | log |
dfcc_libraryt & | library |
namespacet | ns |
This class rewrites GOTO functions that use the built-ins:
__CPROVER_assignable
,__CPROVER_object_whole
,__CRPOVER_object_from
,__CPROVER_object_upto
,__CPROVER_freeable
into GOTO functions that populate a write set instance or havoc a write set by calling the library implementation of these built-ins. Definition at line 43 of file dfcc_spec_functions.h.
dfcc_spec_functionst::dfcc_spec_functionst | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
dfcc_libraryt & | library | ||
) |
Definition at line 21 of file dfcc_spec_functions.cpp.
void dfcc_spec_functionst::generate_havoc_function | ( | const irep_idt & | function_id, |
const irep_idt & | havoc_function_id, | ||
std::size_t & | nof_targets | ||
) |
From a function:
generates a new function:
Which havocs the targets specified by function_id
, passed
function_id | function to generate instructions from |
havoc_function_id | write set variable to havoc |
nof_targets | maximum number of targets to havoc |
Definition at line 43 of file dfcc_spec_functions.cpp.
void dfcc_spec_functionst::generate_havoc_instructions | ( | const irep_idt & | function_id, |
const goto_programt & | original_program, | ||
const exprt & | write_set_to_havoc, | ||
goto_programt & | havoc_program, | ||
std::size_t & | nof_targets | ||
) |
Translates original_program
that specifies assignable targets into a program that havocs the targets.
original_program
must be already fully inlined, and the only function calls allowed are to the built-ins that specify assignable targets: __CPROVER_assignable
, __CPROVER_object_whole
, __CPROVER_object_from
, __CPROVER_object_upto
.The original_program
is assumed to encode an assigns clause using the built-ins __CPROVER_assignable
, __CPROVER_object_whole
, __CPROVER_object_from
, __CPROVER_object_upto
. The method traverses original_program
and emits a sequence of GOTO instructions in havoc_program
that encode the havocing of the target write set write_set_to_havoc
.
[in] | function_id | function id to use for prefixing fresh variables |
[in] | original_program | program from which to derive the havoc program |
[in] | write_set_to_havoc | write set symbol to havoc |
[out] | havoc_program | destination program for havoc instructions |
[out] | nof_targets | max number of havoc targets discovered |
Definition at line 143 of file dfcc_spec_functions.cpp.
Extracts the type of an assigns clause target expression The expression must be of the form: expr = cast(address_of(target), empty*)
Definition at line 33 of file dfcc_spec_functions.cpp.
void dfcc_spec_functionst::to_spec_assigns_function | ( | const irep_idt & | function_id, |
std::size_t & | nof_targets | ||
) |
Transforms (in place) a function.
into a function
Where:
write_set_to_fill
is the write set to populate.function_id | function to transform in place |
nof_targets | receives the estimated size of the write set |
Definition at line 246 of file dfcc_spec_functions.cpp.
void dfcc_spec_functionst::to_spec_assigns_instructions | ( | const exprt & | write_set_to_fill, |
const irep_idt & | language_mode, | ||
goto_programt & | program, | ||
std::size_t & | nof_targets | ||
) |
Rewrites in place program
expressed in terms of built-ins specifying assignable targets declaratively using __CPROVER_assignable
, __CPROVER_object_whole
, __CPROVER_object_from
, __CPROVER_object_upto
into a program populating write_set_to_fill
.
It is the responsibility of the caller of this method to instrument the resulting program against another write set instance to check them for unwanted side effects.
program
must be already fully inlined, and the only function calls allowed are to the built-ins that specify assignable targets: __CPROVER_assignable
, __CPROVER_object_whole
, __CPROVER_object_from
, __CPROVER_object_upto
.[in] | write_set_to_fill | write set to populate. |
[in] | language_mode | used to format expressions. |
[in,out] | program | function to transform in place |
[out] | nof_targets | receives the estimated size of the write set |
Definition at line 272 of file dfcc_spec_functions.cpp.
void dfcc_spec_functionst::to_spec_frees_function | ( | const irep_idt & | function_id, |
std::size_t & | nof_targets | ||
) |
Transforms (in place) a function.
into a function
Where:
write_set_to_fill
is the write set to populate.The function must be fully inlined and loop free.
function_id | function to transform in place |
nof_targets | receives the estimated size of the write set |
Definition at line 329 of file dfcc_spec_functions.cpp.
void dfcc_spec_functionst::to_spec_frees_instructions | ( | const exprt & | write_set_to_fill, |
const irep_idt & | language_mode, | ||
goto_programt & | program, | ||
std::size_t & | nof_targets | ||
) |
Rewrites in place program
expressed in terms of built-ins specifying freeable targets declaratively using __CPROVER_freeable
into a program populating write_set_to_fill
.
It is the responsibility of the caller of this method to instrument the resulting program against another write set instance to check them for unwanted side effects.
program
must be already fully inlined, and the only function calls allowed are to the built-ins that specify freeable targets: __CPROVER_freeable
.[in] | write_set_to_fill | write set to populate. |
[in] | language_mode | used to format expressions. |
[in,out] | program | function to transform in place |
[out] | nof_targets | receives the estimated size of the write set |
Definition at line 355 of file dfcc_spec_functions.cpp.
|
protected |
Definition at line 202 of file dfcc_spec_functions.h.
|
protected |
Definition at line 205 of file dfcc_spec_functions.h.
|
protected |
Definition at line 204 of file dfcc_spec_functions.h.
|
protected |
Definition at line 203 of file dfcc_spec_functions.h.
|
protected |
Definition at line 206 of file dfcc_spec_functions.h.