A base class for loop contracts synthesizers. More...

#include <loop_contracts_synthesizer_base.h>

Inheritance diagram for loop_contracts_synthesizer_baset:

Collaboration diagram for loop_contracts_synthesizer_baset:

Public Member Functions
	loop_contracts_synthesizer_baset (goto_modelt &goto_model, messaget &log)

virtual	~loop_contracts_synthesizer_baset ()=default

virtual invariant_mapt	synthesize_all ()=0
	Synthesize loop invariants that are inductive in the given GOTO program. More...

virtual exprt	synthesize (loop_idt)=0
	Synthesize loop invariant for a specified loop in the `goto_model`. More...

Protected Attributes
goto_modelt &	goto_model

messaget &	log

Detailed Description

A base class for loop contracts synthesizers.

Provides a method for synthesizing loop contracts in a given goto_model.

Derived class should clarify what types of goto_model they targets, e.g., a goto_model contains only memory safety checks, or a goto_model contains both memory safety checks and correctness checks.

Definition at line 27 of file loop_contracts_synthesizer_base.h.

Constructor & Destructor Documentation

◆ loop_contracts_synthesizer_baset()

loop_contracts_synthesizer_baset::loop_contracts_synthesizer_baset	(	goto_modelt &	goto_model,
		messaget &	log
	)

inline

Definition at line 30 of file loop_contracts_synthesizer_base.h.

◆ ~loop_contracts_synthesizer_baset()

virtual loop_contracts_synthesizer_baset::~loop_contracts_synthesizer_baset ( )

virtualdefault

Member Function Documentation

◆ synthesize()

virtual exprt loop_contracts_synthesizer_baset::synthesize ( loop_idt )

pure virtual

Synthesize loop invariant for a specified loop in the goto_model.

Implemented in enumerative_loop_contracts_synthesizert.

◆ synthesize_all()

virtual invariant_mapt loop_contracts_synthesizer_baset::synthesize_all ( )

pure virtual

Synthesize loop invariants that are inductive in the given GOTO program.

The result is a map from loop_idt ids of loops to exprt the GOTO-expression representation of synthesized invariants.

Implemented in enumerative_loop_contracts_synthesizert.

Member Data Documentation

◆ goto_model

goto_modelt& loop_contracts_synthesizer_baset::goto_model

protected

Definition at line 46 of file loop_contracts_synthesizer_base.h.

◆ log

messaget& loop_contracts_synthesizer_baset::log