Skip to content

Commit fc25381

Browse files
Add dsvalue-peek-pass-rough to generate-regression-tests.sh (#2911)
* Add dsvalue-peek-pass-rough to generate-regression-tests.sh * Add test updated by script * Regenerate other tests * Empty commit
1 parent 82b8a19 commit fc25381

File tree

53 files changed

+32712
-32565
lines changed

Some content is hidden

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

53 files changed

+32712
-32565
lines changed

scripts/generate-regression-tests.sh

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,9 @@ generate-evm() {
9797
kollect test-addu48u48 \
9898
make tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k.prove -s -e
9999

100+
kollect test-dsvalue-peek-pass-rough \
101+
make tests/specs/mcd/dsvalue-peek-pass-rough-spec.k.prove -s -e
102+
100103
$KORE/scripts/trim-source-paths.sh *.kore
101104
}
102105

test/regression-evm/test-add0-definition.kore

Lines changed: 1119 additions & 1119 deletions
Large diffs are not rendered by default.

test/regression-evm/test-add0.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
#!/bin/sh
2-
${KORE_EXEC:?} test-add0-definition.kore --module ETHEREUM-SIMULATION --pattern test-add0-tmp.in.ozJ1bLKeAD "$@"
2+
${KORE_EXEC:?} test-add0-definition.kore --module ETHEREUM-SIMULATION --pattern test-add0-tmp.in.J7FM3boJ8J "$@"

test/regression-evm/test-addu48u48-vdefinition.kore

Lines changed: 2443 additions & 2407 deletions
Large diffs are not rendered by default.

test/regression-evm/test-and0-definition.kore

Lines changed: 1119 additions & 1119 deletions
Large diffs are not rendered by default.

test/regression-evm/test-and0.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
#!/bin/sh
2-
${KORE_EXEC:?} test-and0-definition.kore --module ETHEREUM-SIMULATION --pattern test-and0-tmp.in.5W1kabbm5u "$@"
2+
${KORE_EXEC:?} test-and0-definition.kore --module ETHEREUM-SIMULATION --pattern test-and0-tmp.in.SS2aOReh2B "$@"

test/regression-evm/test-branching-invalid-definition.kore

Lines changed: 1119 additions & 1119 deletions
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)