Summary | external | internal | ALL | UNRESOLVED | no link | with env |
---|---|---|---|---|---|---|
ALWAYS | always-external | always-internal | always-all | always-unresolved | ||
CVL function | (https://github.com/Certora/Examples/blob/bf3255766c28068eea2d0513edb8daca7bcaa206/CVLByExample/function-summary/multi-contract/certora/specs/spec_with_summary.spec#L6) | Not allowed | (https://github.com/Certora/Examples/blob/bf3255766c28068eea2d0513edb8daca7bcaa206/CVLByExample/function-summary/multi-contract/certora/specs/spec_with_summary.spec#L6) | |||
HAVOC_ECF | Not allowed | |||||
CONSTANT | (https://github.com/Certora/Examples/blob/8136b977cfe2fbf8e9e7ab0d74896cc62403fdb8/CVLByExample/function-summary/simple/certora/specs/ConstantVSNondet.spec#L5) | Not allowed | ||||
HAVOC_ALL | Not allowed | |||||
DISPATCHER | Not allowed | |||||
NONDET | ||||||
ghost summary | (https://github.com/Certora/Examples/blob/7a13d19cb450effac1b937115ca7b20c23f1ab74/CVLByExample/function-summary/ghost-summary/certora/specs/WithGhostSummary.spec#L3) |