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

Commit caadb9e

Browse files
nwatson22nwatson22
committed
Merge master into noah/node-attributes
2 parents 7d55264 + 8336f52 commit caadb9e

File tree

97 files changed

+890
-271
lines changed

Some content is hidden

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

97 files changed

+890
-271
lines changed

‎deps/k_release

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
6.3.45
1+
6.3.50

‎docs/conf.py

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@
99
project = 'pyk'
1010
author = 'Runtime Verification, Inc'
1111
copyright = '2024, Runtime Verification, Inc'
12-
version = '0.1.724'
13-
release = '0.1.724'
12+
version = '0.1.728'
13+
release = '0.1.728'
1414

1515
# -- General configuration ---------------------------------------------------
1616
# https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

‎package/version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.724
1+
0.1.728

‎pyproject.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "pyk"
7-
version = "0.1.724"
7+
version = "0.1.728"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,4 @@
1-
[Error] Critical: Only one main parameter allowed but found several: "--badflag" and "--extra"
1+
usage: pyk [-h]
2+
{print,rpc-print,rpc-kast,prove-legacy,kompile,run,prove,graph-imports,coverage,kore-to-json,json-to-kore}
3+
...
4+
pyk: error: unrecognized arguments: --badflag --extra ---output-definition test-kompiled

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

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,15 @@
1-
[Error] Critical: You have to provide exactly one main file in order to do
2-
outer parsing.
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]
13+
[--llvm-proof-hint-instrumentation]
14+
main_file
15+
pyk kompile: error: the following arguments are required: main_file

‎regression-new/boundary-cells-opt/bc-none/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ KOMPILE_BACKEND?=haskell
88

99
KPROVE_FLAGS=
1010

11-
include ../../../../include/kframework/ktest.mak
11+
include ../../include/ktest.mak

‎regression-new/cell-bag-sort-llvm/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
-KOMPILE_FLAGS=-w none
1+
KOMPILE_FLAGS=-w none
22

33
include ../include/ktest-fail.mak

