Update output to account for TGovernance

runtimeverification · Jun 12, 2024 · 986bb5a · 986bb5a
1 parent 78d538d
commit 986bb5a
Show file tree

Hide file tree

Showing 2 changed files with 118 additions and 91 deletions.
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
@@ -2977,6 +2977,25 @@ module S2KtestZModTEscrow-CONTRACT
     rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
 
 
+endmodule
+
+module S2KtestZModTGovernance-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KtestZModTGovernanceContract
+
+    syntax S2KtestZModTGovernanceContract ::= "S2KtestZModTGovernance" [symbol(""), klabel(contract_test%TGovernance)]
+
+    syntax Bytes ::= S2KtestZModTGovernanceContract "." S2KtestZModTGovernanceMethod [function, symbol(""), klabel(method_test%TGovernance)]
+
+    syntax S2KtestZModTGovernanceMethod ::= "S2KgetEscrowTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%TGovernance_S2KgetEscrowTokenTotalSupply_)]
+
+    rule  ( S2KtestZModTGovernance . S2KgetEscrowTokenTotalSupply ( ) => #abiCallData ( "getEscrowTokenTotalSupply" , .TypedArgs ) )
+
+
+    rule  ( selector ( "getEscrowTokenTotalSupply()" ) => 2061189261 )
+
+
 endmodule
 
 module S2KtestZModTToken-CONTRACT
@@ -10444,97 +10463,6 @@ module S2KtestZModSymbolicStore-CONTRACT
 
 endmodule
 
-module S2KlibZModforgeZSubstdZModsrcZModTest-CONTRACT
-    imports public FOUNDRY
-
-    syntax Contract ::= S2KlibZModforgeZSubstdZModsrcZModTestContract
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestContract ::= "S2KlibZModforgeZSubstdZModsrcZModTest" [symbol(""), klabel(contract_lib%forge-std%src%Test)]
-
-    syntax Bytes ::= S2KlibZModforgeZSubstdZModsrcZModTestContract "." S2KlibZModforgeZSubstdZModsrcZModTestMethod [function, symbol(""), klabel(method_lib%forge-std%src%Test)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KISZUndTEST_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KexcludeArtifacts_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KexcludeContracts_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KexcludeSenders_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2Kfailed" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2Kfailed_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetArtifactSelectors_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetArtifacts_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetContracts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetContracts_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetSelectors_)]
-
-    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetSenders" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetSenders_)]
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
-
-
-    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
-
-
-    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
-
-
-    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
-
-
-    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
-
-
-    rule  ( selector ( "excludeSenders()" ) => 517440284 )
-
-
-    rule  ( selector ( "failed()" ) => 3124842406 )
-
-
-    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
-
-
-    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
-
-
-    rule  ( selector ( "targetContracts()" ) => 1064470260 )
-
-
-    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
-
-
-    rule  ( selector ( "targetSenders()" ) => 1046363171 )
-
-
-endmodule
-
 module S2KsrcZModTestNumber-CONTRACT
     imports public FOUNDRY
 
@@ -14889,3 +14817,94 @@ module S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-CONTRACT
 
 
 endmodule
+
+module S2KlibZModforgeZSubstdZModsrcZModTest-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KlibZModforgeZSubstdZModsrcZModTestContract
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestContract ::= "S2KlibZModforgeZSubstdZModsrcZModTest" [symbol(""), klabel(contract_lib%forge-std%src%Test)]
+
+    syntax Bytes ::= S2KlibZModforgeZSubstdZModsrcZModTestContract "." S2KlibZModforgeZSubstdZModsrcZModTestMethod [function, symbol(""), klabel(method_lib%forge-std%src%Test)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KISZUndTEST_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KexcludeArtifacts_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KexcludeContracts_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KexcludeSenders_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2Kfailed" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2Kfailed_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetArtifactSelectors_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetArtifacts_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetContracts" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetContracts_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetSelectors_)]
+
+    syntax S2KlibZModforgeZSubstdZModsrcZModTestMethod ::= "S2KtargetSenders" "(" ")" [symbol(""), klabel(method_lib%forge-std%src%Test_S2KtargetSenders_)]
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KlibZModforgeZSubstdZModsrcZModTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
+
+
+    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
+
+
+    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
+
+
+    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
+
+
+    rule  ( selector ( "excludeSenders()" ) => 517440284 )
+
+
+    rule  ( selector ( "failed()" ) => 3124842406 )
+
+
+    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
+
+
+    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
+
+
+    rule  ( selector ( "targetContracts()" ) => 1064470260 )
+
+
+    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
+
+
+    rule  ( selector ( "targetSenders()" ) => 1046363171 )
+
+
+endmodule
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
@@ -38,6 +38,7 @@ module FOUNDRY-MAIN
     imports public S2KtestZModContractBTest-VERIFICATION
     imports public S2KtestZModContractFieldTest-VERIFICATION
     imports public S2KtestZModTEscrow-VERIFICATION
+    imports public S2KtestZModTGovernance-VERIFICATION
     imports public S2KtestZModTToken-VERIFICATION
     imports public S2KtestZModCounter-VERIFICATION
     imports public S2KtestZModCounterTest-VERIFICATION
@@ -377,6 +378,13 @@ module S2KtestZModTEscrow-VERIFICATION
 
 
 
+endmodule
+
+module S2KtestZModTGovernance-VERIFICATION
+    imports public S2KtestZModTGovernance-CONTRACT
+
+
+
 endmodule
 
 module S2KtestZModTToken-VERIFICATION