fix ALL summary

Certora · Mar 5, 2024 · 8bb92e1 · 8bb92e1
1 parent 03d71d9
commit 8bb92e1
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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;