‎regression-new/equals-pattern/1.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
true ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
true ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/2.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
false ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
false ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/3.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
true ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
true ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/4.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
false ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
false ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/5.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
true ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
true ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/6.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
true ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
true ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/7.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
false ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
false ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/8.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
bar ( 2 ) ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
bar ( 2 ) ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/equals-pattern/9.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
10 ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
10 ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/include/ktest-fail.mak

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,11 @@ TESTS?=$(wildcard $(DEFDIR)/*.md) $(wildcard $(DEFDIR)/*.k)
1515
KOMPILE_BACKEND?=llvm
1616
KAST_TESTS?=$(wildcard ./*.kast)
1717

18-
KOMPILE_FLAGS+=--type-inference-mode checked
19-
KPROVE_FLAGS+=
20-
KRUN_FLAGS+=
18+
VERBOSITY?=
19+
20+
KOMPILE_FLAGS+=--type-inference-mode checked $(VERBOSITY)
21+
KPROVE_FLAGS+=$(VERBOSITY)
22+
KRUN_FLAGS+=$(VERBOSITY)
2123

2224
CHECK=| diff -
2325

‎regression-new/include/ktest.mak

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ DEFDIR?=.
3535
# path to kompile output directory
3636
KOMPILED_DIR=$(DEFDIR)/$(notdir $(DEF))-kompiled
3737
# all tests in test directory with matching file extension
38-
RUN_TESTS?=$(wildcard $(TESTDIR)/*.$(EXT))
38+
RUN_TESTS?=$(wildcard $(TESTDIR)/*.$(EXT)) $(wildcard $(TESTDIR)/krun.nopgm)
3939
PROOF_TESTS?=$(wildcard $(TESTDIR)/*-spec.k) $(wildcard $(TESTDIR)/*-spec.md)
4040
SEARCH_TESTS?=$(wildcard $(TESTDIR)/*.$(EXT).search)
4141
STRAT_TESTS?=$(wildcard $(TESTDIR)/*.strat)
@@ -55,7 +55,7 @@ ifeq ($(UNAME), Darwin)
5555
endif
5656

5757
KOMPILE_FLAGS+=--type-inference-mode checked $(VERBOSITY)
58-
KRUN_FLAGS+=
58+
KRUN_FLAGS+=$(VERBOSITY)
5959
KPROVE_FLAGS+=--type-inference-mode checked --failure-info $(VERBOSITY)
6060

6161
CHECK?=| diff -

‎regression-new/issue-1789-rhsOr/haskell/0.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
-1 ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
-1 ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/issue-1789-rhsOr/haskell/1.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
1 ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
1 ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/issue-1789-rhsOr/haskell/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ EXT=test
33
TESTDIR=.
44
KOMPILE_BACKEND=haskell
55

6-
include ../../../../include/kframework/ktest.mak
6+
include ../../include/ktest.mak

‎regression-new/issue-1789-rhsOr/llvm/1.test.out

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,7 @@
55
<foo>
66
bar ~> .K
77
</foo>
8+
<generatedCounter>
9+
0
10+
</generatedCounter>
811
</generatedTop>

‎regression-new/issue-1789-rhsOr/llvm/2.test.out

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,7 @@
55
<foo>
66
baz ~> .K
77
</foo>
8+
<generatedCounter>
9+
0
10+
</generatedCounter>
811
</generatedTop>

‎regression-new/issue-1789-rhsOr/llvm/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ EXT=test
33
TESTDIR=.
44
KOMPILE_BACKEND=llvm
55

6-
include ../../../../include/kframework/ktest.mak
6+
include ../../include/ktest.mak

‎regression-new/issue-1844-noPGM/haskell/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ TESTDIR=.
44
KOMPILE_BACKEND=haskell
55
KOMPILE_FLAGS=--syntax-module TEST
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak

‎regression-new/issue-1844-noPGM/llvm/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ TESTDIR=.
44
KOMPILE_BACKEND=llvm
55
KOMPILE_FLAGS=--syntax-module TEST
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak

‎regression-new/issue-1879-kproveTrans/haskell/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,4 @@ DEF=test
22
TESTDIR=.
33
KOMPILE_BACKEND=haskell
44

5-
include ../../../../include/kframework/ktest.mak
5+
include ../../include/ktest.mak

‎regression-new/issue-1879-kproveTrans/haskell/test-spec.k.out

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,13 @@
1-
#Top
1+
APRProof: b516126047d751393af42ed88cfb13e114e1e924642c335f728abb5cf8246383
2+
status: ProofStatus.PASSED
3+
admitted: False
4+
nodes: 3
5+
pending: 0
6+
failing: 0
7+
vacuous: 0
8+
stuck: 0
9+
terminal: 0
10+
refuted: 0
11+
bounded: 0
12+
execution time: 0s
13+
Subproofs: 0

‎regression-new/issue-2812-kprove-filter-claims/claims/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ KOMPILE_BACKEND=haskell
44
TESTDIR=.
55
KPROVE_FLAGS+=--claims VERIFICATION.s1
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak
88

99
CONSIDER_PROVER_ERRORS=2>&1

‎regression-new/issue-2812-kprove-filter-claims/exclude/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ KOMPILE_BACKEND=haskell
44
TESTDIR=.
55
KPROVE_FLAGS+=--exclude VERIFICATION.fail1 --exclude VERIFICATION.fail2
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak
88

99
CONSIDER_PROVER_ERRORS=2>&1

‎regression-new/issue-2812-kprove-filter-claims/trusted/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ KOMPILE_BACKEND=haskell
44
TESTDIR=.
55
KPROVE_FLAGS+=--trusted VERIFICATION.s1
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak
88

99
CONSIDER_PROVER_ERRORS=2>&1

‎regression-new/issue-2909-allow-anywhere-haskell/haskell/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ TESTDIR=.
44
KOMPILE_BACKEND=haskell
55
KOMPILE_FLAGS=--syntax-module TEST --allow-anywhere-haskell -w none
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak

‎regression-new/issue-2909-allow-anywhere-haskell/llvm/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ TESTDIR=.
44
KOMPILE_BACKEND=llvm
55
KOMPILE_FLAGS=--syntax-module TEST --allow-anywhere-haskell -w none
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak

‎regression-new/issue-3035-antileft/haskell/1.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
bar ( ) ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
bar ( ) ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/issue-3035-antileft/haskell/2.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
baz ( ) ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
baz ( ) ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/issue-3035-antileft/haskell/3.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
foo ( -10 ) ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
foo ( -10 ) ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/issue-3035-antileft/haskell/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ TESTDIR=.
44
KOMPILE_BACKEND=haskell
55
KOMPILE_FLAGS=--syntax-module TEST
66

7-
include ../../../../include/kframework/ktest.mak
7+
include ../../include/ktest.mak

‎regression-new/issue-3035-antileft/llvm/1.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
bar ( ) ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
bar ( ) ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

‎regression-new/issue-3035-antileft/llvm/2.test.out

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
<k>
2-
baz ( ) ~> .K
3-
</k>
1+
<generatedTop>
2+
<k>
3+
baz ( ) ~> .K
4+
</k>
5+
<generatedCounter>
6+
0
7+
</generatedCounter>
8+
</generatedTop>

0 commit comments

Comments
 (0)