Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Commit e4e58e7

Browse files
ehildenbehildenb
committed
!!! regression-new: update all expected output
1 parent a71f988 commit e4e58e7

File tree

281 files changed

+9783
-3408
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

281 files changed

+9783
-3408
lines changed

‎regression-new/bad-flags/no-flags.out‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
1-
usage: pyk kompile [-h] [--verbose] [--debug] [--warnings WARNINGS] [-w2e] [-I INCLUDES]
2-
[--main-module MAIN_MODULE] [--syntax-module SYNTAX_MODULE]
3-
[--md-selector MD_SELECTOR] [--output-definition DEFINITION_DIR] [--backend BACKEND]
4-
[--type-inference-mode TYPE_INFERENCE_MODE] [--emit-json] [-ccopt CCOPTS]
5-
[--no-llvm-kompile] [--with-llvm-library] [--enable-llvm-debug]
6-
[--llvm-kompile-type LLVM_KOMPILE_TYPE] [--llvm-kompile-output LLVM_KOMPILE_OUTPUT]
7-
[--read-only-kompiled-directory] [-O0] [-O1] [-O2] [-O3] [--enable-search]
8-
[--coverage] [--gen-bison-parser] [--gen-glr-bison-parser] [--bison-lists]
1+
usage: pyk kompile [-h] [--verbose] [--debug] [--warnings WARNINGS] [-w2e]
2+
[-I INCLUDES] [--main-module MAIN_MODULE]
3+
[--syntax-module SYNTAX_MODULE] [--md-selector MD_SELECTOR]
4+
[--output-definition DEFINITION_DIR] [--backend BACKEND]
5+
[--type-inference-mode TYPE_INFERENCE_MODE] [--emit-json]
6+
[-ccopt CCOPTS] [--no-llvm-kompile] [--with-llvm-library]
7+
[--enable-llvm-debug]
8+
[--llvm-kompile-type LLVM_KOMPILE_TYPE]
9+
[--llvm-kompile-output LLVM_KOMPILE_OUTPUT]
10+
[--read-only-kompiled-directory] [-O0] [-O1] [-O2] [-O3]
11+
[--enable-search] [--coverage] [--gen-bison-parser]
12+
[--gen-glr-bison-parser] [--bison-lists]
913
[--llvm-proof-hint-instrumentation] [--no-exc-wrap]
1014
main_file
1115
pyk kompile: error: the following arguments are required: main_file

‎regression-new/cell-sort-haskell/1.test.out‎

Lines changed: 38 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,38 @@
1-
<T>
2-
<k>
3-
"done" ~> .K
4-
</k>
5-
<nextFunction>
6-
3
7-
</nextFunction>
8-
<functions>
9-
<function>
10-
<fId>
11-
0
12-
</fId>
13-
</function> <function>
14-
<fId>
15-
1
16-
</fId>
17-
</function> <function>
18-
<fId>
19-
2
20-
</fId>
21-
</function>
22-
</functions>
23-
<contracts>
24-
<contract>
25-
<cName>
26-
foo ~> .K
27-
</cName>
28-
<cFunctions>
29-
f1 |-> 0
30-
f2 |-> 1
31-
f3 |-> 2
32-
</cFunctions>
33-
</contract>
34-
</contracts>
35-
</T>
1+
<generatedTop>
2+
<T>
3+
<k>
4+
"done" ~> .K
5+
</k>
6+
<nextFunction>
7+
3
8+
</nextFunction>
9+
<functions>
10+
<function>
11+
<fId>
12+
0
13+
</fId>
14+
</function> <function>
15+
<fId>
16+
2
17+
</fId>
18+
</function> <function>
19+
<fId>
20+
1
21+
</fId>
22+
</function>
23+
</functions>
24+
<contracts>
25+
<contract>
26+
<cName>
27+
foo ~> .K
28+
</cName>
29+
<cFunctions>
30+
f1 |-> 0 f3 |-> 2 f2 |-> 1
31+
</cFunctions>
32+
</contract>
33+
</contracts>
34+
</T>
35+
<generatedCounter>
36+
0
37+
</generatedCounter>
38+
</generatedTop>

