From 8bb92e13ce87270030d2a2e3c12ba4ce4191b350 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Tue, 5 Mar 2024 10:44:45 +0200 Subject: [PATCH] fix ALL summary --- .../Library/DirectSummary/certora/specs/AllDirect.spec | 2 +- .../MultiContract/certora/specs/FunctionSummary.spec | 2 +- .../UserDefinedReturnType/LibraryVSContractSummary.spec | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec b/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec index 934a7707..45f0aaaa 100644 --- a/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec +++ b/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec @@ -5,7 +5,7 @@ methods { // functions declared in TestLibrary function TestLibrary.calleeInternal() internal returns bool => ALWAYS(true); - function _.calleeExternal() external => ALWAYS(true); + function _.calleeExternal() external => ALWAYS(true) ALL; // functions declared in IUnresolved function _.calleeOverloadedInInterfaceExternal() external => ALWAYS(true) UNRESOLVED; // functions from the contract Test. diff --git a/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec b/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec index f5f05b22..cd898871 100644 --- a/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec +++ b/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec @@ -8,7 +8,7 @@ methods { // A wildcard method entry may not specify return types in the method signature. // The summarized functions belong to other contracts and therefore defined as `external`. // Functions of other contracts - function _.summarizedByFunction() external => summary() expect uint256; + function _.summarizedByFunction() external => summary() expect uint256 ALL; function _.notSummarized() external optional envfree; // functions of the main contract function callByFunctionInCalled1() external returns(uint256) envfree; diff --git a/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec b/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec index 7358ed84..d8204266 100644 --- a/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec +++ b/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec @@ -6,17 +6,17 @@ */ methods { // should summarize both contract and lib functions - function _.funcWithStruct(CalledLibrary.S s) external => ALWAYS(1); + function _.funcWithStruct(CalledLibrary.S s) external => ALWAYS(1) ALL; // should summarize both contract and lib functions - function _.funcWithEnum(CalledLibrary.E e) external => ALWAYS(4); + function _.funcWithEnum(CalledLibrary.E e) external => ALWAYS(4) ALL; // should summarize only the lib function - function _.funcWithStorage(uint[] storage s) external => ALWAYS(2); + function _.funcWithStorage(uint[] storage s) external => ALWAYS(2) ALL; // should summarize only the contract function (in the context of a library, no location // means _not_ storage, so that shouldn't be summarized here) - function _.funcWithStorage(uint[] s) external => ALWAYS(3); + function _.funcWithStorage(uint[] s) external => ALWAYS(3) ALL; function callLibFuncWithStruct(CalledLibrary.S s) external returns (uint) envfree; function callLibFuncWithEnum(CalledLibrary.E e) external returns (uint) envfree;