llzk::verif::detail Namespace Reference

Common interface for precondition and postcondition operations. More...

Classes
class	AssumeDetOpGenericAdaptorBase
struct	CallableSummaryKey
	Cache key for one interprocedural callable-result summary query. More...
struct	CallableSummaryKeyInfo
struct	ConditionOpInterfaceInterfaceTraits
struct	ConditionOpInterfaceTrait
class	ContractEndOpGenericAdaptorBase
class	ContractOpGenericAdaptorBase
struct	ContractTargetOpInterfaceInterfaceTraits
struct	ContractTargetOpInterfaceTrait
class	DecreasesOpGenericAdaptorBase
class	EnsureComputeOpGenericAdaptorBase
class	EnsureConstrainOpGenericAdaptorBase
class	ForbiddenInfluenceAnalyzer
	Interprocedural verifier-local analysis for forbidden precondition influence. More...
struct	IncludedContractFailure
	One included precondition that becomes illegal under a specific caller binding. More...
struct	IncludedContractSummary
	Summary of all included-contract precondition failures under a specific caller binding. More...
struct	IncludedContractSummaryKey
	Cache key for one interprocedural included-contract summary query. More...
struct	IncludedContractSummaryKeyInfo
class	IncludeOpGenericAdaptorBase
class	IncreasesOpGenericAdaptorBase
class	InvariantOpGenericAdaptorBase
struct	InvariantTargetOpInterfaceInterfaceTraits
struct	InvariantTargetOpInterfaceTrait
class	OldOpGenericAdaptorBase
struct	PostconditionOpInterfaceInterfaceTraits
struct	PostconditionOpInterfaceTrait
struct	PreconditionOpInterfaceInterfaceTraits
struct	PreconditionOpInterfaceTrait
class	ProveDetOpGenericAdaptorBase
class	RequireComputeOpGenericAdaptorBase
class	RequireConstrainOpGenericAdaptorBase
class	StepOpGenericAdaptorBase
class	StepYieldOpGenericAdaptorBase
class	VerifAssertOpGenericAdaptorBase
class	VerifProveOpGenericAdaptorBase
class	VerifSMTProveOpGenericAdaptorBase

Typedefs
using	Influence = ForbiddenPreconditionInfluence
using	InfluenceInfo = ForbiddenPreconditionInfluenceInfo

Detailed Description

Common interface for precondition and postcondition operations.

Interface implemented by operations that can be targeted by a contract.

Interface implemented by operations that can be targeted by a loop invariant.

Common interface for postcondition operations (i.e., ensure_*).

Common interface for precondition operations (i.e., require_*).

This declares the MemoryEffectsOpInterface, which, like the cf.assert (MLIR cf dialect) and bool.assert (LLZK bool dialect) ops, adds a MemWrite affect to model program termination.

Targets are referenced by a label that implementations of this interface must provide.

Targets are referenced by name so implementations of this interface must also implement the Symbol interface.

Typedef Documentation

Influence

using llzk::verif::detail::Influence = ForbiddenPreconditionInfluence

Definition at line 113 of file ForbiddenPreconditionInfluence.h.

InfluenceInfo

using llzk::verif::detail::InfluenceInfo = ForbiddenPreconditionInfluenceInfo

Definition at line 114 of file ForbiddenPreconditionInfluence.h.