Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets. More...

#include <dfcc_contract_clauses_codegen.h>

Collaboration diagram for dfcc_contract_clauses_codegent:

Public Member Functions
	dfcc_contract_clauses_codegent (goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)

void	gen_spec_assigns_instructions (const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
	Generates instructions encoding the `assigns_clause` targets and adds them to `dest`.

void	gen_spec_frees_instructions (const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
	Generates instructions encoding the `frees_clause` targets and adds them to `dest`.

Protected Member Functions
void	encode_assignable_target_group (const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
	Generates GOTO instructions to build the representation of the given conditional target group.

void	encode_assignable_target (const irep_idt &language_mode, const exprt &target, goto_programt &dest)
	Generates GOTO instructions to build the representation of the given assignable target.

void	encode_freeable_target_group (const irep_idt &language_mode, const conditional_target_group_exprt &group, goto_programt &dest)
	Generates GOTO instructions to build the representation of the given conditional target group.

void	encode_freeable_target (const irep_idt &language_mode, const exprt &target, goto_programt &dest)
	Generates GOTO instructions to build the representation of the given freeable target.

void	inline_and_check_warnings (goto_programt &goto_program)
	Inlines all calls in the given program and checks that the only missing functions or functions without bodies are built-in functions, and that no other warnings happened.

Protected Attributes
goto_modelt &	goto_model

message_handlert &	message_handler

messaget	log

dfcc_libraryt &	library

namespacet	ns

Detailed Description

Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets.

Definition at line 35 of file dfcc_contract_clauses_codegen.h.

Constructor & Destructor Documentation

◆ dfcc_contract_clauses_codegent()

dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent	(	goto_modelt &	goto_model,
		message_handlert &	message_handler,
		dfcc_libraryt &	library )

Parameters

goto_model	GOTO model being transformed
message_handler	Used debug/warning/error messages
library	The contracts instrumentation library

Definition at line 31 of file dfcc_contract_clauses_codegen.cpp.

Member Function Documentation

◆ encode_assignable_target()

void dfcc_contract_clauses_codegent::encode_assignable_target	(	const irep_idt &	language_mode,
		const exprt &	target,
		goto_programt &	dest )

protected

Generates GOTO instructions to build the representation of the given assignable target.

Definition at line 125 of file dfcc_contract_clauses_codegen.cpp.

◆ encode_assignable_target_group()

void dfcc_contract_clauses_codegent::encode_assignable_target_group	(	const irep_idt &	language_mode,
		const conditional_target_group_exprt &	group,
		goto_programt &	dest )

protected

Generates GOTO instructions to build the representation of the given conditional target group.

Definition at line 98 of file dfcc_contract_clauses_codegen.cpp.

◆ encode_freeable_target()

void dfcc_contract_clauses_codegent::encode_freeable_target	(	const irep_idt &	language_mode,
		const exprt &	target,
		goto_programt &	dest )

protected

Generates GOTO instructions to build the representation of the given freeable target.

Definition at line 214 of file dfcc_contract_clauses_codegen.cpp.

◆ encode_freeable_target_group()

void dfcc_contract_clauses_codegent::encode_freeable_target_group	(	const irep_idt &	language_mode,
		const conditional_target_group_exprt &	group,
		goto_programt &	dest )

protected

Generates GOTO instructions to build the representation of the given conditional target group.

Definition at line 187 of file dfcc_contract_clauses_codegen.cpp.

◆ gen_spec_assigns_instructions()

void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions	(	const irep_idt &	language_mode,
		const exprt::operandst &	assigns_clause,
		goto_programt &	dest )

Generates instructions encoding the assigns_clause targets and adds them to dest.

Assumes that all targets in the clause are represented as plain expressions (i.e. an lambdas expressions introduced for function contract targets may are already instanciated).

Parameters

language_mode	Mode to use for fresh symbols
assigns_clause	Sequence of targets to encode
dest	Destination program

Definition at line 43 of file dfcc_contract_clauses_codegen.cpp.

◆ gen_spec_frees_instructions()

void dfcc_contract_clauses_codegent::gen_spec_frees_instructions	(	const irep_idt &	language_mode,
		const exprt::operandst &	frees_clause,
		goto_programt &	dest )

Generates instructions encoding the frees_clause targets and adds them to dest.

Assumes that all targets in the clause are represented as plain expressions (i.e. an lambdas expressions introduced for function contract targets may are already instanciated).

Parameters

language_mode	Mode to use for fresh symbols
frees_clause	Sequence of targets to encode
dest	Destination program

Definition at line 71 of file dfcc_contract_clauses_codegen.cpp.

◆ inline_and_check_warnings()

void dfcc_contract_clauses_codegent::inline_and_check_warnings ( goto_programt & goto_program )

protected

Inlines all calls in the given program and checks that the only missing functions or functions without bodies are built-in functions, and that no other warnings happened.

Definition at line 260 of file dfcc_contract_clauses_codegen.cpp.