llzk::verif::detail::IncludedContractFailure Struct Reference

One included precondition that becomes illegal under a specific caller binding. More...

#include <ForbiddenPreconditionInfluence.h>

Collaboration diagram for llzk::verif::detail::IncludedContractFailure:

Public Attributes
std::optional< mlir::Location >	preconditionLoc = std::nullopt
InfluenceInfo	influenceInfo = InfluenceInfo::None()

Detailed Description

One included precondition that becomes illegal under a specific caller binding.

The include verifier tracks each failing nested precondition separately so a single verif.include diagnostic can report every included require_* that becomes illegal under the caller's operand binding.

Definition at line 160 of file ForbiddenPreconditionInfluence.h.

Member Data Documentation

influenceInfo

InfluenceInfo llzk::verif::detail::IncludedContractFailure::influenceInfo = InfluenceInfo::None()

Definition at line 162 of file ForbiddenPreconditionInfluence.h.

preconditionLoc

std::optional<mlir::Location> llzk::verif::detail::IncludedContractFailure::preconditionLoc = std::nullopt

Definition at line 161 of file ForbiddenPreconditionInfluence.h.

---

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

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