File tree Expand file tree Collapse file tree
CVLByExample/Summarization
Library/DirectSummary/certora/specs
MultiContract/certora/specs Expand file tree Collapse file tree Original file line number Diff line number Diff line change 55methods {
66 // functions declared in TestLibrary
77 function TestLibrary .calleeInternal () internal returns bool = > ALWAYS (true );
8- function _ .calleeExternal () external = > ALWAYS (true );
8+ function _ .calleeExternal () external = > ALWAYS (true ) ALL ;
99 // functions declared in IUnresolved
1010 function _ .calleeOverloadedInInterfaceExternal () external = > ALWAYS (true ) UNRESOLVED ;
1111 // functions from the contract Test .
Original file line number Diff line number Diff line change @@ -8,7 +8,7 @@ methods {
88 // A wildcard method entry may not specify return types in the method signature .
99 // The summarized functions belong to other contracts and therefore defined as `external` .
1010 // Functions of other contracts
11- function _ .summarizedByFunction () external = > summary () expect uint256 ;
11+ function _ .summarizedByFunction () external = > summary () expect uint256 ALL ;
1212 function _ .notSummarized () external optional envfree ;
1313 // functions of the main contract
1414 function callByFunctionInCalled1 () external returns (uint256 ) envfree ;
Original file line number Diff line number Diff line change 66 * /
77methods {
88 // should summarize both contract and lib functions
9- function _.funcWithStruct (CalledLibrary .S s ) external = > ALWAYS (1 );
9+ function _.funcWithStruct (CalledLibrary .S s ) external = > ALWAYS (1 ) ALL ;
1010
1111 // should summarize both contract and lib functions
12- function _ .funcWithEnum (CalledLibrary .E e ) external = > ALWAYS (4 );
12+ function _ .funcWithEnum (CalledLibrary .E e ) external = > ALWAYS (4 ) ALL ;
1313
1414 // should summarize only the lib function
15- function _ .funcWithStorage (uint [] storage s ) external = > ALWAYS (2 );
15+ function _ .funcWithStorage (uint [] storage s ) external = > ALWAYS (2 ) ALL ;
1616
1717 // should summarize only the contract function (in the context of a library , no location
1818 // means _not_ storage , so that shouldn 't be summarized here )
19- function _.funcWithStorage (uint [] s ) external = > ALWAYS (3 );
19+ function _.funcWithStorage (uint [] s ) external = > ALWAYS (3 ) ALL ;
2020
2121 function callLibFuncWithStruct (CalledLibrary .S s ) external returns (uint ) envfree ;
2222 function callLibFuncWithEnum (CalledLibrary .E e ) external returns (uint ) envfree ;
You can’t perform that action at this time.
0 commit comments