dfcc_obeys_contractt Class Reference

Rewrites calls to obeys_contract predicates into calls to the library implementation. More...

#include <dfcc_obeys_contract.h>

Collaboration diagram for dfcc_obeys_contractt:

Public Member Functions
	dfcc_obeys_contractt (dfcc_libraryt &library, message_handlert &message_handler)
void	rewrite_calls (goto_programt &program, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
	Rewrites calls to obeys_contract 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, std::set< irep_idt > &function_pointer_contracts)
	Rewrites calls to obeys_contract 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 Member Functions
void	get_contract_name (const exprt &expr, std::set< irep_idt > &function_pointer_contracts)
	Extracts the name from the second argument of a call to obeys_contract (modulo any intermediate typecast expressions). More...

Protected Attributes
dfcc_libraryt &	library
message_handlert &	message_handler
messaget	log

Detailed Description

Rewrites calls to obeys_contract predicates into calls to the library implementation.

Definition at line 29 of file dfcc_obeys_contract.h.

Constructor & Destructor Documentation

dfcc_obeys_contractt()

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

Parameters

library	The contracts instrumentation library
message_handler	Used for messages

Definition at line 22 of file dfcc_obeys_contract.cpp.

Member Function Documentation

get_contract_name()

void dfcc_obeys_contractt::get_contract_name ( const exprt &  expr, std::set< irep_idt > &  function_pointer_contracts  )

protected

Extracts the name from the second argument of a call to obeys_contract (modulo any intermediate typecast expressions).

and adds it to function_pointer_contracts

Definition at line 42 of file dfcc_obeys_contract.cpp.

rewrite_calls() [1/2]

void dfcc_obeys_contractt::rewrite_calls	(	goto_programt &	program,
		dfcc_cfg_infot &	cfg_info,
		std::set< irep_idt > &	function_pointer_contracts
	)

Rewrites calls to obeys_contract 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 29 of file dfcc_obeys_contract.cpp.

rewrite_calls() [2/2]

void dfcc_obeys_contractt::rewrite_calls	(	goto_programt &	program,
		goto_programt::targett	first_instruction,
		const goto_programt::targett &	last_instruction,
		dfcc_cfg_infot &	cfg_info,
		std::set< irep_idt > &	function_pointer_contracts
	)

Rewrites calls to obeys_contract 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 62 of file dfcc_obeys_contract.cpp.

Member Data Documentation

library

dfcc_libraryt& dfcc_obeys_contractt::library

protected

Definition at line 58 of file dfcc_obeys_contract.h.

log

messaget dfcc_obeys_contractt::log

protected

Definition at line 60 of file dfcc_obeys_contract.h.

message_handler

message_handlert& dfcc_obeys_contractt::message_handler

protected

Definition at line 59 of file dfcc_obeys_contract.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp