Cache key for one interprocedural included-contract summary query. More...

#include <ForbiddenPreconditionInfluence.h>

Collaboration diagram for llzk::verif::detail::IncludedContractSummaryKey:

Public Member Functions
bool	operator== (const IncludedContractSummaryKey &other) const

Public Attributes
mlir::Operation *	contract {}
llvm::SmallVector< InfluenceInfo >	argInfluences
InfluenceInfo	inheritedControlInfluence = InfluenceInfo::None()

Detailed Description

Cache key for one interprocedural included-contract summary query.

The analyzer memoizes included-contract failures by callee contract and the caller-provided forbidden-influence classification of each include operand. Reusing this key avoids re-analyzing the same included contract under identical argument influence assumptions.

Definition at line 185 of file ForbiddenPreconditionInfluence.h.