Skip to content

Rewriting the settings in KeY files to the new format. #3688

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wadoon wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

Rewriting the settings in KeY files to the new format. #3688

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
503883e
A tool for rewriting the settings in KeY files to the new JSON-like f…
wadoon Apr 6, 2025
679d5d7
move into script folder finishing
wadoon Nov 22, 2025
bf146b1
added gzip support
wadoon Nov 22, 2025
1e09b38
using logger, force flag
wadoon Nov 22, 2025
b9b778c
application of #3590
wadoon Nov 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
6 changes: 5 additions & 1 deletion key.core/src/main/antlr4/KeYLexer.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,10 @@ lexer grammar KeYLexer;
}

private Token tokenBackStorage = null;
private boolean proofIsEOF = true;
public void setProofIsEOF(boolean b) { proofIsEOF = b;}
public boolean isProofIsEOF() { return proofIsEOF;}

@Override
public void emit(Token token) {
int MAX_K = 10;
Expand All @@ -51,7 +55,7 @@ lexer grammar KeYLexer;
break;
}
}
if(token.getType() == PROOF) {
if(token.getType() == PROOF && isProofIsEOF()) {
tokenBackStorage = super.emitEOF();
//will later be overwritten the EOF token
}
Expand Down
12 changes: 8 additions & 4 deletions key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -466,6 +466,10 @@ public ConfigurationWriter printIndent() {
}

public ConfigurationWriter printComment(String comment) {
if (comment == null || comment.isBlank()) {
return this;
}

if (comment.contains("\n")) {
out.format("/* %s */\n", comment);
} else {
Expand Down Expand Up @@ -509,7 +513,7 @@ public ConfigurationWriter printValue(Object value) {
}

private ConfigurationWriter printMap(Map<?, ?> value) {
out.format("{ ");
out.format("{");
indent += 4;
newline().printIndent();
for (Iterator<? extends Map.Entry<?, ?>> iterator =
Expand All @@ -525,7 +529,7 @@ private ConfigurationWriter printMap(Map<?, ?> value) {
}
indent -= 4;
newline().printIndent();
out.format(" }");
out.format("}");
return this;
}

Expand All @@ -536,7 +540,7 @@ private ConfigurationWriter print(String s) {
}

private ConfigurationWriter printSeq(Collection<?> value) {
out.format("[ ");
out.format("[");
indent += 4;
newline();
printIndent();
Expand All @@ -555,7 +559,7 @@ private ConfigurationWriter printSeq(Collection<?> value) {
}
indent -= 4;
newline().printIndent();
out.format(" ]");
out.format("]");
return this;
}

Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ public Configuration getConfiguration() {
* Used by saveSettings() and settingsToString()
*/
public void settingsToStream(Writer out) {
getConfiguration().save(out, "Proof-Settings-Config-File");
getConfiguration().save(out, "");
}

/**
Expand Down
111 changes: 74 additions & 37 deletions ...mples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,42 +1,79 @@
\profile "Java Profile";

\settings {
"#Proof-Settings-Config-File
#Wed Jun 04 18:34:33 CEST 2014
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , runtimeExceptions-runtimeExceptions\\:ban
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
"
\settings{
"Choice" : {
"JavaCard" : "JavaCard\:on",
"Strings" : "Strings\:on",
"assertions" : "assertions\:on",
"bigint" : "bigint\:on",
"finalFields" : "finalFields:immutable",
"floatRules" : "floatRules:strictfpOnly",
"initialisation" : "initialisation\:disableStaticInitialisation",
"intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
"integerSimplificationRules" : "integerSimplificationRules\:full",
"javaLoopTreatment" : "javaLoopTreatment:efficient",
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
"methodExpansion" : "methodExpansion:modularOnly",
"modelFields" : "modelFields\:treatAsAxiom",
"moreSeqRules" : "moreSeqRules:off",
"optimisedSelectRules" : "optimisedSelectRules\:on",
"permissions" : "permissions:off",
"programRules" : "programRules\:Java",
"reach" : "reach\:on",
"runtimeExceptions" : "runtimeExceptions\:ban",
"sequences" : "sequences\:on",
"soundDefaultContracts" : "soundDefaultContracts:on",
"wdChecks" : "wdChecks\:off",
"wdOperator" : "wdOperator\:L"
},
"Labels" : {
"UseOriginLabels" : true
},
"NewSMT" : {

},
"SMTSettings" : {
"SelectedTaclets" : [

],
"UseBuiltUniqueness" : false,
"explicitTypeHierarchy" : false,
"instantiateHierarchyAssumptions" : true,
"integersMaximum" : 2147483645,
"integersMinimum" : -2147483645,
"invariantForall" : false,
"maxGenericSorts" : 2,
"useConstantsForBigOrSmallIntegers" : true,
"useUninterpretedMultiplication" : true
},
"Strategy" : {
"ActiveStrategy" : "JavaCardDLStrategy",
"MaximumNumberOfAutomaticApplications" : 10000,
"Timeout" : -1,
"options" : {
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
"DEP_OPTIONS_KEY" : "DEP_ON",
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
"MPS_OPTIONS_KEY" : "MPS_MERGE",
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
"OSS_OPTIONS_KEY" : "OSS_ON",
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
"VBT_PHASE" : "VBT_SYM_EX"
}
}
}

\javaSource "src/contract";
Expand Down
111 changes: 74 additions & 37 deletions ...es(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,42 +1,79 @@
\profile "Java Profile";

\settings {
"#Proof-Settings-Config-File
#Wed Jun 04 18:34:33 CEST 2014
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , runtimeExceptions-runtimeExceptions\\:ban
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
"
\settings{
"Choice" : {
"JavaCard" : "JavaCard\:on",
"Strings" : "Strings\:on",
"assertions" : "assertions\:on",
"bigint" : "bigint\:on",
"finalFields" : "finalFields:immutable",
"floatRules" : "floatRules:strictfpOnly",
"initialisation" : "initialisation\:disableStaticInitialisation",
"intRules" : "intRules\:arithmeticSemanticsIgnoringOF",
"integerSimplificationRules" : "integerSimplificationRules\:full",
"javaLoopTreatment" : "javaLoopTreatment:efficient",
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
"methodExpansion" : "methodExpansion:modularOnly",
"modelFields" : "modelFields\:treatAsAxiom",
"moreSeqRules" : "moreSeqRules:off",
"optimisedSelectRules" : "optimisedSelectRules\:on",
"permissions" : "permissions:off",
"programRules" : "programRules\:Java",
"reach" : "reach\:on",
"runtimeExceptions" : "runtimeExceptions\:ban",
"sequences" : "sequences\:on",
"soundDefaultContracts" : "soundDefaultContracts:on",
"wdChecks" : "wdChecks\:off",
"wdOperator" : "wdOperator\:L"
},
"Labels" : {
"UseOriginLabels" : true
},
"NewSMT" : {

},
"SMTSettings" : {
"SelectedTaclets" : [

],
"UseBuiltUniqueness" : false,
"explicitTypeHierarchy" : false,
"instantiateHierarchyAssumptions" : true,
"integersMaximum" : 2147483645,
"integersMinimum" : -2147483645,
"invariantForall" : false,
"maxGenericSorts" : 2,
"useConstantsForBigOrSmallIntegers" : true,
"useUninterpretedMultiplication" : true
},
"Strategy" : {
"ActiveStrategy" : "JavaCardDLStrategy",
"MaximumNumberOfAutomaticApplications" : 10000,
"Timeout" : -1,
"options" : {
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
"DEP_OPTIONS_KEY" : "DEP_ON",
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
"MPS_OPTIONS_KEY" : "MPS_MERGE",
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
"OSS_OPTIONS_KEY" : "OSS_ON",
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
"VBT_PHASE" : "VBT_SYM_EX"
}
}
}

\javaSource "src/contract";
Expand Down
Loading
Loading