Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditions. More...

#include <dfcc_is_freeable.h>

Collaboration diagram for dfcc_is_freeablet:

Public Member Functions
	dfcc_is_freeablet (dfcc_libraryt &library, message_handlert &message_handler)

void	rewrite_calls (goto_programt &program, dfcc_cfg_infot &cfg_info)
	Rewrites calls to is_freeable and was_freed predicates into calls to the library implementation in the given program, passing the given write_set expression as parameter to the library function. More...

void	rewrite_calls (goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info)
	Rewrites calls to is_fresh predicates into calls to the library implementation in the given program between first_instruction (included) and last_instruction (excluded), passing the given write_set expression as parameter to the library function. More...

Protected Attributes
dfcc_libraryt &	library

message_handlert &	message_handler

Detailed Description

Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditions.

Definition at line 29 of file dfcc_is_freeable.h.

Constructor & Destructor Documentation

◆ dfcc_is_freeablet()

dfcc_is_freeablet::dfcc_is_freeablet	(	dfcc_libraryt &	library,
		message_handlert &	message_handler
	)

Parameters

library	the contracts instrumentation library
message_handler	used for messages

Definition at line 18 of file dfcc_is_freeable.cpp.

Member Function Documentation

◆ rewrite_calls() [1/2]

void dfcc_is_freeablet::rewrite_calls	(	goto_programt &	program,
		dfcc_cfg_infot &	cfg_info
	)

Rewrites calls to is_freeable and was_freed predicates into calls to the library implementation in the given program, passing the given write_set expression as parameter to the library function.

Definition at line 25 of file dfcc_is_freeable.cpp.

◆ rewrite_calls() [2/2]

void dfcc_is_freeablet::rewrite_calls	(	goto_programt &	program,
		goto_programt::targett	first_instruction,
		const goto_programt::targett &	last_instruction,
		dfcc_cfg_infot &	cfg_info
	)

Rewrites calls to is_fresh predicates into calls to the library implementation in the given program between first_instruction (included) and last_instruction (excluded), passing the given write_set expression as parameter to the library function.

Definition at line 36 of file dfcc_is_freeable.cpp.

Member Data Documentation

◆ library

dfcc_libraryt& dfcc_is_freeablet::library

protected

Definition at line 52 of file dfcc_is_freeable.h.

◆ message_handler

message_handlert& dfcc_is_freeablet::message_handler