llzk::verif::detail Namespace Reference

Classes
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	RequireComputeOpGenericAdaptorBase
class	RequireConstrainOpGenericAdaptorBase
class	StepOpGenericAdaptorBase
class	StepYieldOpGenericAdaptorBase
class	VerifAssertOpGenericAdaptorBase
class	VerifProveOpGenericAdaptorBase
class	VerifSMTProveOpGenericAdaptorBase

Typedefs
using	Influence = ForbiddenPreconditionInfluence
using	InfluenceInfo = ForbiddenPreconditionInfluenceInfo

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.