key icon indicating copy to clipboard operation
key copied to clipboard
verified publisher icon KeYProject

Not all KeY files in repo are parsable.

Open wadoon opened this issue 8 months ago • 5 comments

The follwing KeY files are currently not parsable.

How should we proceed? Fixing them or removing them?

This came up due to the automatic rewriting of the settings.

File: ../key.core/src/test/resources/testcase/smt/tacletTranslation/castOperators.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testAnonymous1.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testAnonymous2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion10.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion11.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion3.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion4.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion5.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion6.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion7.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion8.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testDeletion9.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testHeapDependent1.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testHeapDependent2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testLocationFunction1.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testLocationFunction2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testLocationFunction3.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testQuantified1.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testQuantified2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testQuantified3.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testQuantified4.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testQuantified5.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testShadowOnShadowDiffNr.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testShadowOnShadowSameNr.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testShadowedArrayRule1.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testShadowedArrayRule2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testShadowedAttributeRule1.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updatesimplification/testShadowedAttributeRule2.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/updateterm/updatetermTest3.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/testcase/parserErrorTest/missing_semicolon.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/delayed_error.key -- SKIPPED (origin not parsable).
File: ../key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/missing_semicolon.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/smt/tacletTranslation/castOperators.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testAnonymous1.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testAnonymous2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion10.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion11.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion3.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion4.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion5.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion6.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion7.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion8.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testDeletion9.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testHeapDependent1.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testHeapDependent2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testLocationFunction1.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testLocationFunction2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testLocationFunction3.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testQuantified1.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testQuantified2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testQuantified3.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testQuantified4.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testQuantified5.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testShadowOnShadowDiffNr.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testShadowOnShadowSameNr.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testShadowedArrayRule1.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testShadowedArrayRule2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testShadowedAttributeRule1.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updatesimplification/testShadowedAttributeRule2.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/updateterm/updatetermTest3.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/testcase/parserErrorTest/missing_semicolon.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/de/uka/ilkd/key/nparser/exceptional/delayed_error.key -- SKIPPED (origin not parsable).
File: ../key.core/build/resources/test/de/uka/ilkd/key/nparser/exceptional/missing_semicolon.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/java_dl/anonymousUpdateOnNonrigidTerm.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/java_dl/equivalentUpdates.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/java_dl/examDB/examDB.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/java_dl/payCardOCL/paycard.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/BookExamples/10UsingKeY/Bank-JML/bankjml.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/adt/dt_nat.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/arith/gemplusDecimal/mul.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/reachable/getLast.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/reachable/getLast.key.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/reachable/reachtest.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_contains_ensuresPost_id4.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_contains_respectsMod_id3.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_contains_respectsMod_id4.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_insert_ensuresPost_id1.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_insert_ensuresPost_id2.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_insert_preservesInv.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_insert_respectsMod_id0.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_insert_respectsMod_id1.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example1_insert_respectsMod_id2.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example2_1.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/Case_Studies/example2_1_incomplete.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/charAtSubstring.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/lengthConcat.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/lengthNEq1.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/lengthNEq2.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/lengthReplace.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/lengthSubstring.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/charAtConcat.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/concatConcat.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/concatEqLeft.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/consEq.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/length0.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/lengthGeq0.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/replaceConcat.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/replaceSubstring.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/substringConcat.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/strings/proofs/substringSubstring.proof -- SKIPPED (origin not parsable).
File: ../key.ui/examples/standard_key/taclet_po/testPO6.key -- SKIPPED (origin not parsable).
File: ../key.ui/examples/theories/binaryTree.key -- SKIPPED (origin not parsable).

wadoon avatar May 10 '25 12:05 wadoon

Cannot be parsed before the rewrite or after?

mattulbrich avatar May 11 '25 18:05 mattulbrich

Cannot be parsed before the rewrite or after?

Before the rewrite. Otherwise, I would know that I am the problem.

wadoon avatar May 11 '25 18:05 wadoon

For example, some KeY files use \nonRigid in \functions {...}, which is not allowed anymore.

wadoon avatar May 11 '25 18:05 wadoon

Concerning the nonRigid modifier. I want to submit a PR soon that reenables that modifier at least for predicates (also I think here the modifier is allowed but not passed through to the constructor anymore) as it useful for some other branches (like dependency reasoning etc.) :-)

unp1 avatar May 13 '25 09:05 unp1

The main question behind this story is: Should we keep everything inside the repo up-to-date with software features?

If not so, we should at least mark (put a comment) in files, that are outdated.

wadoon avatar May 13 '25 10:05 wadoon