llzk::verif::detail::IncludedContractSummary Struct Reference

Summary of all included-contract precondition failures under a specific caller binding. More...

#include <ForbiddenPreconditionInfluence.h>

Public Member Functions
	operator bool () const

Public Attributes
llvm::SmallVector< IncludedContractFailure >	failures

Detailed Description

Summary of all included-contract precondition failures under a specific caller binding.

The include verifier memoizes whether a contract remains valid when its entry arguments are seeded with the forbidden-influence classification of the corresponding verif.include operands. If failures occur, this structure records each offending callee precondition together with the merged influence information that caused it to become illegal.

Definition at line 173 of file ForbiddenPreconditionInfluence.h.

Member Function Documentation

operator bool()

llzk::verif::detail::IncludedContractSummary::operator bool ( ) const

inlineexplicit

Definition at line 176 of file ForbiddenPreconditionInfluence.h.

Member Data Documentation

failures

llvm::SmallVector<IncludedContractFailure> llzk::verif::detail::IncludedContractSummary::failures

Definition at line 174 of file ForbiddenPreconditionInfluence.h.

---

The documentation for this struct was generated from the following file:

• include/llzk/Dialect/Verif/Util/ForbiddenPreconditionInfluence.h