‎regression-new/checkClaimError/rule-spec.k.out‎

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,33 @@
1-
[Error] Compiler: Only claims and simplification rules are allowed in proof modules.
1+
[Error] Compiler: Only claims and simplification rules are allowed in proof
2+
modules.
23
Source(rule-spec.k)
34
Location(6,10,6,43)
45
6 | rule <k> doIt(foo) => doIt(0) ... </k>
56
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
67
[Error] Compiler: Had 1 structural errors.
8+
Traceback (most recent call last):
9+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 105, in _kprove
10+
return run_process(run_args, logger=_LOGGER, env=env, check=check)
11+
File "/home/dev/src/pyk/src/pyk/utils.py", line 451, in run_process
12+
res.check_returncode()
13+
File "/usr/lib/python3.10/subprocess.py", line 457, in check_returncode
14+
raise CalledProcessError(self.returncode, self.args, self.stdout,
15+
subprocess.CalledProcessError: Command '('kprove', 'rule-spec.k', '--definition', 'errorClaim-kompiled', '--output', 'json', '--type-inference-mode', 'checked', '--dry-run', '--emit-json-spec', '/tmp/tmppacrxgx1')' returned non-zero exit status 113.
16+
17+
The above exception was the direct cause of the following exception:
18+
19+
Traceback (most recent call last):
20+
File "<string>", line 1, in <module>
21+
File "/home/dev/src/pyk/src/pyk/__main__.py", line 90, in main
22+
execute(options)
23+
File "/home/dev/src/pyk/src/pyk/__main__.py", line 252, in exec_prove
24+
proofs = kprove.prove_rpc(options=options)
25+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 380, in prove_rpc
26+
all_claims = self.get_claims(
27+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 425, in get_claims
28+
flat_module_list = self.get_claim_modules(
29+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 400, in get_claim_modules
30+
_kprove(
31+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 107, in _kprove
32+
raise RuntimeError(
33+
RuntimeError: ('Command kprove exited with code 113 for: rule-spec.k', '', None)

‎regression-new/checkClaimError/syntax-spec.k.out‎

Lines changed: 30 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,39 @@
1-
[Error] Compiler: Found syntax declaration in proof module. Only tokens for existing sorts are allowed.
1+
[Error] Compiler: Found syntax declaration in proof module. Only tokens for
2+
existing sorts are allowed.
23
Source(syntax-spec.k)
34
Location(6,18,6,29)
45
6 | syntax X ::= "errorHere"
56
. ^~~~~~~~~~~
6-
[Error] Compiler: Found syntax declaration in proof module. Only tokens for existing sorts are allowed.
7+
[Error] Compiler: Found syntax declaration in proof module. Only tokens for
8+
existing sorts are allowed.
79
Source(syntax-spec.k)
810
Location(7,5,7,13)
911
7 | syntax Y
1012
. ^~~~~~~~
1113
[Error] Compiler: Had 2 structural errors.
14+
Traceback (most recent call last):
15+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 105, in _kprove
16+
return run_process(run_args, logger=_LOGGER, env=env, check=check)
17+
File "/home/dev/src/pyk/src/pyk/utils.py", line 451, in run_process
18+
res.check_returncode()
19+
File "/usr/lib/python3.10/subprocess.py", line 457, in check_returncode
20+
raise CalledProcessError(self.returncode, self.args, self.stdout,
21+
subprocess.CalledProcessError: Command '('kprove', 'syntax-spec.k', '--definition', 'errorClaim-kompiled', '--output', 'json', '--type-inference-mode', 'checked', '--dry-run', '--emit-json-spec', '/tmp/tmp2z_mabgd')' returned non-zero exit status 113.
22+
23+
The above exception was the direct cause of the following exception:
24+
25+
Traceback (most recent call last):
26+
File "<string>", line 1, in <module>
27+
File "/home/dev/src/pyk/src/pyk/__main__.py", line 90, in main
28+
execute(options)
29+
File "/home/dev/src/pyk/src/pyk/__main__.py", line 252, in exec_prove
30+
proofs = kprove.prove_rpc(options=options)
31+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 380, in prove_rpc
32+
all_claims = self.get_claims(
33+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 425, in get_claims
34+
flat_module_list = self.get_claim_modules(
35+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 400, in get_claim_modules
36+
_kprove(
37+
File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 107, in _kprove
38+
raise RuntimeError(
39+
RuntimeError: ('Command kprove exited with code 113 for: syntax-spec.k', '', None)

‎regression-new/checks/checkCircularList.k.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
[Error] Compiler: Had 1 parsing errors.
2-
[Error] Compiler: Illegal circular relation: Exp < ExpList < Exp
2+
[Error] Compiler: Illegal circular relation: ExpList < Exp < ExpList
33
[ERROR] Running process failed with returncode 113:
44
kompile checkCircularList.k --md-selector k --emit-json --warnings none --no-exc-wrap --backend llvm --output-definition checkCircularList-kompiled --type-inference-mode checked

‎regression-new/checks/existentialCheck.k.out‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
[Error] Compiler: Claims are not allowed in the definition.
22
Source(existentialCheck.k)
3-
Location(15,9,15,29)
3+
Location(15,9,15,30)
44
15 | claim <k> ?X:Int => .K </k>
5-
. ^~~~~~~~~~~~~~~~~~~~
5+
. ^~~~~~~~~~~~~~~~~~~~~
66
[Error] Compiler: Existential variable ?X found in LHS. Existential variables are only allowed in the RHS.
77
Source(existentialCheck.k)
88
Location(15,13,15,15)

‎regression-new/checks/macroWithFunction.k.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@
66
[Error] Compiler: Had 1 structural errors after macro expansion.
77
while executing phase "expand macros" on sentence at
88
Source(macroWithFunction.k)
9-
Location(23,10,23,37)
9+
Location(23,10,23,38)
1010
[ERROR] Running process failed with returncode 113:
1111
kompile macroWithFunction.k --md-selector k --emit-json --warnings none --no-exc-wrap --backend llvm --output-definition macroWithFunction-kompiled --type-inference-mode checked

‎regression-new/checks/priorityError.k.out‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,22 @@
11
[Error] Inner Parser: Priority filter exception. Cannot use lguard as an immediate child of plus. Consider using parentheses around lguard
22
Source(priorityError.k)
3-
Location(21,19,21,22)
3+
Location(21,20,21,23)
44
21 | rule .K => 1 + l 2 // unable to disambiguate - error
5-
. ^~~
5+
. ^~~
66
[Error] Inner Parser: Priority filter exception. Cannot use rguard as an immediate child of plus. Consider using parentheses around rguard
77
Source(priorityError.k)
8-
Location(22,15,22,18)
8+
Location(22,16,22,19)
99
22 | rule .K => 1 r + 2 // unable to disambiguate - error
10-
. ^~~
10+
. ^~~
1111
[Error] Inner Parser: Parsing ambiguity.
1212
1: syntax Exp ::= "l" Exp [klabel(lguard), symbol]
1313
lguard(rguard(#token("1","Int")))
1414
2: syntax Exp ::= Exp "r" [klabel(rguard), symbol]
1515
rguard(lguard(#token("1","Int")))
1616
Source(priorityError.k)
17-
Location(23,15,23,20)
17+
Location(23,16,23,21)
1818
23 | rule .K => l 1 r // ambiguous - error
19-
. ^~~~~
19+
. ^~~~~
2020
[Error] Compiler: Had 3 parsing errors.
2121
[ERROR] Running process failed with returncode 113:
2222
kompile priorityError.k --md-selector k --emit-json --warnings none --no-exc-wrap --backend llvm --output-definition priorityError-kompiled --type-inference-mode checked

‎regression-new/concrete-function-cache/a2-spec.k.out‎

Lines changed: 27 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,27 @@
1-
kore-exec: [] Warning (WarnStuckClaimState):
2-
The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: a2-spec.k:7:1-8:18
3-
Context:
4-
(InfoReachability) while checking the implication
5-
#Ceil ( bar ( X ) )
6-
#And
7-
#Not ( #Ceil ( baz ( X ) )
8-
#And
9-
{
10-
bar ( X )
11-
#Equals
12-
baz ( X )
13-
} )
14-
#And
15-
<k>
16-
end ( bar ( X ) ) ~> .K
17-
</k>
18-
#And
19-
{
20-
true
21-
#Equals
22-
X <Int 0
23-
}
24-
[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
1+
APRProof: A2-SPEC.s2
2+
status: ProofStatus.FAILED
3+
admitted: False
4+
nodes: 5
5+
pending: 0
6+
failing: 1
7+
vacuous: 0
8+
stuck: 1
9+
terminal: 0
10+
refuted: 0
11+
bounded: 0
12+
execution time: 0s
13+
Subproofs: 0
14+
1 Failure nodes. (0 pending and 1 failing)
15+
16+
Failing nodes:
17+
18+
Node id: 5
19+
Failure reason:
20+
Matching failed.
21+
The following cells failed matching individually (antecedent #Implies consequent):
22+
K_CELL: end ( bar ( X:Int ) ) #Implies end ( baz ( X:Int ) )
23+
Path condition:
24+
#Ceil ( bar ( X:Int ) )
25+
Failed to generate a model.
26+
27+
Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN

‎regression-new/concrete-function/a1-spec.k.out‎

Lines changed: 27 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,27 @@
1-
kore-exec: [] Warning (WarnStuckClaimState):
2-
The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: a1-spec.k:7:1-8:18
3-
Context:
4-
(InfoReachability) while checking the implication
5-
#Ceil ( barConcrete ( X ) )
6-
#And
7-
#Not ( #Ceil ( baz ( X ) )
8-
#And
9-
{
10-
barConcrete ( X )
11-
#Equals
12-
baz ( X )
13-
} )
14-
#And
15-
<k>
16-
end ( barConcrete ( X ) ) ~> .K
17-
</k>
18-
#And
19-
{
20-
true
21-
#Equals
22-
X >Int 0
23-
}
24-
[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
1+
APRProof: A1-SPEC.s1
2+
status: ProofStatus.FAILED
3+
admitted: False
4+
nodes: 5
5+
pending: 0
6+
failing: 1
7+
vacuous: 0
8+
stuck: 1
9+
terminal: 0
10+
refuted: 0
11+
bounded: 0
12+
execution time: 0s
13+
Subproofs: 0
14+
1 Failure nodes. (0 pending and 1 failing)
15+
16+
Failing nodes:
17+
18+
Node id: 5
19+
Failure reason:
20+
Matching failed.
21+
The following cells failed matching individually (antecedent #Implies consequent):
22+
K_CELL: end ( barConcrete ( X:Int ) ) #Implies end ( baz ( X:Int ) )
23+
Path condition:
24+
#Ceil ( barConcrete ( X:Int ) )
25+
Failed to generate a model.
26+
27+
Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN

0 commit comments

Comments
 (0)