From d026c5cbe9389cd551b54443c05d5c0a85d7c1e7 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Tue, 28 Nov 2023 17:33:40 +0100
Subject: [PATCH 01/40] Hopefully (yet untested) fixed previous 'assigns' and
also introduced 'loop_modifies' and 'loop_writes' from OpenJML as JML aliases
---
key.core/src/main/antlr4/JmlLexer.g4 | 7 +++----
key.core/src/main/antlr4/JmlParser.g4 | 4 +++-
2 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index f1a67a2afd5..bfb5ef93228 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -74,8 +74,8 @@ fragment Pfree: '_free'?; //suffix
ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
ASSERT: 'assert' Pred -> pushMode(expr);
ASSUME: 'assume' Pred -> pushMode(expr);
-ASSIGNABLE: 'assignable' Pfree -> pushMode(expr);
-ASSIGNS: 'assigns' Pred -> pushMode(expr);
+ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr);
+LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') (Pfree|Pred) -> pushMode(expr);
AXIOM: 'axiom' -> pushMode(expr);
BREAKS: 'breaks' -> pushMode(expr);
CAPTURES: 'captures' Pred -> pushMode(expr);
@@ -105,8 +105,7 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr);
MERGE_POINT: 'merge_point';
MERGE_PROC: 'merge_proc';
MERGE_PARAMS: 'merge_params' -> pushMode(expr);
-MODIFIABLE: 'modifiable' Pred -> pushMode(expr);
-MODIFIES: 'modifies' Pred -> pushMode(expr);
+MODIFIABLE: ('modifiable' | 'modifies') Pred -> pushMode(expr);
MONITORED: 'monitored' -> pushMode(expr);
MONITORS_FOR: 'monitors_for' -> pushMode(expr);
//OLD: 'old' -> pushMode(expr);
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index a66965df0fd..1de7aba7f3f 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -87,7 +87,7 @@ accessible_clause
(lhs=expression COLON)? rhs=storeRefUnion
(MEASURED_BY mby=expression)?
SEMI_TOPLEVEL;
-assignable_clause: (ASSIGNABLE|MODIFIES|MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+assignable_clause: (ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
//depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ;
//decreases_clause: DECREASES termexpression (COMMA termexpression)*;
represents_clause
@@ -175,9 +175,11 @@ loop_specification
| loop_separates_clause
| loop_determines_clause
| assignable_clause
+ | loop_assignable_clause
| variant_function)*;
loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL;
+loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL;
//loop_separates_clause: SEPARATES expression;
//loop_determines_clause: DETERMINES expression;
From b35e0a895adf6e6211659ca74913441993b40748 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Tue, 28 Nov 2023 18:09:33 +0100
Subject: [PATCH 02/40] Re-added MODIFIES as it was also used somewhere else
---
key.core/src/main/antlr4/JmlLexer.g4 | 3 ++-
key.core/src/main/antlr4/JmlParser.g4 | 4 ++--
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index bfb5ef93228..75bb8d4b1f3 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -105,7 +105,8 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr);
MERGE_POINT: 'merge_point';
MERGE_PROC: 'merge_proc';
MERGE_PARAMS: 'merge_params' -> pushMode(expr);
-MODIFIABLE: ('modifiable' | 'modifies') Pred -> pushMode(expr);
+MODIFIABLE: 'modifiable' Pred -> pushMode(expr);
+MODIFIES: 'modifies' Pred -> pushMode(expr);
MONITORED: 'monitored' -> pushMode(expr);
MONITORS_FOR: 'monitors_for' -> pushMode(expr);
//OLD: 'old' -> pushMode(expr);
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index 1de7aba7f3f..23c20a54994 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -87,7 +87,7 @@ accessible_clause
(lhs=expression COLON)? rhs=storeRefUnion
(MEASURED_BY mby=expression)?
SEMI_TOPLEVEL;
-assignable_clause: (ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+assignable_clause: (ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
//depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ;
//decreases_clause: DECREASES termexpression (COMMA termexpression)*;
represents_clause
@@ -179,7 +179,7 @@ loop_specification
| variant_function)*;
loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL;
-loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL;
//loop_separates_clause: SEPARATES expression;
//loop_determines_clause: DETERMINES expression;
From e65a8e8253df0ec91efce38c097e5a868b995b36 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Wed, 29 Nov 2023 01:05:50 +0100
Subject: [PATCH 03/40] Added syntax highlighting
---
.../java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
index 2eb275be4c5..cea30168b0f 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
@@ -177,7 +177,10 @@ private enum CommentState {
"\\working_space", "\\values", "\\inv",
// clause keywords:
"accessible", "accessible_redundantly", "assert", "assert_redundantly", "assignable",
- "assignable_free", "assignable_redundantly", "assume", "assume_redudantly", "breaks",
+ "assignable_free", "assignable_redundantly", "assigns", "assigns_free",
+ "assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly",
+ "loop_modifies", "loop_modifies_free", "loop_modifies_redundantly", "loop_writes",
+ "loop_writes_free", "loop_writes_redundantly"," assume", "assume_redudantly", "breaks",
"breaks_redundantly", "\\by", "callable", "callable_redundantly", "captures",
"captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies",
"decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", "diverges",
From bfc513ce83ac1576c88f0d28a0807f260e37145f Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Wed, 29 Nov 2023 01:23:23 +0100
Subject: [PATCH 04/40] Removed one ambiguity
---
key.core/src/main/antlr4/JmlParser.g4 | 1 -
1 file changed, 1 deletion(-)
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index 23c20a54994..96bc5ff50ac 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -174,7 +174,6 @@ loop_specification
| determines_clause
| loop_separates_clause
| loop_determines_clause
- | assignable_clause
| loop_assignable_clause
| variant_function)*;
From 9b4e1fd40ac6ef3e1c38d0c119b17e6378bea5f3 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Wed, 29 Nov 2023 01:31:24 +0100
Subject: [PATCH 05/40] Minor formatting
---
.../main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
index cea30168b0f..6a71eebebf2 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
@@ -180,7 +180,7 @@ private enum CommentState {
"assignable_free", "assignable_redundantly", "assigns", "assigns_free",
"assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly",
"loop_modifies", "loop_modifies_free", "loop_modifies_redundantly", "loop_writes",
- "loop_writes_free", "loop_writes_redundantly"," assume", "assume_redudantly", "breaks",
+ "loop_writes_free", "loop_writes_redundantly", "assume", "assume_redudantly", "breaks",
"breaks_redundantly", "\\by", "callable", "callable_redundantly", "captures",
"captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies",
"decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", "diverges",
From c9ed0b8d2b21580c0739d12f8d997c170547f6bd Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Wed, 29 Nov 2023 22:24:09 +0100
Subject: [PATCH 06/40] Mistakenly included redundancy suffix
---
key.core/src/main/antlr4/JmlLexer.g4 | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index 75bb8d4b1f3..c4436657100 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -75,7 +75,7 @@ ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
ASSERT: 'assert' Pred -> pushMode(expr);
ASSUME: 'assume' Pred -> pushMode(expr);
ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr);
-LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') (Pfree|Pred) -> pushMode(expr);
+LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') Pfree -> pushMode(expr);
AXIOM: 'axiom' -> pushMode(expr);
BREAKS: 'breaks' -> pushMode(expr);
CAPTURES: 'captures' Pred -> pushMode(expr);
From 0ffead610249390fc980367e690a22d72f857f1d Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Wed, 21 Feb 2024 17:49:56 +0100
Subject: [PATCH 07/40] Integrated port of loop assignable at HackeYthon
---
.../key/speclang/njml/TextualTranslator.java | 29 +++++++++++++++++--
.../ilkd/key/speclang/njml/Translator.java | 16 ++++++++++
2 files changed, 43 insertions(+), 2 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index 20ecef050c2..183e52dee3f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -12,6 +12,7 @@
import org.key_project.util.collection.ImmutableSLList;
import org.antlr.v4.runtime.ParserRuleContext;
+import org.antlr.v4.runtime.tree.TerminalNode;
import org.antlr.v4.runtime.Token;
import org.jspecify.annotations.Nullable;
@@ -254,9 +255,10 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
@Override
public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
+ final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE()
+ : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE();
final boolean isFree =
- ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free")
- || ctx.MODIFIES() != null && ctx.MODIFIES().getText().endsWith("_free");
+ assign != null && assign.getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
? OriginTermLabel.SpecType.ASSIGNABLE_FREE
@@ -276,6 +278,29 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
return null;
}
+ @Override public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
+ Name[] heaps = visitTargetHeap(ctx.targetHeap());
+ final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE()
+ : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE() != null ?
+ ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE();
+ final boolean isFree =
+ assign != null && assign.getText().endsWith("_free");
+ final LabeledParserRuleContext ctx2 =
+ LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
+ ? OriginTermLabel.SpecType.ASSIGNABLE_FREE
+ : OriginTermLabel.SpecType.ASSIGNABLE,
+ attachOriginLabel);
+ for (Name heap : heaps) {
+ if (loopContract != null) {
+ loopContract.addClause(
+ isFree ? TextualJMLLoopSpec.ClauseHd.ASSIGNABLE_FREE
+ : TextualJMLLoopSpec.ClauseHd.ASSIGNABLE,
+ heap, ctx2);
+ }
+ }
+ return null;
+ }
+
@Override
public Object visitVariant_function(JmlParser.Variant_functionContext ctx) {
final LabeledParserRuleContext ctx2 =
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index 15de4187522..90c2c438552 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -2007,6 +2007,22 @@ public SLExpression visitAssignable_clause(JmlParser.Assignable_clauseContext ct
return new SLExpression(t);
}
+ @Override
+ public SLExpression visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
+ Term t;
+ LocationVariable[] heaps = visitTargetHeap(ctx.targetHeap());
+ if (ctx.STRICTLY_NOTHING() != null) {
+ t = tb.strictlyNothing();
+ } else {
+ final Term storeRef = accept(ctx.storeRefUnion());
+ assert storeRef != null;
+ t = termFactory.assignable(storeRef);
+ }
+ for (LocationVariable heap : heaps) {
+ contractClauses.add(ContractClauses.ASSIGNABLE, heap, t);
+ }
+ return new SLExpression(t);
+ }
@Override
public SLExpression visitSignals_only_clause(JmlParser.Signals_only_clauseContext ctx) {
From 097abe385cd906d538833ba9d777a8bd8a06f2d7 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Wed, 21 Feb 2024 17:50:58 +0100
Subject: [PATCH 08/40] Applied spotless
---
.../de/uka/ilkd/key/speclang/njml/TextualTranslator.java | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index 183e52dee3f..a296f5d7ea7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -12,8 +12,8 @@
import org.key_project.util.collection.ImmutableSLList;
import org.antlr.v4.runtime.ParserRuleContext;
-import org.antlr.v4.runtime.tree.TerminalNode;
import org.antlr.v4.runtime.Token;
+import org.antlr.v4.runtime.tree.TerminalNode;
import org.jspecify.annotations.Nullable;
import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec.ClauseHd.INVARIANT;
@@ -278,11 +278,12 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
return null;
}
- @Override public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
+ @Override
+ public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE()
- : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE() != null ?
- ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE();
+ : ctx.MODIFIES() != null ? ctx.MODIFIES()
+ : ctx.MODIFIABLE() != null ? ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE();
final boolean isFree =
assign != null && assign.getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
From 394edd50012d432b8ad8b24c66c9e401ffed5089 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Tue, 27 Feb 2024 18:41:00 +0100
Subject: [PATCH 09/40] Added more keywords (at least preliminarily and up for
discussion)
---
key.core/src/main/antlr4/JmlLexer.g4 | 9 ++++---
.../ilkd/key/gui/sourceview/JavaDocument.java | 24 ++++++++++++-------
2 files changed, 22 insertions(+), 11 deletions(-)
diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index c4436657100..73d999b4242 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -75,7 +75,10 @@ ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
ASSERT: 'assert' Pred -> pushMode(expr);
ASSUME: 'assume' Pred -> pushMode(expr);
ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr);
-LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') Pfree -> pushMode(expr);
+LOOP_ASSIGNABLE
+ : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' |
+ 'loop_modifiable' | 'loop_modifies' | 'loop_modifying' |
+ 'loop_writable' | 'loop_writes' | 'loop_writing') Pfree -> pushMode(expr);
AXIOM: 'axiom' -> pushMode(expr);
BREAKS: 'breaks' -> pushMode(expr);
CAPTURES: 'captures' Pred -> pushMode(expr);
@@ -105,8 +108,8 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr);
MERGE_POINT: 'merge_point';
MERGE_PROC: 'merge_proc';
MERGE_PARAMS: 'merge_params' -> pushMode(expr);
-MODIFIABLE: 'modifiable' Pred -> pushMode(expr);
-MODIFIES: 'modifies' Pred -> pushMode(expr);
+MODIFIABLE: ('modifiable' | 'writable') Pred -> pushMode(expr);
+MODIFIES: ('modifies' | 'modifying' | 'writes' | 'writing') Pred -> pushMode(expr);
MONITORED: 'monitored' -> pushMode(expr);
MONITORS_FOR: 'monitors_for' -> pushMode(expr);
//OLD: 'old' -> pushMode(expr);
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
index 6a71eebebf2..8eefe1e7c83 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
@@ -163,7 +163,7 @@ private enum CommentState {
"spec_safe_math", "static", "strictfp", "strictly_pure", "synchronized", "transient",
"two_state", "uninitialized", "volatile",
- "no_state", "modifies", "erases", "modifiable", "returns", "break_behavior",
+ "no_state", "modifies", "modifying", "erases", "modifiable", "returns", "break_behavior",
"continue_behavior", "return_behavior",
// special JML expressions:
"\\constraint_for", "\\created", "\\disjoint", "\\duration", "\\everything", "\\exception",
@@ -176,14 +176,22 @@ private enum CommentState {
"\\static_invariant_for", "\\strictly_nothing", "\\subset", "\\sum", "\\type", "\\typeof",
"\\working_space", "\\values", "\\inv",
// clause keywords:
- "accessible", "accessible_redundantly", "assert", "assert_redundantly", "assignable",
- "assignable_free", "assignable_redundantly", "assigns", "assigns_free",
+ "accessible", "accessible_redundantly", "assert", "assert_redundantly",
+ "assignable", "assignable_free", "assignable_redundantly", "assigns", "assigns_free",
"assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly",
- "loop_modifies", "loop_modifies_free", "loop_modifies_redundantly", "loop_writes",
- "loop_writes_free", "loop_writes_redundantly", "assume", "assume_redudantly", "breaks",
- "breaks_redundantly", "\\by", "callable", "callable_redundantly", "captures",
+ "loop_assignable", "loop_assignable_free", "loop_assignable_redundantly", "loop_assigns",
+ "loop_assigns_free", "loop_assigns_redundantly", "loop_assigning", "loop_assigning_free",
+ "loop_assigning_redundantly", "loop_modifiable", "loop_modifiable_free",
+ "loop_modifiable_redundantly", "loop_modifies", "loop_modifies_free",
+ "loop_modifies_redundantly", "loop_modifying", "loop_modifying_free",
+ "loop_modifying_redundantly", "loop_writable", "loop_writable_free",
+ "loop_writable_redundantly", "loop_writes", "loop_writes_free", "loop_writes_redundantly",
+ "loop_writing", "loop_writing_free", "loop_writing_redundantly",
+ "assume", "assume_redudantly", "breaks", "breaks_redundantly", "\\by",
+ "callable", "callable_redundantly", "captures",
"captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies",
- "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", "diverges",
+ "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly",
+ "loop_variant", "loop_variant_redundantly", "diverges",
"determines", "diverges_redundantly", "duration", "duration_redundantly", "ensures",
"ensures_free", "ensures_redundantly", "\\erases", "forall", "for_example", "hence_by",
"implies_that", "in", "in_redundantly", "\\into", "loop_invariant", "loop_invariant_free",
@@ -195,7 +203,7 @@ private enum CommentState {
"abrupt_behavior", "abrupt_behaviour", "also", "axiom", "behavior", "behaviour",
"constraint", "exceptional_behavior", "exceptional_behaviour", "initially", "invariant",
"invariant_free", "model_behavior", "model_behaviour", "monitors_for", "normal_behavior",
- "normal_behaviour", "readable", "writable",
+ "normal_behaviour", "readable", "writable", "writes", "writing",
// ADT functions:
"\\seq_empty", "\\seq_def", "\\seq_singleton", "\\seq_get", "\\seq_put", "\\seq_reverse",
"\\seq_length", "\\index_of", "\\seq_concat", "\\empty", "\\singleton", "\\set_union",
From ece551beebd7af956003ea33725681b89ec171d5 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Thu, 29 Feb 2024 16:24:35 +0100
Subject: [PATCH 10/40] Unify modifiable|modifying|modifies as the distinction
has not been used anywhere
---
key.core/src/main/antlr4/JmlLexer.g4 | 15 ++++++++-------
key.core/src/main/antlr4/JmlParser.g4 | 4 ++--
.../ilkd/key/speclang/njml/TextualTranslator.java | 9 ++-------
3 files changed, 12 insertions(+), 16 deletions(-)
diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index 73d999b4242..002c9d5896d 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -74,11 +74,14 @@ fragment Pfree: '_free'?; //suffix
ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
ASSERT: 'assert' Pred -> pushMode(expr);
ASSUME: 'assume' Pred -> pushMode(expr);
-ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr);
+ASSIGNABLE
+ : ('assignable' | 'assigns' | 'assigning' |
+ 'modifiable' | 'modifies' | 'modifying' |
+ 'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr);
LOOP_ASSIGNABLE
: ('loop_assignable' | 'loop_assigns' | 'loop_assigning' |
'loop_modifiable' | 'loop_modifies' | 'loop_modifying' |
- 'loop_writable' | 'loop_writes' | 'loop_writing') Pfree -> pushMode(expr);
+ 'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr);
AXIOM: 'axiom' -> pushMode(expr);
BREAKS: 'breaks' -> pushMode(expr);
CAPTURES: 'captures' Pred -> pushMode(expr);
@@ -90,7 +93,7 @@ DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr)
DETERMINES: 'determines' -> pushMode(expr);
DIVERGES: 'diverges' Pred -> pushMode(expr);
//DURATION: 'duration' Pred -> pushMode(expr);
-ENSURES: ('ensures' (Pfree|Pred) | 'post' Pred )-> pushMode(expr);
+ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr);
FOR_EXAMPLE: 'for_example' -> pushMode(expr);
//FORALL: 'forall' -> pushMode(expr); //?
HELPER: 'helper';
@@ -100,7 +103,7 @@ INITIALLY: 'initially' -> pushMode(expr);
INSTANCE: 'instance';
INVARIANT: 'invariant' (Pfree|Pred) -> pushMode(expr);
LOOP_CONTRACT: 'loop_contract';
-LOOP_INVARIANT: ('loop_invariant' (Pfree|Pred) | 'maintaining' Pred) -> pushMode(expr);
+LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred) -> pushMode(expr);
LOOP_DETERMINES: 'loop_determines'; // internal translation for 'determines' in loop invariants
LOOP_SEPARATES: 'loop_separates'; //KeY extension, deprecated
MAPS: 'maps' Pred -> pushMode(expr);
@@ -108,8 +111,6 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr);
MERGE_POINT: 'merge_point';
MERGE_PROC: 'merge_proc';
MERGE_PARAMS: 'merge_params' -> pushMode(expr);
-MODIFIABLE: ('modifiable' | 'writable') Pred -> pushMode(expr);
-MODIFIES: ('modifies' | 'modifying' | 'writes' | 'writing') Pred -> pushMode(expr);
MONITORED: 'monitored' -> pushMode(expr);
MONITORS_FOR: 'monitors_for' -> pushMode(expr);
//OLD: 'old' -> pushMode(expr);
@@ -117,7 +118,7 @@ MONITORS_FOR: 'monitors_for' -> pushMode(expr);
//PRE: 'pre' Pred -> pushMode(expr);
READABLE: 'readable';
REPRESENTS: 'represents' Pred -> pushMode(expr);
-REQUIRES: ('requires' (Pfree|Pred) | 'pre' Pred) -> pushMode(expr);
+REQUIRES: ('requires'| 'pre') (Pfree|Pred) -> pushMode(expr);
RETURN: 'return' -> pushMode(expr);
RETURNS: 'returns' -> pushMode(expr);
RESPECTS: 'respects' -> pushMode(expr);
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index 96bc5ff50ac..804323c5cc5 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -87,7 +87,7 @@ accessible_clause
(lhs=expression COLON)? rhs=storeRefUnion
(MEASURED_BY mby=expression)?
SEMI_TOPLEVEL;
-assignable_clause: (ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
//depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ;
//decreases_clause: DECREASES termexpression (COMMA termexpression)*;
represents_clause
@@ -178,7 +178,7 @@ loop_specification
| variant_function)*;
loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL;
-loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL;
//loop_separates_clause: SEPARATES expression;
//loop_determines_clause: DETERMINES expression;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index a296f5d7ea7..975ede713e9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -255,10 +255,8 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
@Override
public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
- final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE()
- : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE();
final boolean isFree =
- assign != null && assign.getText().endsWith("_free");
+ ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
? OriginTermLabel.SpecType.ASSIGNABLE_FREE
@@ -281,11 +279,8 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
@Override
public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
- final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE()
- : ctx.MODIFIES() != null ? ctx.MODIFIES()
- : ctx.MODIFIABLE() != null ? ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE();
final boolean isFree =
- assign != null && assign.getText().endsWith("_free");
+ ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
? OriginTermLabel.SpecType.ASSIGNABLE_FREE
From c69175996bcd3e24412cdf3ede76b2af2ccd0d78 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Thu, 29 Feb 2024 18:01:30 +0100
Subject: [PATCH 11/40] Some syntax harmonization for some consistency within
the code base
---
.../uka/ilkd/key/util/rifl/RIFLHandler.java | 8 +-
.../de.uka.ilkd.key.util/rifl/rifl-1.0.dtd | 6 +-
.../TestSymbolicExecutionTreeBuilder.java | 24 ++--
.../TestTruthValueEvaluationUtil.java | 24 ++--
.../slicing/TestThinBackwardSlicer.java | 36 ++---
.../de/uka/ilkd/key/testgen/ProofInfo.java | 4 +-
.../ilkd/key/testgen/TestCaseGenerator.java | 2 +-
key.core/src/main/antlr4/JmlLexer.g4 | 6 +-
key.core/src/main/antlr4/JmlParser.g4 | 8 +-
.../ilkd/key/logic/label/OriginTermLabel.java | 8 +-
.../init/FunctionalOperationContractPO.java | 2 +-
.../key/proof/init/WellDefinednessPO.java | 2 +-
.../metaconstruct/CreateBeforeLoopUpdate.java | 2 +-
.../rule/metaconstruct/CreateFrameCond.java | 2 +-
.../metaconstruct/CreateHeapAnonUpdate.java | 4 +-
.../AbstractAuxiliaryContractImpl.java | 26 ++--
.../ilkd/key/speclang/AuxiliaryContract.java | 10 +-
.../ilkd/key/speclang/BlockContractImpl.java | 8 +-
.../key/speclang/BlockWellDefinedness.java | 12 +-
.../key/speclang/ClassWellDefinedness.java | 12 +-
.../de/uka/ilkd/key/speclang/Contract.java | 2 +-
.../key/speclang/DependencyContractImpl.java | 2 +-
.../speclang/FunctionalAuxiliaryContract.java | 4 +-
.../FunctionalOperationContractImpl.java | 6 +-
.../speclang/InformationFlowContractImpl.java | 2 +-
.../ilkd/key/speclang/LoopContractImpl.java | 20 +--
.../key/speclang/LoopWellDefinedness.java | 12 +-
.../key/speclang/MethodWellDefinedness.java | 18 +--
.../speclang/StatementWellDefinedness.java | 6 +-
.../key/speclang/WellDefinednessCheck.java | 66 +++++-----
.../key/speclang/jml/JMLSpecExtractor.java | 4 +-
.../pretranslation/TextualJMLLoopSpec.java | 30 ++---
.../pretranslation/TextualJMLSpecCase.java | 14 +-
.../jml/translation/JMLSpecFactory.java | 124 +++++++++---------
.../key/speclang/njml/ContractClauses.java | 2 +-
.../key/speclang/njml/JmlTermFactory.java | 10 +-
.../key/speclang/njml/TextualTranslator.java | 26 ++--
.../ilkd/key/speclang/njml/Translator.java | 12 +-
.../key/speclang/ContractFactoryTest.java | 6 +-
.../speclang/jml/TestJMLPreTranslator.java | 10 +-
.../ilkd/key/gui/sourceview/JavaDocument.java | 5 +-
.../ilkd/key/gui/sourceview/SourceView.java | 2 +-
42 files changed, 295 insertions(+), 294 deletions(-)
diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java
index 94addf6468f..f7a7066bbb7 100644
--- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java
+++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java
@@ -102,12 +102,12 @@ private void assignHandle(Attributes attributes) {
categories2domains.put(p, domain);
}
- private void setAssignable(Attributes attributes) {
+ private void setModifiable(Attributes attributes) {
assert tmpHandle == null;
tmpHandle = attributes.getValue("handle");
}
- private void unsetAssignable() {
+ private void unsetModifiable() {
assert tmpHandle != null;
tmpHandle = null;
}
@@ -214,7 +214,7 @@ public void startElement(String uri, String localName, String qName, Attributes
// case "domainassignment":
case "domains" -> startDomains();
case "domain" -> putDomain(attributes);
- case "assignable" -> setAssignable(attributes);
+ case "modifiable" -> setModifiable(attributes);
case "field" -> putField(attributes);
case "parameter" -> putParam(attributes);
case "returnvalue" -> putReturn(attributes);
@@ -240,7 +240,7 @@ public void startElement(String uri, String localName, String qName, Attributes
@Override
public void endElement(String uri, String localName, String qName) {
switch (localName) {
- case "assignable" -> unsetAssignable();
+ case "modifiable" -> unsetModifiable();
case "category" -> unsetCategory();
case "domains" -> checkDomains();
case "domainassignment" -> checkDomainAssignmentsWithFlows();
diff --git a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd
index 9c4a9da821a..618a508badd 100644
--- a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd
+++ b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd
@@ -8,9 +8,9 @@
-
-
-
+
+
+
diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java
index 606c82e328e..ef4d66447d4 100644
--- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java
+++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java
@@ -186,37 +186,37 @@ public void testUseOperationContractLightweightOperationContractTest() throws Ex
}
/**
- * Tests example: /set/blockContractAssignableEverything
+ * Tests example: /set/blockContractModifiableEverything
*/
@Test
- public void testBlockContractAssignableEverything() throws Exception {
+ public void testBlockContractModifiableEverything() throws Exception {
doSETTestAndDispose(testCaseDirectory,
- "/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof",
- "/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml",
+ "/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof",
+ "/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml",
false, false, true, true, false, false, false, false, false, false, false, false,
false);
}
/**
- * Tests example: /set/blockContractAssignableLocationNotRequested
+ * Tests example: /set/blockContractModifiableLocationNotRequested
*/
@Test
- public void testBlockContractAssignableLocationNotRequested() throws Exception {
+ public void testBlockContractModifiableLocationNotRequested() throws Exception {
doSETTestAndDispose(testCaseDirectory,
- "/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof",
- "/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml",
+ "/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof",
+ "/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml",
false, false, true, true, false, false, false, false, false, false, false, false,
false);
}
/**
- * Tests example: /set/blockContractAssignableRequestedLocation
+ * Tests example: /set/blockContractModifiableRequestedLocation
*/
@Test
- public void testBlockContractAssignableRequestedLocation() throws Exception {
+ public void testBlockContractModifiableRequestedLocation() throws Exception {
doSETTestAndDispose(testCaseDirectory,
- "/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof",
- "/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml",
+ "/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof",
+ "/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml",
false, false, true, true, false, false, false, false, false, false, false, false,
false);
}
diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java
index 587c44c4811..e02a1979ce7 100644
--- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java
+++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java
@@ -89,10 +89,10 @@ public void testTruthValueLabelBelowUpdatesDifferentToApplicationTerm() throws E
}
/**
- * Tests example: /set/truthValueExceptinalAssignableNothingTest
+ * Tests example: /set/truthValueExceptionalModifiableNothingTest
*/
@Test
- public void testExceptinalAssignableNothingTest_OSS() throws Exception {
+ public void testExceptionalModifiableNothingTest_OSS() throws Exception {
// Create expected results
ExpectedBranchResult goal374 =
new ExpectedBranchResult(new ExpectedTruthValueResult("0.0", TruthValue.FALSE),
@@ -138,16 +138,16 @@ public void testExceptinalAssignableNothingTest_OSS() throws Exception {
new ExpectedTruthValueEvaluationResult(goal374, goal407, goal444, goal475, goal476);
// Perform test
doTruthValueEvaluationTest(
- "/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof",
- "/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml",
+ "/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof",
+ "/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml",
false, false, false, exceptionResult);
}
/**
- * Tests example: /set/truthValueExceptinalAssignableNothingTest
+ * Tests example: /set/truthValueExceptionalModifiableNothingTest
*/
@Test
- public void testExceptinalAssignableNothingTest() throws Exception {
+ public void testExceptionalModifiableNothingTest() throws Exception {
// Create expected results
ExpectedBranchResult goal374 =
new ExpectedBranchResult(new ExpectedTruthValueResult("0.0", TruthValue.FALSE),
@@ -193,8 +193,8 @@ public void testExceptinalAssignableNothingTest() throws Exception {
new ExpectedTruthValueEvaluationResult(goal374, goal407, goal444, goal475, goal476);
// Perform test
doTruthValueEvaluationTest(
- "/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof",
- "/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml",
+ "/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof",
+ "/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml",
false, false, false, exceptionResult);
}
@@ -310,11 +310,11 @@ public void IGNORE_testAddingOfLabeledSubtree() throws Exception {
}
/**
- * Tests example: /set/truthValueAssignableAndLoop
+ * Tests example: /set/truthValueModifiableAndLoop
*/
@Test
@Disabled
- public void IGNORE_testAssignableAndLoop() throws Exception {
+ public void IGNORE_testModifiableAndLoop() throws Exception {
// Create expected results
ExpectedBranchResult goal430 =
new ExpectedBranchResult(new ExpectedTruthValueResult("3.0", TruthValue.FALSE),
@@ -370,8 +370,8 @@ public void IGNORE_testAssignableAndLoop() throws Exception {
ExpectedTruthValueEvaluationResult result5 =
new ExpectedTruthValueEvaluationResult(goal1113, goal1134, goal1137);
// Perform test
- doTruthValueEvaluationTest("/set/truthValueAssignableAndLoop/test/MagicProofNoOSS.proof",
- "/set/truthValueAssignableAndLoop/oracle/MagicProofNoOSS.xml", true, true, false,
+ doTruthValueEvaluationTest("/set/truthValueModifiableAndLoop/test/MagicProofNoOSS.proof",
+ "/set/truthValueModifiableAndLoop/oracle/MagicProofNoOSS.xml", true, true, false,
resultExceptionBranch, resultInvInitial, resultPrecondition, resultLoopEnd, result5);
}
diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java
index 89abfcd9b27..3cca929d806 100644
--- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java
+++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java
@@ -51,74 +51,74 @@ public class TestThinBackwardSlicer extends AbstractSymbolicExecutionTestCase {
private static final Logger LOGGER = LoggerFactory.getLogger(TestThinBackwardSlicer.class);
/**
- * Tests slicing on the example {@code blockContractAssignableLocationNotRequested}.
+ * Tests slicing on the example {@code blockContractModifiableLocationNotRequested}.
*
* @throws Exception Occurred Exception.
*/
@Test
- public void testBlockContractAssignableLocationNotRequested() throws Exception {
+ public void testBlockContractModifiableLocationNotRequested() throws Exception {
doSlicingTest(
- "/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof",
+ "/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof",
new ReturnSelector(122), true, 109, 14, 12);
}
/**
- * Tests slicing on the example {@code blockContractAssignableRequestedLocation}.
+ * Tests slicing on the example {@code blockContractModifiableRequestedLocation}.
*
* @throws Exception Occurred Exception.
*/
@Test
- public void testBlockContractAssignableRequestedLocation() throws Exception {
+ public void testBlockContractModifiableRequestedLocation() throws Exception {
doSlicingTest(
- "/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof",
+ "/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof",
new ReturnSelector(111), true, 23);
}
/**
- * Tests slicing on the example {@code blockContractAssignableEverything}.
+ * Tests slicing on the example {@code blockContractModifiableEverything}.
*
* @throws Exception Occurred Exception.
*/
@Test
- public void testBlockContractAssignableEverything() throws Exception {
+ public void testBlockContractModifiableEverything() throws Exception {
doSlicingTest(
- "/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof",
+ "/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof",
new ReturnSelector(97), true, 23);
}
/**
- * Tests slicing on the example {@code methodContractAssignableLocationNotRequested}.
+ * Tests slicing on the example {@code methodContractModifiableLocationNotRequested}.
*
* @throws Exception Occurred Exception.
*/
@Test
- public void testMethodContractAssignableLocationNotRequested() throws Exception {
+ public void testMethodContractModifiableLocationNotRequested() throws Exception {
doSlicingTest(
- "/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof",
+ "/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof",
new ReturnSelector(29), true, 14, 12);
}
/**
- * Tests slicing on the example {@code methodContractAssignableRequestedLocation}.
+ * Tests slicing on the example {@code methodContractModifiableRequestedLocation}.
*
* @throws Exception Occurred Exception.
*/
@Test
- public void testMethodContractAssignableRequestedLocation() throws Exception {
+ public void testMethodContractModifiableRequestedLocation() throws Exception {
doSlicingTest(
- "/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof",
+ "/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof",
new ReturnSelector(29), true, 23);
}
/**
- * Tests slicing on the example {@code methodContractAssignableEverything}.
+ * Tests slicing on the example {@code methodContractModifiableEverything}.
*
* @throws Exception Occurred Exception.
*/
@Test
- public void testMethodContractAssignableEverything() throws Exception {
+ public void testMethodContractModifiableEverything() throws Exception {
doSlicingTest(
- "/slicing/methodContractAssignableEverything/MethodContractAssignableExample.proof",
+ "/slicing/methodContractModifiableEverything/MethodContractModifiableExample.proof",
new ReturnSelector(29), true, 23);
}
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
index cc140fd6171..7c2ac9f4a98 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
@@ -86,9 +86,9 @@ public Term getPreConTerm() {
return services.getTermBuilder().ff();
}
- public Term getAssignable() {
+ public Term getModifiable() {
Contract c = getContract();
- return c.getAssignable(services.getTypeConverter().getHeapLDT().getHeap());
+ return c.getModifiable(services.getTypeConverter().getHeapLDT().getHeap());
}
public String getCode() {
diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
index e9b17899bd5..c1466476515 100644
--- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
+++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
@@ -460,7 +460,7 @@ protected String getOracleAssertion(List oracleMethods) {
oracleMethods.addAll(oracleGenerator.getOracleMethods());
LOGGER.debug("Modifier Set: {}",
- oracleGenerator.getOracleLocationSet(info.getAssignable()));
+ oracleGenerator.getOracleLocationSet(info.getModifiable()));
return "assertTrue(" + oracleCall + ");";
}
diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4
index 002c9d5896d..4ca18aa0bca 100644
--- a/key.core/src/main/antlr4/JmlLexer.g4
+++ b/key.core/src/main/antlr4/JmlLexer.g4
@@ -74,11 +74,11 @@ fragment Pfree: '_free'?; //suffix
ACCESSIBLE: 'accessible' Pred -> pushMode(expr);
ASSERT: 'assert' Pred -> pushMode(expr);
ASSUME: 'assume' Pred -> pushMode(expr);
-ASSIGNABLE
+MODIFIABLE
: ('assignable' | 'assigns' | 'assigning' |
'modifiable' | 'modifies' | 'modifying' |
'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr);
-LOOP_ASSIGNABLE
+LOOP_MODIFIABLE
: ('loop_assignable' | 'loop_assigns' | 'loop_assigning' |
'loop_modifiable' | 'loop_modifies' | 'loop_modifying' |
'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr);
@@ -181,7 +181,7 @@ DEPENDS: 'depends'; // internal translation for 'accessible' on model fields
/* JML and JML* keywords */
/*ACCESSIBLE: 'accessible';
-ASSIGNABLE: 'assignable';
+MODIFIABLE: 'modifiable';
BREAKS: 'breaks';
CONTINUES: 'continues';
DECREASES: 'decreases'; // internal translation for 'measured_by'
diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4
index 804323c5cc5..1449567d14d 100644
--- a/key.core/src/main/antlr4/JmlParser.g4
+++ b/key.core/src/main/antlr4/JmlParser.g4
@@ -65,7 +65,7 @@ clause
:
( ensures_clause | requires_clause | measured_by_clause
| captures_clause | diverges_clause | working_space_clause
- | duration_clause | when_clause | assignable_clause | accessible_clause
+ | duration_clause | when_clause | modifiable_clause | accessible_clause
| signals_clause | signals_only_clause | variant_function | name_clause
| breaks_clause | continues_clause | returns_clause | separates_clause
| determines_clause
@@ -87,7 +87,7 @@ accessible_clause
(lhs=expression COLON)? rhs=storeRefUnion
(MEASURED_BY mby=expression)?
SEMI_TOPLEVEL;
-assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+modifiable_clause: MODIFIABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
//depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ;
//decreases_clause: DECREASES termexpression (COMMA termexpression)*;
represents_clause
@@ -174,11 +174,11 @@ loop_specification
| determines_clause
| loop_separates_clause
| loop_determines_clause
- | loop_assignable_clause
+ | loop_modifiable_clause
| variant_function)*;
loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL;
-loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
+loop_modifiable_clause: (LOOP_MODIFIABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL;
variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL;
//loop_separates_clause: SEPARATES expression;
//loop_determines_clause: DETERMINES expression;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
index 5adc7067338..9fb36aa9062 100755
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
@@ -782,14 +782,14 @@ public enum SpecType {
ASSERT("assert"),
/**
- * assignable
+ * modifiable
*/
- ASSIGNABLE("assignable"),
+ MODIFIABLE("modifiable"),
/**
- * assignable_free
+ * modifiable_free
*/
- ASSIGNABLE_FREE("assignable_free"),
+ MODIFIABLE_FREE("modifiable_free"),
/**
* assume
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
index b00fe7b6233..8e19fe5a5ef 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
@@ -255,7 +255,7 @@ protected Term buildFrameClause(List modHeaps, Map
}
}
- return tb.addLabelToAllSubs(frameTerm, new Origin(SpecType.ASSIGNABLE));
+ return tb.addLabelToAllSubs(frameTerm, new Origin(SpecType.MODIFIABLE));
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
index 474bca4516d..a5177213160 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
@@ -39,7 +39,7 @@
* WD( && ) &
* ( &
* -> WD() &
- * {anon^assignable}WD()
+ * {anon^modifiable}WD()
* }
*
*
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java
index f80b447495b..d9dd5bc891b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java
@@ -15,7 +15,7 @@
import de.uka.ilkd.key.util.MiscTools;
/**
- * Initializes the "before loop" update needed for the assignable clause.
+ * Initializes the "before loop" update needed for the modifiable clause.
*
* Only remembers the heaps of the context, not the changed local variables, although this is done
* for the built-in loop invariant rules, where they however are never used.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java
index b213c770edf..135e1a85745 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java
@@ -23,7 +23,7 @@
import de.uka.ilkd.key.util.MiscTools;
/**
- * Creates the frame condition (aka "assignable clause") for the given loop. Also accepts the
+ * Creates the frame condition (aka "modifiable clause") for the given loop. Also accepts the
* pre-state update and extracts the symbols from there. New symbols in the pre-state update (like
* "heap_BeforeLOOP") are added to the namespaces. This is because the update is, for the loop scope
* invariant taclet, created by a variable condition; new symbols created there are not
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java
index d260b6b73f8..bfaea15b0ea 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java
@@ -77,10 +77,10 @@ private static Term createHeapAnonUpdate(LoopSpecification loopSpec, boolean isT
final List heapContext = //
HeapContext.getModHeaps(services, isTransaction);
final Map mods = new LinkedHashMap<>();
- // The call to MiscTools.removeSingletonPVs removes from the assignable clause
+ // The call to MiscTools.removeSingletonPVs removes from the modifiable clause
// the program variables which of course should not be part of an anonymizing
// heap expression. The reason why they're there at all is that for Abstract
- // Execution, it actually makes sense to have program variables in assignable
+ // Execution, it actually makes sense to have program variables in modifiable
// clauses, since for an abstract statement they cannot be extracted like for
// concrete statements (such as loop bodies). (DS, 2019-07-05)
heapContext.forEach(heap -> mods.put(heap,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java
index 1cb413878ca..7bd04738279 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java
@@ -571,7 +571,7 @@ public IProgramMethod getTarget() {
}
@Override
- public Term getAssignable(LocationVariable heap) {
+ public Term getModifiable(LocationVariable heap) {
return modifiesClauses.get(heap);
}
@@ -1020,14 +1020,14 @@ protected static abstract class Creator extends Ter
private final Term diverges;
/**
- * A map from every heap to an assignable term.
+ * A map from every heap to an modifiable term.
*/
- private final Map assignables;
+ private final Map modifiables;
/**
- * A map from every heap to a free assignable term.
+ * A map from every heap to a free modifiable term.
*/
- private final Map assignablesFree;
+ private final Map modifiablesFree;
/**
* A list of heaps used in this contract.
@@ -1066,8 +1066,8 @@ protected static abstract class Creator extends Ter
* termination.
* @param signalsOnly a term specifying which uncaught exceptions may occur.
* @param diverges a diverges clause.
- * @param assignables map from every heap to an assignable term.
- * @param assignablesFree map from every heap to a free assignable term.
+ * @param modifiables map from every heap to an modifiable term.
+ * @param modifiablesFree map from every heap to a free modifiable term.
* @param hasMod map specifying on which heaps this contract has a modifies clause.
* @param hasFreeMod map specifying on which heaps this contract has a free modifies clause.
* @param services services.
@@ -1081,8 +1081,8 @@ public Creator(final String baseName, final StatementBlock block, final List infFlowSpecs,
final Map breaks, final Map continues, final Term returns,
final Term signals, final Term signalsOnly, final Term diverges,
- final Map assignables,
- final Map assignablesFree,
+ final Map modifiables,
+ final Map modifiablesFree,
final Map hasMod,
final Map hasFreeMod,
final Services services) {
@@ -1105,8 +1105,8 @@ public Creator(final String baseName, final StatementBlock block, final List buildModifiesClauses() {
- return assignables;
+ return modifiables;
}
/**
@@ -1436,7 +1436,7 @@ private Map buildModifiesClauses() {
* @return the contract's free modifies clauses.
*/
private Map buildFreeModifiesClauses() {
- return assignablesFree;
+ return modifiablesFree;
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java
index 9307017e160..7f0646a25f0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java
@@ -436,9 +436,9 @@ Term getFreeModifiesClause(LocationVariable heapVariable, Term heap, Term self,
/**
*
* @param heap the heap to use.
- * @return this contract's assignable term on the specified heap.
+ * @return this contract's modifiable term on the specified heap.
*/
- Term getAssignable(LocationVariable heap);
+ Term getModifiable(LocationVariable heap);
/**
* Accepts a visitor.
@@ -656,7 +656,7 @@ class Variables {
public final Map remembranceHeaps;
/**
- * A map from every variable {@code var} that is assignable inside the block to
+ * A map from every variable {@code var} that is modifiable inside the block to
* {@code var_Before_BLOCK}.
*/
public final Map remembranceLocalVariables;
@@ -693,7 +693,7 @@ class Variables {
* @param exception exception variable to set when the block terminates by an uncaught
* {@code throw} statement.
* @param remembranceHeaps a map from every heap {@code heap} to {@code heap_Before_BLOCK}.
- * @param remembranceLocalVariables a map from every variable {@code var} that is assignable
+ * @param remembranceLocalVariables a map from every variable {@code var} that is modifiable
* inside the block to {@code var_Before_BLOCK}.
* @param outerRemembranceHeaps a map from every heap {@code heap} that is accessible inside
* the block to {@code heap_Before_METHOD}.
@@ -1302,7 +1302,7 @@ class Terms {
* @param exception exception variable to set when the block terminates by an uncaught
* {@code throw} statement.
* @param remembranceHeaps a map from every heap {@code heap} to {@code heap_Before_BLOCK}.
- * @param remembranceLocalVariables a map from every variable {@code var} that is assignable
+ * @param remembranceLocalVariables a map from every variable {@code var} that is modifiable
* inside the block to {@code var_Before_BLOCK}.
* @param outerRemembranceHeaps a map from every heap {@code heap} that is accessible inside
* the block to {@code heap_Before_METHOD}.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java
index c99f2a643e9..051c062ad17 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java
@@ -242,7 +242,7 @@ public static class Creator extends AbstractAuxiliaryContractImpl.Creator labels,
Term measuredBy, Map ensures,
Map ensuresFree, ImmutableList infFlowSpecs,
Map breaks, Map continues, Term returns, Term signals,
- Term signalsOnly, Term diverges, Map assignables,
- Map assignablesFree,
+ Term signalsOnly, Term diverges, Map modifiables,
+ Map modifiablesFree,
Map hasMod, Map hasFreeMod,
Services services) {
super(baseName, block, labels, method, behavior, variables,
requires, requiresFree, measuredBy, ensures, ensuresFree,
infFlowSpecs, breaks, continues, returns, signals, signalsOnly,
- diverges, assignables, assignablesFree, hasMod, hasFreeMod, services);
+ diverges, modifiables, modifiablesFree, hasMod, hasFreeMod, services);
}
@Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
index eb975315251..e1bc7f2bcb8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
@@ -31,10 +31,10 @@ public class BlockWellDefinedness extends StatementWellDefinedness {
private final BlockContract block;
private BlockWellDefinedness(String name, int id, Type type, IObserverFunction target,
- LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable,
+ LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable,
Term accessible, Condition ensures, Term mby, Term rep, BlockContract block,
TermBuilder tb) {
- super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures,
+ super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures,
mby, rep, tb);
this.block = block;
}
@@ -55,7 +55,7 @@ public BlockWellDefinedness(BlockContract block, BlockContract.Variables variabl
final LocationVariable h = getHeap();
this.block = block;
setRequires(block.getPrecondition(h, variables, services));
- setAssignable(block.hasModifiesClause(h) ? block.getAssignable(h) : TB.strictlyNothing(),
+ setModifiable(block.hasModifiesClause(h) ? block.getModifiable(h) : TB.strictlyNothing(),
services);
setEnsures(block.getPostcondition(h, variables, services));
}
@@ -63,7 +63,7 @@ public BlockWellDefinedness(BlockContract block, BlockContract.Variables variabl
@Override
public BlockWellDefinedness map(UnaryOperator op, Services services) {
return new BlockWellDefinedness(getName(), id(), type(), getTarget(), getHeap(),
- getOrigVars(), getRequires().map(op), op.apply(getAssignable()),
+ getOrigVars(), getRequires().map(op), op.apply(getModifiable()),
op.apply(getAccessible()), getEnsures().map(op), op.apply(getMby()),
op.apply(getRepresents()), block.map(op, services), services.getTermBuilder());
}
@@ -89,14 +89,14 @@ public boolean transactionApplicableContract() {
@Override
public Contract setID(int newId) {
return new BlockWellDefinedness(getName(), newId, type(), getTarget(), getHeap(),
- getOrigVars(), getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getOrigVars(), getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), getStatement(), TB);
}
@Override
public Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM) {
return new BlockWellDefinedness(getName(), id(), type(), newPM, getHeap(), getOrigVars(),
- getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), getStatement().setTarget(newKJT, newPM), TB);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
index 6a26c9dbb00..97e0f4324f2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
@@ -33,10 +33,10 @@ public final class ClassWellDefinedness extends WellDefinednessCheck {
private final ClassInvariant inv;
private ClassWellDefinedness(String name, int id, Type type, IObserverFunction target,
- LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable,
+ LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable,
Term accessible, Condition ensures, Term mby, Term rep, ClassInvariant inv,
TermBuilder tb) {
- super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures,
+ super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures,
mby, rep, tb);
this.inv = inv;
}
@@ -48,7 +48,7 @@ public ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term a
assert inv != null;
this.inv = inv;
setRequires(inv.getOriginalInv());
- setAssignable(TB.strictlyNothing(), services);
+ setModifiable(TB.strictlyNothing(), services);
setEnsures(inv.getOriginalInv());
setAccessible(accessible);
setMby(mby);
@@ -57,7 +57,7 @@ public ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term a
@Override
public ClassWellDefinedness map(UnaryOperator op, Services services) {
return new ClassWellDefinedness(getName(), id(), type(), getTarget(), getHeap(),
- getOrigVars(), getRequires().map(op), op.apply(getAssignable()),
+ getOrigVars(), getRequires().map(op), op.apply(getModifiable()),
op.apply(getAccessible()), getEnsures().map(op), op.apply(getMby()),
op.apply(getRepresents()), inv.map(op, services), services.getTermBuilder());
}
@@ -140,14 +140,14 @@ public boolean transactionApplicableContract() {
@Override
public ClassWellDefinedness setID(int newId) {
return new ClassWellDefinedness(getName(), newId, type(), getTarget(), getHeap(),
- getOrigVars(), getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getOrigVars(), getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), getInvariant(), TB);
}
@Override
public ClassWellDefinedness setTarget(KeYJavaType newKJT, IObserverFunction newPM) {
return new ClassWellDefinedness(getName(), id(), type(), newPM, getHeap(), getOrigVars(),
- getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), getInvariant().setKJT(newKJT), TB);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java
index 5fce4da8523..57e701167e4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java
@@ -149,7 +149,7 @@ Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm,
Term getRequires(LocationVariable heap);
- Term getAssignable(LocationVariable heap);
+ Term getModifiable(LocationVariable heap);
Term getAccessible(ProgramVariable heap);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java
index 254e116dfca..0716e5120b7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java
@@ -238,7 +238,7 @@ public Term getRequires(LocationVariable heap) {
}
@Override
- public Term getAssignable(LocationVariable heap) {
+ public Term getModifiable(LocationVariable heap) {
throw new UnsupportedOperationException("Not applicable for dependency contracts.");
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java
index 48c9f19fa0c..1368d978509 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java
@@ -246,8 +246,8 @@ public Term getRequires(LocationVariable heap) {
}
@Override
- public Term getAssignable(LocationVariable heap) {
- return contract.getAssignable(heap);
+ public Term getModifiable(LocationVariable heap) {
+ return contract.getModifiable(heap);
}
@Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
index a34b12930fc..41c76640f68 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
@@ -69,11 +69,11 @@ public class FunctionalOperationContractImpl implements FunctionalOperationContr
*/
final Map originalAxioms;
/**
- * The original assignable clause terms.
+ * The original modifiable clause terms.
*/
final Map originalMods;
/**
- * The original assignable_free clause terms.
+ * The original modifiable_free clause terms.
*/
final Map originalFreeMods;
final Map originalDeps;
@@ -593,7 +593,7 @@ public Term getEnsures(LocationVariable heap) {
}
@Override
- public Term getAssignable(LocationVariable heap) {
+ public Term getModifiable(LocationVariable heap) {
return originalMods.get(heap);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java
index 972089dcdbe..80ef9a56af8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java
@@ -643,7 +643,7 @@ public Term getRequires(LocationVariable heap) {
@Override
- public Term getAssignable(LocationVariable heap) {
+ public Term getModifiable(LocationVariable heap) {
return null;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
index ff2ae281ed4..9322cd366fa 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
@@ -942,8 +942,8 @@ public static class Creator extends AbstractAuxiliaryContractImpl.Creator labels,
Term measuredBy, Map ensures,
Map ensuresFree, ImmutableList infFlowSpecs,
Map breaks, Map continues, Term returns, Term signals,
- Term signalsOnly, Term diverges, Map assignables,
- Map assignablesFree,
+ Term signalsOnly, Term diverges, Map modifiables,
+ Map modifiablesFree,
Map hasMod, Map hasFreeMod,
Term decreases, Services services) {
super(baseName, block, labels, method, behavior, variables,
requires, requiresFree, measuredBy, ensures, ensuresFree,
infFlowSpecs, breaks, continues, returns, signals, signalsOnly,
- diverges, assignables, assignablesFree, hasMod, hasFreeMod, services);
+ diverges, modifiables, modifiablesFree, hasMod, hasFreeMod, services);
this.decreases = decreases;
}
@@ -989,8 +989,8 @@ public Creator(String baseName, StatementBlock block, List labels,
* termination.
* @param signalsOnly a term specifying which uncaught exceptions may occur.
* @param diverges a diverges clause.
- * @param assignables map from every heap to an assignable term.
- * @param assignablesFree map from every heap to an assignable_free term.
+ * @param modifiables map from every heap to a modifiable term.
+ * @param modifiablesFree map from every heap to a modifiable_free term.
* @param hasMod map specifying on which heaps this contract has a modifies clause.
* @param hasFreeMod map specifying on which heaps this contract has a free modifies clause.
* @param decreases the decreases term.
@@ -1002,14 +1002,14 @@ public Creator(String baseName, LoopStatement loop, List labels,
Term measuredBy, Map ensures,
Map ensuresFree, ImmutableList infFlowSpecs,
Map breaks, Map continues, Term returns, Term signals,
- Term signalsOnly, Term diverges, Map assignables,
- Map assignablesFree,
+ Term signalsOnly, Term diverges, Map modifiables,
+ Map modifiablesFree,
Map hasMod, Map hasFreeMod,
Term decreases, Services services) {
super(baseName, null, labels, method, behavior, variables,
requires, requiresFree, measuredBy, ensures, ensuresFree,
infFlowSpecs, breaks, continues, returns, signals, signalsOnly,
- diverges, assignables, assignablesFree, hasMod, hasFreeMod, services);
+ diverges, modifiables, modifiablesFree, hasMod, hasFreeMod, services);
this.loop = loop;
this.decreases = decreases;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java
index 5cc3c7d23c8..67f4212a699 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java
@@ -28,10 +28,10 @@ public class LoopWellDefinedness extends StatementWellDefinedness {
private final LoopSpecification inv;
private LoopWellDefinedness(String name, int id, Type type, IObserverFunction target,
- LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable,
+ LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable,
Term accessible, Condition ensures, Term mby, Term rep, LoopSpecification inv,
TermBuilder tb) {
- super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures,
+ super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures,
mby, rep, tb);
this.inv = inv;
}
@@ -45,7 +45,7 @@ public LoopWellDefinedness(LoopSpecification inv, ImmutableSet
this.inv = inv;
setMby(inv.getInternalVariant());
setRequires(inv.getInternalInvariants().get(h));
- setAssignable(inv.getInternalModifies().get(h), services);
+ setModifiable(inv.getInternalModifies().get(h), services);
setEnsures(inv.getInternalInvariants().get(h));
}
@@ -66,7 +66,7 @@ public LoopSpecification getStatement() {
@Override
public LoopWellDefinedness map(UnaryOperator op, Services services) {
return new LoopWellDefinedness(getName(), id(), type(), getTarget(), getHeap(),
- getOrigVars(), getRequires().map(op), op.apply(getAssignable()),
+ getOrigVars(), getRequires().map(op), op.apply(getModifiable()),
op.apply(getAccessible()), getEnsures().map(op), op.apply(getMby()),
op.apply(getRepresents()), inv.map(op, services), services.getTermBuilder());
}
@@ -79,14 +79,14 @@ public boolean transactionApplicableContract() {
@Override
public Contract setID(int newId) {
return new LoopWellDefinedness(getName(), newId, type(), getTarget(), getHeap(),
- getOrigVars(), getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getOrigVars(), getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), getStatement(), TB);
}
@Override
public Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM) {
return new LoopWellDefinedness(getName(), id(), type(), newPM, getHeap(), getOrigVars(),
- getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), getStatement().setTarget(newKJT, newPM), TB);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
index 24886682532..8e03793ea35 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
@@ -47,10 +47,10 @@ public final class MethodWellDefinedness extends WellDefinednessCheck {
private final boolean modelField;
private MethodWellDefinedness(String name, int id, Type type, IObserverFunction target,
- LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable,
+ LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable,
Term accessible, Condition ensures, Term mby, Term rep, Contract contract,
Term globalDefs, Term axiom, boolean model, TermBuilder tb) {
- super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures,
+ super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures,
mby, rep, tb);
this.contract = contract;
this.globalDefs = globalDefs;
@@ -69,8 +69,8 @@ public MethodWellDefinedness(FunctionalOperationContract contract, Services serv
final LocationVariable hPre = (LocationVariable) origVars.atPres.get(h);
setRequires(contract.getRequires(h));
- setAssignable(
- contract.hasModifiesClause(h) ? contract.getAssignable(h) : TB.strictlyNothing(),
+ setModifiable(
+ contract.hasModifiesClause(h) ? contract.getModifiable(h) : TB.strictlyNothing(),
services);
combineAccessible(contract.getAccessible(h),
hPre != null ? contract.getAccessible(hPre) : null, services);
@@ -95,7 +95,7 @@ public MethodWellDefinedness(DependencyContract contract, Services services) {
final LocationVariable hPre = (LocationVariable) contract.getOrigVars().atPres.get(h);
setRequires(contract.getRequires(h));
- setAssignable(TB.strictlyNothing(), services);
+ setModifiable(TB.strictlyNothing(), services);
combineAccessible(contract.getAccessible(h),
hPre != null ? contract.getAccessible(hPre) : null, services);
setEnsures(TB.tt());
@@ -127,7 +127,7 @@ public MethodWellDefinedness(RepresentsAxiom rep, Services services) {
final LocationVariable hPre = (LocationVariable) origVars.atPres.get(h);
setRequires(contract.getRequires(h));
- setAssignable(TB.strictlyNothing(), services);
+ setModifiable(TB.strictlyNothing(), services);
combineAccessible(contract.getAccessible(h),
hPre != null ? contract.getAccessible(hPre) : null, services);
setEnsures(TB.tt());
@@ -261,7 +261,7 @@ ImmutableList getRest() {
public MethodWellDefinedness map(UnaryOperator op, Services services) {
// TODO Auto-generated method stub
return new MethodWellDefinedness(getName(), id(), type(), getTarget(), getHeap(),
- getOrigVars(), getRequires().map(op), op.apply(getAssignable()),
+ getOrigVars(), getRequires().map(op), op.apply(getModifiable()),
op.apply(getAccessible()), getEnsures().map(op), op.apply(getMby()),
op.apply(getRepresents()), contract.map(op, services), op.apply(globalDefs),
op.apply(axiom), modelField, services.getTermBuilder());
@@ -460,14 +460,14 @@ public boolean transactionApplicableContract() {
@Override
public MethodWellDefinedness setID(int newId) {
return new MethodWellDefinedness(getName(), newId, type(), getTarget(), getHeap(),
- getOrigVars(), getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getOrigVars(), getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), contract, globalDefs, axiom, modelField(), TB);
}
@Override
public MethodWellDefinedness setTarget(KeYJavaType newKJT, IObserverFunction newPM) {
return new MethodWellDefinedness(getName(), id(), type(), newPM, getHeap(), getOrigVars(),
- getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(),
+ getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(),
getRepresents(), contract.setTarget(newKJT, newPM), globalDefs, axiom, modelField(),
TB);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java
index f4b75a2e545..fd353072fc3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java
@@ -43,9 +43,9 @@ public abstract class StatementWellDefinedness extends WellDefinednessCheck {
}
StatementWellDefinedness(String name, int id, Type type, IObserverFunction target,
- LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable,
+ LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable,
Term accessible, Condition ensures, Term mby, Term rep, TermBuilder tb) {
- super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures,
+ super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures,
mby, rep, tb);
}
@@ -189,7 +189,7 @@ public final boolean modelField() {
* A data structure to pass the needed terms for the well-definedness sequent of a jml
* statement, including the context update, pre-condition for the statement, well-formedness
* condition for the anonymous heap, well-definedness term for the statement's
- * assignable-clause, well-definedness term for other clauses in the statement and the
+ * modifiable-clause, well-definedness term for other clauses in the statement and the
* well-definedness term for the statement's post-condition with the according updates (heap of
* pre-state becomes current heap and the current heap gets anonymised) applied to it.
*
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
index 5517964de1a..ac5caf6588c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
@@ -45,7 +45,7 @@
/**
* A contract for checking the well-definedness of a jml specification element (i.e. a class
* invariant, a method contract, a model field or any jml statement), consisting of precondition,
- * assignable-clause, postcondition, accessible-clause, measured-by-clause and represents-clause.
+ * modifiable-clause, postcondition, accessible-clause, measured-by-clause and represents-clause.
*
* @author Michael Kirsten
*/
@@ -68,7 +68,7 @@ enum Type {
private final OriginalVariables origVars;
private Condition requires;
- private Term assignable;
+ private Term modifiable;
private Condition ensures;
private Term accessible;
private Term mby;
@@ -88,7 +88,7 @@ enum Type {
}
WellDefinednessCheck(String name, int id, Type type, IObserverFunction target,
- LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable,
+ LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable,
Term accessible, Condition ensures, Term mby, Term represents, TermBuilder tb) {
this.name = name;
this.id = id;
@@ -97,7 +97,7 @@ enum Type {
this.heap = heap;
this.origVars = origVars;
this.requires = requires;
- this.assignable = assignable;
+ this.modifiable = modifiable;
this.accessible = accessible;
this.ensures = ensures;
this.mby = mby;
@@ -395,17 +395,17 @@ private String getText(boolean includeHtmlMarkup, Services services) {
final boolean isInv = type().equals(Type.CLASS_INVARIANT);
final boolean isLoop = type().equals(Type.LOOP_INVARIANT);
final boolean showSig = !isInv && !modelField();
- if (getAssignable() != null && showSig) {
+ if (getModifiable() != null && showSig) {
String printMods = LogicPrinter.quickPrintTerm(
- getAssignable(null).equalsModIrrelevantTermLabels(TB.strictlyNothing()) ? TB.empty()
- : this.getAssignable(null),
+ getModifiable(null).equalsModIrrelevantTermLabels(TB.strictlyNothing()) ? TB.empty()
+ : this.getModifiable(null),
services);
mods = mods + (includeHtmlMarkup ? "" : "\n") + "mod"
+ (includeHtmlMarkup ? " " : ": ")
+ (includeHtmlMarkup ? LogicPrinter.escapeHTML(printMods, false)
: printMods.trim());
}
- if (getAssignable().equals(TB.strictlyNothing()) && showSig) {
+ if (getModifiable().equals(TB.strictlyNothing()) && showSig) {
mods = mods + (includeHtmlMarkup ? "" : "") + ", creates no new objects"
+ (includeHtmlMarkup ? " " : "");
}
@@ -727,24 +727,24 @@ final void setRequires(Term req) {
this.requires = split(req);
}
- final void setAssignable(Term ass, TermServices services) {
- this.assignable = ass;
+ final void setModifiable(Term ass, TermServices services) {
+ this.modifiable = ass;
if (ass == null || TB.strictlyNothing().equalsModIrrelevantTermLabels(ass)
|| TB.FALSE().equalsModIrrelevantTermLabels(ass)) {
- this.assignable = TB.strictlyNothing();
+ this.modifiable = TB.strictlyNothing();
} else if (TB.tt().equalsModIrrelevantTermLabels(ass)
|| TB.TRUE().equalsModIrrelevantTermLabels(ass)) {
- this.assignable = TB.allLocs();
+ this.modifiable = TB.allLocs();
}
}
- final void combineAssignable(Term ass1, Term ass2, TermServices services) {
+ final void combineModifiable(Term ass1, Term ass2, TermServices services) {
if (ass1 == null || TB.strictlyNothing().equalsModIrrelevantTermLabels(ass1)) {
- setAssignable(ass2, services);
+ setModifiable(ass2, services);
} else if (ass2 == null || TB.strictlyNothing().equalsModIrrelevantTermLabels(ass2)) {
- setAssignable(ass1, services);
+ setModifiable(ass1, services);
} else {
- setAssignable(TB.union(ass1, ass2), services);
+ setModifiable(TB.union(ass1, ass2), services);
}
}
@@ -792,8 +792,8 @@ final Type type() {
}
/**
- * Collects all remaining (implicitly or explicity) specified clauses (except for pre-condition,
- * post-condition and assignable-clause).
+ * Collects all remaining (implicitly or explicitly) specified clauses (except for
+ * pre-condition, post-condition and modifiable-clause).
*
* @return a list of all remaining clauses
*/
@@ -865,12 +865,12 @@ public WellDefinednessCheck combine(WellDefinednessCheck wdc, TermServices servi
final Term acc = wdc.replace(wdc.getAccessible(), this.getOrigVars());
setAccessible(acc);
}
- if (this.getAssignable() != null && wdc.getAssignable() != null) {
- final Term ass = wdc.replace(wdc.getAssignable(), this.getOrigVars());
- combineAssignable(ass, this.getAssignable(), services);
- } else if (wdc.getAssignable() != null) {
- final Term ass = wdc.replace(wdc.getAssignable(), this.getOrigVars());
- setAssignable(ass, services);
+ if (this.getModifiable() != null && wdc.getModifiable() != null) {
+ final Term ass = wdc.replace(wdc.getModifiable(), this.getOrigVars());
+ combineModifiable(ass, this.getModifiable(), services);
+ } else if (wdc.getModifiable() != null) {
+ final Term ass = wdc.replace(wdc.getModifiable(), this.getOrigVars());
+ setModifiable(ass, services);
}
final Condition ens = wdc.replace(wdc.getEnsures(), this.getOrigVars());
addEnsures(ens);
@@ -915,12 +915,12 @@ public static boolean isOn() {
}
/**
- * collects terms for precondition, assignable clause and other specification elements, and
+ * collects terms for precondition, modifiable clause and other specification elements, and
* postcondition and signals-clause
*/
public final POTerms createPOTerms() {
final Condition pre = this.getRequires();
- final Term mod = this.getAssignable();
+ final Term mod = this.getModifiable();
final ImmutableList rest = this.getRest();
final Condition post = this.getEnsures();
return new POTerms(pre, mod, rest, post);
@@ -991,7 +991,7 @@ public final Term getPost(final Condition post, ParsableVariable result,
/**
* Gets the necessary updates applicable to the post-condition
*
- * @param mod the assignable-clause
+ * @param mod the modifiable-clause
* @param heap the current heap variable
* @param heapAtPre the current variable for the heap of the pre-state
* @param anonHeap the anonymous heap term
@@ -1036,9 +1036,9 @@ public final Condition getRequires() {
return this.requires;
}
- public final Term getAssignable() {
- assert this.assignable != null;
- return this.assignable;
+ public final Term getModifiable() {
+ assert this.modifiable != null;
+ return this.modifiable;
}
public final Term getAccessible() {
@@ -1094,8 +1094,8 @@ public final Term getRequires(LocationVariable heap) {
}
@Override
- public final Term getAssignable(LocationVariable heap) {
- return getAssignable();
+ public final Term getModifiable(LocationVariable heap) {
+ return getModifiable();
}
@Override
@@ -1311,7 +1311,7 @@ public record TermAndFunc(Term term, Function func) {}
/**
* A data structure for storing and passing all specifications of a specification element
- * includinf pre- and post-condition, an assignable-clause and a list of all other clauses
+ * including pre- and post-condition, a modifiable-clause and a list of all other clauses
* specified.
*
* @author Michael Kirsten
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
index 7ea6299b0c0..a55d8244cc6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
@@ -398,12 +398,12 @@ public ImmutableSet extractMethodSpecs(IProgramMethod pm,
// add purity. Strict purity overrides purity.
if (isStrictlyPure || pm.isModel()) {
for (LocationVariable heap : HeapContext.getModHeaps(services, false)) {
- specCase.addClause(ASSIGNABLE, heap.name(),
+ specCase.addClause(MODIFIABLE, heap.name(),
JmlFacade.parseExpr("\\strictly_nothing"));
}
} else if (isPure) {
for (LocationVariable heap : HeapContext.getModHeaps(services, false)) {
- specCase.addClause(ASSIGNABLE, heap.name(), JmlFacade.parseExpr("\\nothing"));
+ specCase.addClause(MODIFIABLE, heap.name(), JmlFacade.parseExpr("\\nothing"));
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLoopSpec.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLoopSpec.java
index 239218a3c0e..bb8e7bcab15 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLoopSpec.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLoopSpec.java
@@ -16,7 +16,7 @@
import org.jspecify.annotations.Nullable;
/**
- * A JML loop specification (invariant, assignable clause, decreases clause, ...) in textual form.
+ * A JML loop specification (invariant, modifiable clause, decreases clause, ...) in textual form.
*/
public final class TextualJMLLoopSpec extends TextualJMLConstruct {
private LabeledParserRuleContext variant = null;
@@ -26,7 +26,7 @@ public final class TextualJMLLoopSpec extends TextualJMLConstruct {
* Heap-dependent clauses
*/
public enum ClauseHd {
- INFORMATION_FLOW, ASSIGNABLE, ASSIGNABLE_FREE, INVARIANT, INVARIANT_FREE
+ INFORMATION_FLOW, MODIFIABLE, MODIFIABLE_FREE, INVARIANT, INVARIANT_FREE
}
public TextualJMLLoopSpec(ImmutableList mods) {
@@ -67,28 +67,28 @@ private ImmutableList getList(Object key) {
return ImmutableList.fromList(seq);
}
- public ImmutableList getAssignable() {
- return getList(ClauseHd.ASSIGNABLE);
+ public ImmutableList getModifiable() {
+ return getList(ClauseHd.MODIFIABLE);
}
- public Map> getAssignables() {
- return getMap(ClauseHd.ASSIGNABLE);
+ public Map> getModifiables() {
+ return getMap(ClauseHd.MODIFIABLE);
}
- public Map> getAssignablesInit() {
- return getMapInit(ClauseHd.ASSIGNABLE);
+ public Map> getModifiablesInit() {
+ return getMapInit(ClauseHd.MODIFIABLE);
}
- public ImmutableList getAssignableFree() {
- return getList(ClauseHd.ASSIGNABLE_FREE);
+ public ImmutableList getModifiableFree() {
+ return getList(ClauseHd.MODIFIABLE_FREE);
}
- public Map> getAssignablesFree() {
- return getMap(ClauseHd.ASSIGNABLE_FREE);
+ public Map> getModifiablesFree() {
+ return getMap(ClauseHd.MODIFIABLE_FREE);
}
- public Map> getAssignablesFreeInit() {
- return getMapInit(ClauseHd.ASSIGNABLE_FREE);
+ public Map> getModifiablesFreeInit() {
+ return getMapInit(ClauseHd.MODIFIABLE_FREE);
}
public ImmutableList getInfFlowSpecs() {
@@ -156,7 +156,7 @@ public LabeledParserRuleContext getVariant() {
* (Name heap : HeapLDT.VALID_HEAP_NAMES) { it = freeInvariants.get(heap.toString()).iterator();
* while (it.hasNext()) { sb.append("free invariant<" + heap + ">: " + it.next() + "\n"); } }
* for (Name heap : HeapLDT.VALID_HEAP_NAMES) { it =
- * assignables.get(heap.toString()).iterator(); while (it.hasNext()) { sb.append("assignable<" +
+ * modifiables.get(heap.toString()).iterator(); while (it.hasNext()) { sb.append("modifiable<" +
* heap + ">: " + it.next() + "\n"); } } for (Name heap : HeapLDT.VALID_HEAP_NAMES) { it =
* infFlowSpecs.iterator(); while (it.hasNext()) { sb.append("determines<" + heap + ">: " +
* it.next() + "\n"); } } if (variant != null) { sb.append("decreases: " + variant); }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java
index 5e0b9e960fa..e9e59e50ab6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java
@@ -36,8 +36,8 @@ public ImmutableList getEnsuresFree(Name toString) {
return getList(ENSURES_FREE, toString);
}
- public ImmutableList getAssignableFree(Name toString) {
- return getList(ASSIGNABLE_FREE, toString);
+ public ImmutableList getModifiableFree(Name toString) {
+ return getList(MODIFIABLE_FREE, toString);
}
private ImmutableList getList(@NonNull ClauseHd clause,
@@ -65,8 +65,8 @@ public ImmutableList getRequires(Name heap) {
return getList(REQUIRES, heap);
}
- public ImmutableList getAssignable(Name heap) {
- return getList(ASSIGNABLE, heap);
+ public ImmutableList getModifiable(Name heap) {
+ return getList(MODIFIABLE, heap);
}
public ImmutableList getDecreases() {
@@ -85,7 +85,7 @@ public enum Clause {
* Heap-dependent clauses
*/
public enum ClauseHd {
- ACCESSIBLE, ASSIGNABLE, ASSIGNABLE_FREE, REQUIRES, REQUIRES_FREE, ENSURES, ENSURES_FREE,
+ ACCESSIBLE, MODIFIABLE, MODIFIABLE_FREE, REQUIRES, REQUIRES_FREE, ENSURES, ENSURES_FREE,
AXIOMS,
}
@@ -239,8 +239,8 @@ private ImmutableList getList(Object key) {
return ImmutableList.fromList(seq);
}
- public ImmutableList getAssignable() {
- return getList(ASSIGNABLE);
+ public ImmutableList getModifiable() {
+ return getList(MODIFIABLE);
}
public ImmutableList getEnsures() {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
index 5653bfbb809..0e0f2f4e7f4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
@@ -169,14 +169,14 @@ private ImmutableSet createInformationFlowContracts(ContractClauses cl
InformationFlowContract symbData = cf.createInformationFlowContract(
pm.getContainerType(), pm, pm.getContainerType(), Modality.DIA,
clauses.requires.get(heap), clauses.requiresFree.get(heap), clauses.measuredBy,
- clauses.assignables.get(heap), !clauses.hasMod.get(heap), progVars,
+ clauses.modifiables.get(heap), !clauses.hasMod.get(heap), progVars,
clauses.accessibles.get(heap), clauses.infFlowSpecs, false);
symbDatas = symbDatas.add(symbData);
} else if (clauses.diverges.equals(tb.tt())) {
InformationFlowContract symbData = cf.createInformationFlowContract(
pm.getContainerType(), pm, pm.getContainerType(), Modality.BOX,
clauses.requires.get(heap), clauses.requiresFree.get(heap), clauses.measuredBy,
- clauses.assignables.get(heap), !clauses.hasMod.get(heap), progVars,
+ clauses.modifiables.get(heap), !clauses.hasMod.get(heap), progVars,
clauses.accessibles.get(heap), clauses.infFlowSpecs, false);
symbDatas = symbDatas.add(symbData);
} else {
@@ -184,12 +184,12 @@ private ImmutableSet createInformationFlowContracts(ContractClauses cl
pm.getContainerType(), pm, pm.getContainerType(), Modality.DIA,
tb.and(clauses.requires.get(heap), tb.not(clauses.diverges)),
clauses.requiresFree.get(heap), clauses.measuredBy,
- clauses.assignables.get(heap), !clauses.hasMod.get(heap), progVars,
+ clauses.modifiables.get(heap), !clauses.hasMod.get(heap), progVars,
clauses.accessibles.get(heap), clauses.infFlowSpecs, false);
InformationFlowContract symbData2 = cf.createInformationFlowContract(
pm.getContainerType(), pm, pm.getContainerType(), Modality.BOX,
clauses.requires.get(heap), clauses.requiresFree.get(heap), clauses.measuredBy,
- clauses.assignables.get(heap), !clauses.hasMod.get(heap), progVars,
+ clauses.modifiables.get(heap), !clauses.hasMod.get(heap), progVars,
clauses.accessibles.get(heap), clauses.infFlowSpecs, false);
symbDatas = symbDatas.add(symbData1).add(symbData2);
}
@@ -206,8 +206,8 @@ public static class ContractClauses {
public final Map requiresFree = new LinkedHashMap<>();
public Term measuredBy;
public Term decreases;
- public final Map assignables = new LinkedHashMap<>();
- public final Map assignablesFree = new LinkedHashMap<>();
+ public final Map modifiables = new LinkedHashMap<>();
+ public final Map modifiablesFree = new LinkedHashMap<>();
public final Map accessibles = new LinkedHashMap<>();
public final Map ensures = new LinkedHashMap<>();
public final Map ensuresFree = new LinkedHashMap<>();
@@ -366,9 +366,9 @@ private ContractClauses translateJMLClauses(TextualJMLSpecCase textualSpecCase,
progVars.atBefores, textualSpecCase.getDecreases());
for (LocationVariable heap : services.getTypeConverter().getHeapLDT().getAllHeaps()) {
- translateAssignable(context, progVars, heap, savedHeap,
- textualSpecCase.getAssignable(heap.name()),
- textualSpecCase.getAssignableFree(heap.name()), clauses);
+ translateModifiable(context, progVars, heap, savedHeap,
+ textualSpecCase.getModifiable(heap.name()),
+ textualSpecCase.getModifiableFree(heap.name()), clauses);
translateRequires(context, progVars, heap, savedHeap,
textualSpecCase.getRequires(heap.name()),
textualSpecCase.getRequiresFree(heap.name()), clauses);
@@ -411,9 +411,9 @@ private void translateAccessible(Context context, ProgramVariableCollection prog
clauses.accessibles.put(heap, null);
clauses.accessibles.put(heapAtPre, null);
} else {
- clauses.accessibles.put(heap, translateAssignable(context, progVars.paramVars,
+ clauses.accessibles.put(heap, translateModifiable(context, progVars.paramVars,
progVars.atPres, progVars.atBefores, accessible));
- clauses.accessibles.put(heapAtPre, translateAssignable(context, progVars.paramVars,
+ clauses.accessibles.put(heapAtPre, translateModifiable(context, progVars.paramVars,
progVars.atPres, progVars.atBefores, accessiblePre));
}
}
@@ -476,46 +476,46 @@ private void translateRequires(Context context, ProgramVariableCollection progVa
}
}
- private void translateAssignable(Context context, ProgramVariableCollection progVars,
+ private void translateModifiable(Context context, ProgramVariableCollection progVars,
LocationVariable heap, final LocationVariable savedHeap,
final ImmutableList mod,
final ImmutableList modFree, ContractClauses clauses)
throws SLTranslationException {
clauses.hasMod.put(heap, !translateStrictlyPure(context, progVars.paramVars, mod));
- // For assignable_free, the default if there is no modFree term is strictly_nothing.
+ // For modifiable_free, the default if there is no modFree term is strictly_nothing.
clauses.hasFreeMod.put(heap,
!modFree.isEmpty() && !translateStrictlyPure(context, progVars.paramVars, modFree));
if (heap == savedHeap && mod.isEmpty()) {
- clauses.assignables.put(heap, null);
+ clauses.modifiables.put(heap, null);
} else {
final Boolean hasMod = clauses.hasMod.get(heap);
if (hasMod == null || !hasMod) {
- final ImmutableList assignableNothing =
- ImmutableSLList.nil().append(getAssignableNothing());
- clauses.assignables.put(heap, translateAssignable(context, progVars.paramVars,
- progVars.atPres, progVars.atBefores, assignableNothing));
+ final ImmutableList modifiableNothing =
+ ImmutableSLList.nil().append(getModifiableNothing());
+ clauses.modifiables.put(heap, translateModifiable(context, progVars.paramVars,
+ progVars.atPres, progVars.atBefores, modifiableNothing));
} else {
- clauses.assignables.put(heap, translateAssignable(context, progVars.paramVars,
+ clauses.modifiables.put(heap, translateModifiable(context, progVars.paramVars,
progVars.atPres, progVars.atBefores, mod));
}
}
if (heap == savedHeap && modFree.isEmpty()) {
- clauses.assignablesFree.put(heap, null);
+ clauses.modifiablesFree.put(heap, null);
} else {
final Boolean hasFreeMod = clauses.hasFreeMod.get(heap);
if (hasFreeMod == null || !hasFreeMod) {
- final ImmutableList assignableFreeNothing =
+ final ImmutableList modifiableFreeNothing =
ImmutableSLList
- .nil().append(getAssignableFreeNothing());
- clauses.assignablesFree.put(heap,
- translateAssignableFree(context, progVars.paramVars,
- progVars.atPres, progVars.atBefores, assignableFreeNothing));
+ .nil().append(getModifiableFreeNothing());
+ clauses.modifiablesFree.put(heap,
+ translateModifiableFree(context, progVars.paramVars,
+ progVars.atPres, progVars.atBefores, modifiableFreeNothing));
} else {
- clauses.assignablesFree.put(heap,
- translateAssignableFree(context, progVars.paramVars,
+ clauses.modifiablesFree.put(heap,
+ translateModifiableFree(context, progVars.paramVars,
progVars.atPres, progVars.atBefores, modFree));
}
}
@@ -523,14 +523,14 @@ private void translateAssignable(Context context, ProgramVariableCollection prog
}
@NonNull
- private LabeledParserRuleContext getAssignableNothing() {
- return new LabeledParserRuleContext(JmlFacade.parseClause("assignable \\nothing;"),
+ private LabeledParserRuleContext getModifiableNothing() {
+ return new LabeledParserRuleContext(JmlFacade.parseClause("modifiable \\nothing;"),
ParameterlessTermLabel.IMPLICIT_SPECIFICATION_LABEL);
}
@NonNull
- private LabeledParserRuleContext getAssignableFreeNothing() {
- return new LabeledParserRuleContext(JmlFacade.parseClause("assignable_free \\nothing;"),
+ private LabeledParserRuleContext getModifiableFreeNothing() {
+ return new LabeledParserRuleContext(JmlFacade.parseClause("modifiable_free \\nothing;"),
ParameterlessTermLabel.IMPLICIT_SPECIFICATION_LABEL);
}
@@ -628,8 +628,8 @@ private Term translateUnionClauses(Context context, ImmutableList 1) {
throw new SLTranslationException(
- "\"assignable \\less_than_nothing\" does not go with other "
- + "assignable clauses (even if they declare the same).",
+ "\"modifiable \\less_than_nothing\" does not go with other "
+ + "modifiable clauses (even if they declare the same).",
Location.fromToken(expr.first.start));
}
return tb.empty();
@@ -738,7 +738,7 @@ private Term translateAccessible(Context context, ImmutableList
}
}
- private Term translateAssignable(Context context, ImmutableList paramVars,
+ private Term translateModifiable(Context context, ImmutableList paramVars,
Map atPres, Map atBefores,
ImmutableList originalClauses) throws SLTranslationException {
@@ -746,24 +746,24 @@ private Term translateAssignable(Context context, ImmutableList
return tb.allLocs();
} else {
return translateUnionClauses(context, paramVars, atPres, atBefores, originalClauses,
- SpecType.ASSIGNABLE);
+ SpecType.MODIFIABLE);
}
}
- private Term translateAssignableFree(Context context, ImmutableList paramVars,
+ private Term translateModifiableFree(Context context, ImmutableList paramVars,
Map atPres, Map atBefores,
ImmutableList originalClauses) throws SLTranslationException {
- // If originalClauses.isEmpty, the default value for assignable_free is strictly_nothing,
+ // If originalClauses.isEmpty, the default value for modifiable_free is strictly_nothing,
// which cannot be represented by a LocSet term.
assert !originalClauses.isEmpty();
return translateUnionClauses(context, paramVars, atPres, atBefores, originalClauses,
- SpecType.ASSIGNABLE_FREE);
+ SpecType.MODIFIABLE_FREE);
}
private boolean translateStrictlyPure(Context context, ImmutableList paramVars,
- ImmutableList assignableClauses) {
+ ImmutableList modifiableClauses) {
- for (LabeledParserRuleContext expr : assignableClauses) {
+ for (LabeledParserRuleContext expr : modifiableClauses) {
Term translated =
new JmlIO(services).context(context).parameters(paramVars).translateTerm(expr);
@@ -854,7 +854,7 @@ private Map generatePostCondition(ProgramVariableCollect
result.put(heap, post);
} else {
- if (clauses.assignables.get(heap) != null) {
+ if (clauses.modifiables.get(heap) != null) {
result.put(heap, tb.tt());
}
}
@@ -901,7 +901,7 @@ public ImmutableSet createFunctionalOperationContracts(String name, IP
Term pre = tb.convertToFormula(clauses.requires.get(heap));
pres.put(heap, pre);
} else {
- if (clauses.assignables.get(heap) != null) {
+ if (clauses.modifiables.get(heap) != null) {
pres.put(heap, tb.tt());
}
}
@@ -912,7 +912,7 @@ public ImmutableSet createFunctionalOperationContracts(String name, IP
// create diamond modality contract
FunctionalOperationContract contract = cf.func(name, pm, true, pres,
clauses.requiresFree, clauses.measuredBy, posts, clauses.ensuresFree, axioms,
- clauses.assignables, clauses.assignablesFree, clauses.accessibles, clauses.hasMod,
+ clauses.modifiables, clauses.modifiablesFree, clauses.accessibles, clauses.hasMod,
clauses.hasFreeMod, progVars);
contract = cf.addGlobalDefs(contract, abbrvLhs);
result = result.add(contract);
@@ -920,7 +920,7 @@ public ImmutableSet createFunctionalOperationContracts(String name, IP
// create box modality contract
FunctionalOperationContract contract = cf.func(name, pm, false, pres,
clauses.requiresFree, clauses.measuredBy, posts, clauses.ensuresFree, axioms,
- clauses.assignables, clauses.assignablesFree, clauses.accessibles, clauses.hasMod,
+ clauses.modifiables, clauses.modifiablesFree, clauses.accessibles, clauses.hasMod,
clauses.hasFreeMod, progVars);
contract = cf.addGlobalDefs(contract, abbrvLhs);
result = result.add(contract);
@@ -935,12 +935,12 @@ public ImmutableSet createFunctionalOperationContracts(String name, IP
}
FunctionalOperationContract contract1 = cf.func(name, pm, true, pres,
clauses.requiresFree, clauses.measuredBy, posts, clauses.ensuresFree, axioms,
- clauses.assignables, clauses.assignablesFree, clauses.accessibles, clauses.hasMod,
+ clauses.modifiables, clauses.modifiablesFree, clauses.accessibles, clauses.hasMod,
clauses.hasFreeMod, progVars);
contract1 = cf.addGlobalDefs(contract1, abbrvLhs);
FunctionalOperationContract contract2 = cf.func(name, pm, false, clauses.requires,
clauses.requiresFree, clauses.measuredBy, posts, clauses.ensuresFree, axioms,
- clauses.assignables, clauses.assignablesFree, clauses.accessibles, clauses.hasMod,
+ clauses.modifiables, clauses.modifiablesFree, clauses.accessibles, clauses.hasMod,
clauses.hasFreeMod, progVars);
contract2 = cf.addGlobalDefs(contract2, abbrvLhs);
result = result.add(contract1).add(contract2);
@@ -1309,7 +1309,7 @@ public ImmutableSet createJMLBlockContracts(IProgramMethod method
method, behavior, variables, clauses.requires, clauses.requiresFree, clauses.measuredBy,
clauses.ensures, clauses.ensuresFree, clauses.infFlowSpecs, clauses.breaks,
clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly,
- clauses.diverges, clauses.assignables, clauses.assignablesFree,
+ clauses.diverges, clauses.modifiables, clauses.modifiablesFree,
clauses.hasMod, clauses.hasFreeMod, services).create();
}
@@ -1342,7 +1342,7 @@ public ImmutableSet createJMLLoopContracts(final IProgramMethod me
method, behavior, variables, clauses.requires, clauses.requiresFree, clauses.measuredBy,
clauses.ensures, clauses.ensuresFree, clauses.infFlowSpecs, clauses.breaks,
clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly,
- clauses.diverges, clauses.assignables, clauses.assignablesFree, clauses.hasMod,
+ clauses.diverges, clauses.modifiables, clauses.modifiablesFree, clauses.hasMod,
clauses.hasFreeMod, clauses.decreases, services)
.create();
}
@@ -1377,7 +1377,7 @@ public ImmutableSet createJMLLoopContracts(IProgramMethod method,
method, behavior, variables, clauses.requires, clauses.requiresFree, clauses.measuredBy,
clauses.ensures, clauses.ensuresFree, clauses.infFlowSpecs, clauses.breaks,
clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly,
- clauses.diverges, clauses.assignables, clauses.assignablesFree, clauses.hasMod,
+ clauses.diverges, clauses.modifiables, clauses.modifiablesFree, clauses.hasMod,
clauses.hasFreeMod, clauses.decreases, services)
.create();
}
@@ -1514,14 +1514,14 @@ private ImmutableList collectLocalVariablesVisibleTo(Statement
private LoopSpecification createJMLLoopInvariant(IProgramMethod pm, LoopStatement loop,
Map> originalInvariants,
Map> originalFreeInvariants,
- Map> originalAssignables,
- Map> originalFreeAssignables,
+ Map> originalModifiables,
+ Map> originalFreeModifiables,
ImmutableList originalInfFlowSpecs,
LabeledParserRuleContext originalVariant) {
assert pm != null;
assert loop != null;
assert originalInvariants != null;
- assert originalAssignables != null;
+ assert originalModifiables != null;
assert originalInfFlowSpecs != null;
// create variables for self, parameters, other relevant local variables
@@ -1548,11 +1548,11 @@ private LoopSpecification createJMLLoopInvariant(IProgramMethod pm, LoopStatemen
Map freeInvariants = translateToTermFreeInvariants(context,
originalFreeInvariants, allVars, allHeaps, atPres, services, tb);
- // translateToTerm assignable
+ // translateToTerm modifiable
Map mods =
- translateToTermAssignable(context, atPres, allVars, originalAssignables, false);
+ translateToTermModifiable(context, atPres, allVars, originalModifiables, false);
Map freeMods =
- translateToTermAssignable(context, atPres, allVars, originalFreeAssignables, true);
+ translateToTermModifiable(context, atPres, allVars, originalFreeModifiables, true);
// translateToTerm infFlowSpecs
@@ -1604,19 +1604,19 @@ private Map> translateToTermInfFlow
return infFlowSpecs;
}
- private Map translateToTermAssignable(Context context,
+ private Map translateToTermModifiable(Context context,
Map atPres, ImmutableList allVars,
- Map> originalAssignables,
+ Map> originalModifiables,
boolean free) {
Map mods = new LinkedHashMap<>();
- for (String h : originalAssignables.keySet()) {
+ for (String h : originalModifiables.keySet()) {
LocationVariable heap =
services.getTypeConverter().getHeapLDT().getHeapForName(new Name(h));
if (heap == null) {
continue;
}
Term a;
- ImmutableList as = originalAssignables.get(h);
+ ImmutableList as = originalModifiables.get(h);
if (as.isEmpty()) {
if (free) {
a = tb.strictlyNothing();
@@ -1629,7 +1629,7 @@ private Map translateToTermAssignable(Context context,
Term translated =
new JmlIO(services).context(context).parameters(allVars).atPres(atPres)
.atBefore(atPres).translateTerm(expr,
- free ? SpecType.ASSIGNABLE_FREE : SpecType.ASSIGNABLE);
+ free ? SpecType.MODIFIABLE_FREE : SpecType.MODIFIABLE);
a = tb.union(a, translated);
}
}
@@ -1653,8 +1653,8 @@ private ImmutableList append(ImmutableList loc
public LoopSpecification createJMLLoopInvariant(IProgramMethod pm, LoopStatement loop,
TextualJMLLoopSpec textualLoopSpec) {
return createJMLLoopInvariant(pm, loop, textualLoopSpec.getInvariants(),
- textualLoopSpec.getFreeInvariants(), textualLoopSpec.getAssignablesInit(),
- textualLoopSpec.getAssignablesFreeInit(), textualLoopSpec.getInfFlowSpecs(),
+ textualLoopSpec.getFreeInvariants(), textualLoopSpec.getModifiablesInit(),
+ textualLoopSpec.getModifiablesFreeInit(), textualLoopSpec.getInfFlowSpecs(),
textualLoopSpec.getVariant());
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/ContractClauses.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/ContractClauses.java
index b3070b6ea1f..192e44f07d2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/ContractClauses.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/ContractClauses.java
@@ -27,7 +27,7 @@ class ContractClauses {
static final Clauses BREAKS = new Clauses<>();
static final Clauses CONTINUES = new Clauses<>();
- static final Clauses ASSIGNABLE = new Clauses<>();
+ static final Clauses MODIFIABLE = new Clauses<>();
static final Clauses ACCESSIBLE = new Clauses<>();
static final Clauses ENSURES = new Clauses<>();
static final Clauses ENSURES_FREE = new Clauses<>();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
index 5fba719ee4b..2783e1e5d37 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
@@ -920,14 +920,14 @@ public Term createLocSet(ImmutableList exprList) {
singletons = singletons.append(t);
} else if (t.op() instanceof ProgramVariable) {
// this case may happen with local variables
- exc.addIgnoreWarning("local variable in assignable clause");
+ exc.addIgnoreWarning("local variable in modifiable clause");
LOGGER.debug("Can't create a locset from local variable " + t + ".\n"
- + "In this version of KeY, you do not need to put them in assignable clauses.");
+ + "In this version of KeY, you do not need to put them in modifiable clauses.");
} else {
- throw exc.createException0("Can't create a locset from " + t + ".");
+ throw exc.createException0("Cannot create a locset from " + t + ".");
}
} else {
- throw exc.createException0("Can't create a locset of a singleton: " + expr);
+ throw exc.createException0("Cannot create a locset of a singleton: " + expr);
}
} else {
throw exc.createException0("Not a term: " + expr);
@@ -1053,7 +1053,7 @@ public Triple depends(SLExpression lhs, Term rhs,
}
- public Term assignable(@NonNull Term term) {
+ public Term modifiable(@NonNull Term term) {
return accessible(term);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index 975ede713e9..c12f87f1220 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -253,23 +253,23 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
}
@Override
- public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
+ public Object visitModifiable_clause(JmlParser.Modifiable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
final boolean isFree =
- ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free");
+ ctx.MODIFIABLE() != null && ctx.MODIFIABLE().getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
- ? OriginTermLabel.SpecType.ASSIGNABLE_FREE
- : OriginTermLabel.SpecType.ASSIGNABLE,
+ ? OriginTermLabel.SpecType.MODIFIABLE_FREE
+ : OriginTermLabel.SpecType.MODIFIABLE,
attachOriginLabel);
for (Name heap : heaps) {
if (methodContract != null) {
- methodContract.addClause(isFree ? ASSIGNABLE_FREE : ASSIGNABLE, heap, ctx2);
+ methodContract.addClause(isFree ? MODIFIABLE_FREE : MODIFIABLE, heap, ctx2);
}
if (loopContract != null) {
loopContract.addClause(
- isFree ? TextualJMLLoopSpec.ClauseHd.ASSIGNABLE_FREE
- : TextualJMLLoopSpec.ClauseHd.ASSIGNABLE,
+ isFree ? TextualJMLLoopSpec.ClauseHd.MODIFIABLE_FREE
+ : TextualJMLLoopSpec.ClauseHd.MODIFIABLE,
heap, ctx2);
}
}
@@ -277,20 +277,20 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
}
@Override
- public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
+ public Object visitLoop_modifiable_clause(JmlParser.Loop_modifiable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
final boolean isFree =
- ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free");
+ ctx.MODIFIABLE() != null && ctx.MODIFIABLE().getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
- ? OriginTermLabel.SpecType.ASSIGNABLE_FREE
- : OriginTermLabel.SpecType.ASSIGNABLE,
+ ? OriginTermLabel.SpecType.MODIFIABLE_FREE
+ : OriginTermLabel.SpecType.MODIFIABLE,
attachOriginLabel);
for (Name heap : heaps) {
if (loopContract != null) {
loopContract.addClause(
- isFree ? TextualJMLLoopSpec.ClauseHd.ASSIGNABLE_FREE
- : TextualJMLLoopSpec.ClauseHd.ASSIGNABLE,
+ isFree ? TextualJMLLoopSpec.ClauseHd.MODIFIABLE_FREE
+ : TextualJMLLoopSpec.ClauseHd.MODIFIABLE,
heap, ctx2);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index 90c2c438552..ac8fc7b0ee6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -1991,7 +1991,7 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
}
@Override
- public SLExpression visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) {
+ public SLExpression visitModifiable_clause(JmlParser.Modifiable_clauseContext ctx) {
Term t;
LocationVariable[] heaps = visitTargetHeap(ctx.targetHeap());
if (ctx.STRICTLY_NOTHING() != null) {
@@ -1999,16 +1999,16 @@ public SLExpression visitAssignable_clause(JmlParser.Assignable_clauseContext ct
} else {
final Term storeRef = accept(ctx.storeRefUnion());
assert storeRef != null;
- t = termFactory.assignable(storeRef);
+ t = termFactory.modifiable(storeRef);
}
for (LocationVariable heap : heaps) {
- contractClauses.add(ContractClauses.ASSIGNABLE, heap, t);
+ contractClauses.add(ContractClauses.MODIFIABLE, heap, t);
}
return new SLExpression(t);
}
@Override
- public SLExpression visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) {
+ public SLExpression visitLoop_modifiable_clause(JmlParser.Loop_modifiable_clauseContext ctx) {
Term t;
LocationVariable[] heaps = visitTargetHeap(ctx.targetHeap());
if (ctx.STRICTLY_NOTHING() != null) {
@@ -2016,10 +2016,10 @@ public SLExpression visitLoop_assignable_clause(JmlParser.Loop_assignable_clause
} else {
final Term storeRef = accept(ctx.storeRefUnion());
assert storeRef != null;
- t = termFactory.assignable(storeRef);
+ t = termFactory.modifiable(storeRef);
}
for (LocationVariable heap : heaps) {
- contractClauses.add(ContractClauses.ASSIGNABLE, heap, t);
+ contractClauses.add(ContractClauses.MODIFIABLE, heap, t);
}
return new SLExpression(t);
}
diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java
index 9633474126f..67cd6fd5597 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java
@@ -73,7 +73,7 @@ public synchronized void setUp() {
* @throws SLTranslationException is not thrown if the test succeeds
*/
@Test
- public void testCombineEqualAssignable() throws SLTranslationException {
+ public void testCombineEqualModifiable() throws SLTranslationException {
String contract = """
/*@ normal_behavior
@ requires a != 5;
@@ -99,7 +99,7 @@ public void testCombineEqualAssignable() throws SLTranslationException {
* @throws SLTranslationException is not thrown if test succeeds
*/
@Test
- public void testCombineEmptyAssignable() throws SLTranslationException {
+ public void testCombineEmptyModifiable() throws SLTranslationException {
String contract = """
/*@ normal_behavior
@ requires a != 5;
@@ -125,7 +125,7 @@ public void testCombineEmptyAssignable() throws SLTranslationException {
* @throws SLTranslationException is not thrown if test succeeds
*/
@Test
- public void testCombineDifferentAssignable() throws SLTranslationException {
+ public void testCombineDifferentModifiable() throws SLTranslationException {
String contract = """
/*@ normal_behavior
@ requires a != 5;
diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
index 39259c24443..60d7d008569 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
@@ -148,7 +148,7 @@ public void testSimpleSpec() {
Assertions.assertSame(Behavior.NORMAL_BEHAVIOR, specCase.getBehavior());
Assertions.assertEquals(1, specCase.getRequires().size());
- Assertions.assertEquals(0, specCase.getAssignable().size());
+ Assertions.assertEquals(0, specCase.getModifiable().size());
Assertions.assertEquals(0, specCase.getEnsures().size());
Assertions.assertEquals(0, specCase.getSignals().size());
Assertions.assertEquals(0, specCase.getSignalsOnly().size());
@@ -177,7 +177,7 @@ public void testComplexSpec() {
Assertions.assertSame(Behavior.BEHAVIOR, specCase.getBehavior());
Assertions.assertEquals(2, specCase.getRequires().size());
- Assertions.assertEquals(1, specCase.getAssignable().size());
+ Assertions.assertEquals(1, specCase.getModifiable().size());
Assertions.assertEquals(1, specCase.getEnsures().size());
Assertions.assertEquals(1, specCase.getSignals().size());
Assertions.assertEquals(1, specCase.getSignalsOnly().size());
@@ -187,7 +187,7 @@ public void testComplexSpec() {
Assertions.assertEquals("ensuresfalse;",
specCase.getEnsures().head().first.getText().trim());
Assertions.assertEquals("assignable\\nothing;",
- specCase.getAssignable().head().first.getText().trim());
+ specCase.getModifiable().head().first.getText().trim());
Assertions.assertEquals("signals(Exception)e;",
specCase.getSignals().head().first.getText().trim());
Assertions.assertEquals("signals_onlyonlythis;",
@@ -219,14 +219,14 @@ public void testMultipleSpecs() {
Assertions.assertSame(Behavior.NORMAL_BEHAVIOR, specCase1.getBehavior());
Assertions.assertEquals(0, specCase1.getRequires().size());
- Assertions.assertEquals(1, specCase1.getAssignable().size());
+ Assertions.assertEquals(1, specCase1.getModifiable().size());
Assertions.assertEquals(1, specCase1.getEnsures().size());
Assertions.assertEquals(0, specCase1.getSignals().size());
Assertions.assertEquals(0, specCase1.getSignalsOnly().size());
Assertions.assertSame(Behavior.EXCEPTIONAL_BEHAVIOR, specCase2.getBehavior());
Assertions.assertEquals(1, specCase2.getRequires().size());
- Assertions.assertEquals(0, specCase2.getAssignable().size());
+ Assertions.assertEquals(0, specCase2.getModifiable().size());
Assertions.assertEquals(0, specCase2.getEnsures().size());
Assertions.assertEquals(1, specCase2.getSignals().size());
Assertions.assertEquals(0, specCase2.getSignalsOnly().size());
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
index 8eefe1e7c83..327a0866140 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
@@ -163,8 +163,7 @@ private enum CommentState {
"spec_safe_math", "static", "strictfp", "strictly_pure", "synchronized", "transient",
"two_state", "uninitialized", "volatile",
- "no_state", "modifies", "modifying", "erases", "modifiable", "returns", "break_behavior",
- "continue_behavior", "return_behavior",
+ "no_state", "erases", "returns", "break_behavior", "continue_behavior", "return_behavior",
// special JML expressions:
"\\constraint_for", "\\created", "\\disjoint", "\\duration", "\\everything", "\\exception",
"\\exists", "\\forall", "\\fresh", "\\index", "\\invariant_for", "\\is_initialized",
@@ -179,6 +178,8 @@ private enum CommentState {
"accessible", "accessible_redundantly", "assert", "assert_redundantly",
"assignable", "assignable_free", "assignable_redundantly", "assigns", "assigns_free",
"assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly",
+ "modifiable", "modifiable_free", "modifiable_redundantly", "modifies", "modifies_free",
+ "modifies_redundantly", "modifying", "modifying_free", "modifying_redundantly",
"loop_assignable", "loop_assignable_free", "loop_assignable_redundantly", "loop_assigns",
"loop_assigns_free", "loop_assigns_redundantly", "loop_assigning", "loop_assigning_free",
"loop_assigning_redundantly", "loop_modifiable", "loop_modifiable_free",
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
index 54e6a1b9bf5..f1aabfc5199 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
@@ -858,7 +858,7 @@ private static String collectPathInformation(Node node) {
node = node.parent();
}
// if no label was found we have to prove the postcondition
- return "Show Postcondition/Assignable";
+ return "Show Postcondition/Modifiable";
}
/**
From cadb96a00482dbdf6646be1262ad71dd5c4b3f48 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Thu, 29 Feb 2024 19:16:28 +0100
Subject: [PATCH 12/40] Added warning for potentially dangerous aliases of
modifiable.
---
.../jml/translation/JMLSpecFactory.java | 2 +-
.../ilkd/key/speclang/njml/Translator.java | 21 +++++++++++++++++++
2 files changed, 22 insertions(+), 1 deletion(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
index 0e0f2f4e7f4..6c0875f566e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
@@ -628,7 +628,7 @@ private Term translateUnionClauses(Context context, ImmutableList 1) {
throw new SLTranslationException(
- "\"modifiable \\less_than_nothing\" does not go with other "
+ "\"modifiable \\less_than_nothing\" cannot be joined with other "
+ "modifiable clauses (even if they declare the same).",
Location.fromToken(expr.first.start));
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index ac8fc7b0ee6..1808ce4eead 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -65,6 +65,9 @@
*/
class Translator extends JmlParserBaseVisitor {
+ private static String[] DISCOURAGED_CLAUSE_NAMES =
+ { "assigning", "assigns", "modifying", "modifies", "writing", "writes",};
+
private final Services services;
private final TermBuilder tb;
private final JavaInfo javaInfo;
@@ -1994,6 +1997,7 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
public SLExpression visitModifiable_clause(JmlParser.Modifiable_clauseContext ctx) {
Term t;
LocationVariable[] heaps = visitTargetHeap(ctx.targetHeap());
+ warnPotentiallyUnintendedFramingSemantics(ctx, ctx.MODIFIABLE().getText());
if (ctx.STRICTLY_NOTHING() != null) {
t = tb.strictlyNothing();
} else {
@@ -2011,6 +2015,7 @@ public SLExpression visitModifiable_clause(JmlParser.Modifiable_clauseContext ct
public SLExpression visitLoop_modifiable_clause(JmlParser.Loop_modifiable_clauseContext ctx) {
Term t;
LocationVariable[] heaps = visitTargetHeap(ctx.targetHeap());
+ warnPotentiallyUnintendedFramingSemantics(ctx, ctx.MODIFIABLE().getText());
if (ctx.STRICTLY_NOTHING() != null) {
t = tb.strictlyNothing();
} else {
@@ -2546,6 +2551,22 @@ protected void addWarning(ParserRuleContext node, String description) {
exc.addWarning(description, node.start);
}
+ private void warnPotentiallyUnintendedFramingSemantics(JmlParser.ParserRuleContext ctx,
+ String clauseName) {
+ clauseName =
+ clauseName.startsWith("loop_") ? clauseName.replaceFirst("loop_", "") : clauseName;
+ for (final String s: DISCOURAGED_CLAUSE_NAMES) { // FIXME
+ if (clauseName != null && clauseName.startsWith(s)) {
+ addWarning(ctx, clauseName + " does not conform to KeY's supported JML language, "
+ + "but is interpreted by KeY as modifiable-clause in order to deal with "
+ + "other JML-like languages. "
+ + "However, this interpretation may not correspond to the semantics "
+ + "actually intended by you. Please consult KeY's official documentation "
+ + "of the modifiable-clause.");
+ }
+ }
+ }
+
public List getWarnings() {
return exc.getWarnings();
}
From 02e719a4729a245124066c8dcb94246d50f66546 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Thu, 29 Feb 2024 19:22:32 +0100
Subject: [PATCH 13/40] Fixed parameter type within translator warning
---
.../src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index 0413f57758b..c14141beefa 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -2552,7 +2552,7 @@ protected void addWarning(ParserRuleContext node, String description) {
exc.addWarning(description, node.start);
}
- private void warnPotentiallyUnintendedFramingSemantics(JmlParser.ParserRuleContext ctx,
+ private void warnPotentiallyUnintendedFramingSemantics(ParserRuleContext ctx,
String clauseName) {
clauseName =
clauseName.startsWith("loop_") ? clauseName.replaceFirst("loop_", "") : clauseName;
From cf778c550468b7b60fe9218befcc0fc65dc909f5 Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Thu, 29 Feb 2024 19:50:48 +0100
Subject: [PATCH 14/40] Applied spotless
---
.../key/speclang/njml/TextualTranslator.java | 5 ++---
.../ilkd/key/speclang/njml/Translator.java | 20 +++++++++----------
2 files changed, 12 insertions(+), 13 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index c12f87f1220..1789bfb9e35 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -13,7 +13,6 @@
import org.antlr.v4.runtime.ParserRuleContext;
import org.antlr.v4.runtime.Token;
-import org.antlr.v4.runtime.tree.TerminalNode;
import org.jspecify.annotations.Nullable;
import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec.ClauseHd.INVARIANT;
@@ -256,7 +255,7 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) {
public Object visitModifiable_clause(JmlParser.Modifiable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
final boolean isFree =
- ctx.MODIFIABLE() != null && ctx.MODIFIABLE().getText().endsWith("_free");
+ ctx.MODIFIABLE() != null && ctx.MODIFIABLE().getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
? OriginTermLabel.SpecType.MODIFIABLE_FREE
@@ -280,7 +279,7 @@ public Object visitModifiable_clause(JmlParser.Modifiable_clauseContext ctx) {
public Object visitLoop_modifiable_clause(JmlParser.Loop_modifiable_clauseContext ctx) {
Name[] heaps = visitTargetHeap(ctx.targetHeap());
final boolean isFree =
- ctx.MODIFIABLE() != null && ctx.MODIFIABLE().getText().endsWith("_free");
+ ctx.MODIFIABLE() != null && ctx.MODIFIABLE().getText().endsWith("_free");
final LabeledParserRuleContext ctx2 =
LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree
? OriginTermLabel.SpecType.MODIFIABLE_FREE
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index c14141beefa..91937dfa665 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -66,7 +66,7 @@
class Translator extends JmlParserBaseVisitor {
private static String[] DISCOURAGED_CLAUSE_NAMES =
- { "assigning", "assigns", "modifying", "modifies", "writing", "writes",};
+ { "assigning", "assigns", "modifying", "modifies", "writing", "writes" };
private final Services services;
private final TermBuilder tb;
@@ -2552,18 +2552,18 @@ protected void addWarning(ParserRuleContext node, String description) {
exc.addWarning(description, node.start);
}
- private void warnPotentiallyUnintendedFramingSemantics(ParserRuleContext ctx,
- String clauseName) {
+ private void warnPotentiallyUnintendedFramingSemantics(
+ ParserRuleContext ctx, String clauseName) {
clauseName =
- clauseName.startsWith("loop_") ? clauseName.replaceFirst("loop_", "") : clauseName;
- for (final String s: DISCOURAGED_CLAUSE_NAMES) { // FIXME
+ clauseName.startsWith("loop_") ? clauseName.replaceFirst("loop_", "") : clauseName;
+ for (final String s : DISCOURAGED_CLAUSE_NAMES) {
if (clauseName != null && clauseName.startsWith(s)) {
addWarning(ctx, clauseName + " does not conform to KeY's supported JML language, "
- + "but is interpreted by KeY as modifiable-clause in order to deal with "
- + "other JML-like languages. "
- + "However, this interpretation may not correspond to the semantics "
- + "actually intended by you. Please consult KeY's official documentation "
- + "of the modifiable-clause.");
+ + "but is interpreted by KeY as modifiable-clause in order to deal with "
+ + "other JML-like languages. "
+ + "However, this interpretation may not correspond to the semantics "
+ + "actually intended by you. Please consult KeY's official documentation "
+ + "of the modifiable-clause.");
}
}
}
From 16f34020f24b6bfa32d8d2a742bec5660b0d9c6d Mon Sep 17 00:00:00 2001
From: Michael Kirsten
Date: Fri, 1 Mar 2024 18:17:26 +0100
Subject: [PATCH 15/40] Integrated reviewer feedback
---
.../BlockContractModifiableEverything.xml} | 6 +--
.../BlockContractModifiableEverything.java} | 6 +--
.../BlockContractModifiableEverything.proof} | 6 +--
...ontractModifiableLocationNotRequested.xml} | 6 +--
...ntractModifiableLocationNotRequested.java} | 6 +--
...tractModifiableLocationNotRequested.proof} | 6 +--
...ckContractModifiableRequestedLocation.xml} | 8 +--
...kContractModifiableRequestedLocation.java} | 6 +--
...ContractModifiableRequestedLocation.proof} | 6 +--
... InstanceContractTest_mainExceptional.xml} | 10 ++--
...nceContractTest_mainExceptionalUnused.xml} | 8 +--
...tanceContractTest_mainExceptionalVoid.xml} | 6 +--
.../test/InstanceContractTest.java | 50 +++++++++----------
...=> StaticContractTest_mainExceptional.xml} | 10 ++--
...ticContractTest_mainExceptionalUnused.xml} | 8 +--
...taticContractTest_mainExceptionalVoid.xml} | 6 +--
.../test/StaticContractTest.java | 50 +++++++++----------
.../ExceptionalModifiableNothingTest.xml} | 4 +-
.../ExceptionalModifiableNothingTest.java} | 2 +-
.../ExceptionalModifiableNothingTest.proof} | 4 +-
...xceptionalModifiableNothingTest_OSS.proof} | 4 +-
.../oracle/MagicProofNoOSS.xml | 0
.../test/ExampleInstance.java | 0
.../test/MagicProofNoOSS.proof | 0
.../BlockContractModifiableEverything.java} | 6 +--
.../BlockContractModifiableEverything.proof} | 6 +--
...ntractModifiableLocationNotRequested.java} | 6 +--
...tractModifiableLocationNotRequested.proof} | 6 +--
...kContractModifiableRequestedLocation.java} | 6 +--
...ContractModifiableRequestedLocation.proof} | 6 +--
.../MethodContractModifiableExample.java} | 8 +--
.../MethodContractModifiableExample.proof} | 8 +--
...ntractModifiableLocationNotRequested.java} | 8 +--
...tractModifiableLocationNotRequested.proof} | 8 +--
...dContractModifiableRequestedLocation.java} | 8 +--
...ContractModifiableRequestedLocation.proof} | 8 +--
.../jml/translation/JMLSpecFactory.java | 4 +-
.../key/speclang/njml/JmlTermFactory.java | 5 +-
.../ilkd/key/speclang/njml/Translator.java | 12 ++---
.../ArrayMax.java | 2 +-
.../IGNORE | 0
.../examples/InformationFlow/Sum/README.txt | 2 +-
42 files changed, 164 insertions(+), 163 deletions(-)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml => blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml} (93%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{blockContractAssignableEverything/test/BlockContractAssignableEverything.java => blockContractModifiableEverything/test/BlockContractModifiableEverything.java} (87%)
rename key.core.symbolic_execution/src/test/resources/testcase/{slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof => set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof} (98%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml => blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml} (95%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java => blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java} (84%)
rename key.core.symbolic_execution/src/test/resources/testcase/{slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof => set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof} (97%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml => blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml} (91%)
rename key.core.symbolic_execution/src/test/resources/testcase/{slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java => set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java} (85%)
rename key.core.symbolic_execution/src/test/resources/testcase/{slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof => set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof} (97%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/{InstanceContractTest_mainExceptinal.xml => InstanceContractTest_mainExceptional.xml} (62%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/{InstanceContractTest_mainExceptinalUnused.xml => InstanceContractTest_mainExceptionalUnused.xml} (65%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/{InstanceContractTest_mainExceptinalVoid.xml => InstanceContractTest_mainExceptionalVoid.xml} (78%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/{StaticContractTest_mainExceptinal.xml => StaticContractTest_mainExceptional.xml} (57%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/{StaticContractTest_mainExceptinalUnused.xml => StaticContractTest_mainExceptionalUnused.xml} (60%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/{StaticContractTest_mainExceptinalVoid.xml => StaticContractTest_mainExceptionalVoid.xml} (74%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml => truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml} (84%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.java => truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.java} (79%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof => truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof} (99%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof => truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof} (99%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueAssignableAndLoop => truthValueModifiableAndLoop}/oracle/MagicProofNoOSS.xml (100%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueAssignableAndLoop => truthValueModifiableAndLoop}/test/ExampleInstance.java (100%)
rename key.core.symbolic_execution/src/test/resources/testcase/set/{truthValueAssignableAndLoop => truthValueModifiableAndLoop}/test/MagicProofNoOSS.proof (100%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{blockContractAssignableEverything/BlockContractAssignableEverything.java => blockContractModifiableEverything/BlockContractModifiableEverything.java} (87%)
rename key.core.symbolic_execution/src/test/resources/testcase/{set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof => slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof} (98%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.java => blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.java} (84%)
rename key.core.symbolic_execution/src/test/resources/testcase/{set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof => slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof} (97%)
rename key.core.symbolic_execution/src/test/resources/testcase/{set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.java => slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.java} (85%)
rename key.core.symbolic_execution/src/test/resources/testcase/{set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof => slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof} (97%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{methodContractAssignableEverything/MethodContractAssignableExample.java => methodContractModifiableEverything/MethodContractModifiableExample.java} (86%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{methodContractAssignableEverything/MethodContractAssignableExample.proof => methodContractModifiableEverything/MethodContractModifiableExample.proof} (96%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.java => methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.java} (84%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof => methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof} (94%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.java => methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.java} (84%)
rename key.core.symbolic_execution/src/test/resources/testcase/slicing/{methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof => methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof} (94%)
rename key.core/src/test/resources/testcase/parserMessageTest/{AssignableLocationIgnoredWarning => ModifiableLocationIgnoredWarning}/ArrayMax.java (97%)
rename key.core/src/test/resources/testcase/parserMessageTest/{AssignableLocationIgnoredWarning => ModifiableLocationIgnoredWarning}/IGNORE (100%)
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml
similarity index 93%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml
index a909f58e08d..a9489d5c9e3 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml
@@ -1,6 +1,6 @@
-
+
@@ -27,8 +27,8 @@ mod allLocs \setMinus freshLocs(heap)termination diamond" pathCondition="true" p
-
-
+
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.java b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.java
similarity index 87%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.java
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.java
index 7a5f1a3b1c4..738e953f0f4 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.java
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.java
@@ -1,9 +1,9 @@
-public class BlockContractAssignableEverything {
+public class BlockContractModifiableEverything {
public static int x;
-
+
public static int y;
-
+
/*@ normal_behavior
@ requires true;
@ ensures true;
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof
similarity index 98%
rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof
index 6a45f67f7b0..719b974c07a 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof
@@ -43,9 +43,9 @@
\proofObligation "#Proof Obligation Settings
#Wed Mar 30 16:07:42 CEST 2016
-name=BlockContractAssignableEverything[BlockContractAssignableEverything\\:\\:main()].JML normal_behavior operation contract.0
+name=BlockContractModifiableEverything[BlockContractModifiableEverything\\:\\:main()].JML normal_behavior operation contract.0
addSymbolicExecutionLabel=true
-contract=BlockContractAssignableEverything[BlockContractAssignableEverything\\:\\:main()].JML normal_behavior operation contract.0
+contract=BlockContractModifiableEverything[BlockContractModifiableEverything\\:\\:main()].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
@@ -150,7 +150,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
(rule "activeUseStaticFieldReadAccess" (formula "5") (term "1"))
(rule "assignment_read_static_attribute" (formula "5") (term "1"))
(builtin "One Step Simplification" (formula "5"))
- (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableEverything_x_0"))
+ (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableEverything_x_0"))
(rule "simplifySelectOfAnon" (formula "1"))
(builtin "One Step Simplification" (formula "1"))
(rule "dismissNonSelectedField" (formula "1") (term "2,0"))
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml
similarity index 95%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml
index 0b9624d3278..c8172e0f445 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml
@@ -1,6 +1,6 @@
-
+
@@ -9,7 +9,7 @@
pre measuredByEmpty
post exc_0 = null
mod {(null,
- BlockContractAssignableLocationNotRequested::$y)}termination diamond" pathCondition="true" pathConditionChanged="false" preconditionComplied="false">
+ BlockContractModifiableLocationNotRequested::$y)}termination diamond" pathCondition="true" pathConditionChanged="false" preconditionComplied="false">
@@ -25,7 +25,7 @@ mod {(null,
-
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java
similarity index 84%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java
index f52e591322a..02f4f17b4b3 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.java
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.java
@@ -1,9 +1,9 @@
-public class BlockContractAssignableLocationNotRequested {
+public class BlockContractModifiableLocationNotRequested {
public static int x;
-
+
public static int y;
-
+
/*@ normal_behavior
@ requires true;
@ ensures true;
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof
similarity index 97%
rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof
index 6592986d5af..c1234f982db 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof
@@ -43,9 +43,9 @@
\proofObligation "#Proof Obligation Settings
#Wed Mar 30 16:39:35 CEST 2016
-name=BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0
+name=BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0
addSymbolicExecutionLabel=true
-contract=BlockContractAssignableLocationNotRequested[BlockContractAssignableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0
+contract=BlockContractModifiableLocationNotRequested[BlockContractModifiableLocationNotRequested\\:\\:main()].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
@@ -172,7 +172,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
(rule "activeUseStaticFieldReadAccess" (formula "5") (term "1"))
(rule "assignment_read_static_attribute" (formula "5") (term "1"))
(builtin "One Step Simplification" (formula "5"))
- (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableLocationNotRequested_x_0"))
+ (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableLocationNotRequested_x_0"))
(rule "simplifySelectOfAnon" (formula "1"))
(builtin "One Step Simplification" (formula "1"))
(rule "dismissNonSelectedField" (formula "1") (term "2,0"))
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml
similarity index 91%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml
index ccd38bcd680..003fffcc5cd 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml
@@ -1,6 +1,6 @@
-
+
@@ -8,7 +8,7 @@
+mod {(null, BlockContractModifiableRequestedLocation::$x)}termination diamond" pathCondition="true" pathConditionChanged="false" preconditionComplied="false">
@@ -24,8 +24,8 @@ mod {(null, BlockContractAssignableRequestedLocation::$x)}termination diamond" p
-
-
+
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java
similarity index 85%
rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java
index 1cdba40e8be..9fd28452517 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.java
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.java
@@ -1,9 +1,9 @@
-public class BlockContractAssignableRequestedLocation {
+public class BlockContractModifiableRequestedLocation {
public static int x;
-
+
public static int y;
-
+
/*@ normal_behavior
@ requires true;
@ ensures true;
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof
similarity index 97%
rename from key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof
rename to key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof
index e8cd6d684ce..e3110f878a0 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof
@@ -43,9 +43,9 @@
\proofObligation "#Proof Obligation Settings
#Wed Mar 30 16:36:39 CEST 2016
-name=BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0
+name=BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0
addSymbolicExecutionLabel=true
-contract=BlockContractAssignableRequestedLocation[BlockContractAssignableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0
+contract=BlockContractModifiableRequestedLocation[BlockContractModifiableRequestedLocation\\:\\:main()].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
@@ -178,7 +178,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
(rule "activeUseStaticFieldReadAccess" (formula "5") (term "1"))
(rule "assignment_read_static_attribute" (formula "5") (term "1"))
(builtin "One Step Simplification" (formula "5"))
- (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractAssignableRequestedLocation_x_0"))
+ (rule "pullOutSelect" (formula "5") (term "0,1,0") (inst "selectSK=BlockContractModifiableRequestedLocation_x_0"))
(rule "simplifySelectOfAnon" (formula "1"))
(builtin "One Step Simplification" (formula "1"))
(rule "dismissNonSelectedField" (formula "1") (term "2,0"))
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinal.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptional.xml
similarity index 62%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinal.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptional.xml
index 4072f9325be..26286014a2f 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinal.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptional.xml
@@ -1,16 +1,16 @@
-
-
-
+
+
-
+termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" selfTerm="self" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false">
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalUnused.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalUnused.xml
similarity index 65%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalUnused.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalUnused.xml
index 07c84ff756e..32fe130b384 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalUnused.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalUnused.xml
@@ -1,15 +1,15 @@
-
-
+
-
+termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" selfTerm="self" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false">
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalVoid.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalVoid.xml
similarity index 78%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalVoid.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalVoid.xml
index 5ee15c6add9..7a55f8ba13a 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptinalVoid.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/oracle/InstanceContractTest_mainExceptionalVoid.xml
@@ -1,7 +1,7 @@
-
-
+
-
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java
index bd8210bfa21..0537d8ef083 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceContractTest/test/InstanceContractTest.java
@@ -1,7 +1,7 @@
public class InstanceContractTest {
private int value;
-
+
public int mainVoidMethod() {
voidMethod();
return value;
@@ -13,7 +13,7 @@ public int mainVoidMethod() {
public void voidMethod() {
value = 42;
}
-
+
public int mainNoArgs() {
return noArgs();
}
@@ -24,7 +24,7 @@ public int mainNoArgs() {
public int noArgs() {
return 42;
}
-
+
public int mainResult(int x) {
return result(x);
}
@@ -36,9 +36,9 @@ public int mainResult(int x) {
public int result(int x) {
return x*x;
}
-
-
+
+
public int mainResultNotSpecified(int x) {
return result(x);
}
@@ -50,35 +50,35 @@ public int mainResultNotSpecified(int x) {
public int resultNotSpecified(int x) {
return x*x;
}
-
- public void mainExceptinalVoid(boolean x) throws Exception {
- exceptinalVoid(x);
+
+ public void mainExceptionalVoid(boolean x) throws Exception {
+ exceptionalVoid(x);
}
/*@ exceptional_behavior
@ signals_only Exception;
@ signals (Exception) true;
@*/
- public void exceptinalVoid(boolean x) throws Exception {
+ public void exceptionalVoid(boolean x) throws Exception {
throw new Exception();
}
-
- public void mainExceptinalUnused(boolean x) throws Exception {
- exceptinal(x);
+
+ public void mainExceptionalUnused(boolean x) throws Exception {
+ exceptional(x);
}
-
- public boolean mainExceptinal(boolean x) throws Exception {
- return exceptinal(x);
+
+ public boolean mainExceptional(boolean x) throws Exception {
+ return exceptional(x);
}
/*@ exceptional_behavior
@ signals_only Exception;
@ signals (Exception) true;
@*/
- public boolean exceptinal(boolean x) throws Exception {
+ public boolean exceptional(boolean x) throws Exception {
throw new Exception();
}
-
+
public void mainBooleanResultUnused(boolean x) {
booleanResult(x);
}
@@ -89,7 +89,7 @@ public void mainBooleanResultUnused(boolean x) {
public boolean booleanResult(boolean x) {
return !x;
}
-
+
public void mainBooleanResultUnspecifiedUnused(boolean x) {
booleanResultUnspecified(x);
}
@@ -100,20 +100,20 @@ public void mainBooleanResultUnspecifiedUnused(boolean x) {
public boolean booleanResultUnspecified(boolean x) {
return !x;
}
-
+
public void mainExceptionalConstructor() throws Exception {
- new IntWrapper();
+ new IntWrapper();
}
-
+
public int mainConstructor() {
IntWrapper w = new IntWrapper(42);
return w.value;
}
-
+
public int mainOnObject(IntWrapper x) {
return x.getValue();
}
-
+
public static class IntWrapper {
public int value;
@@ -123,14 +123,14 @@ public static class IntWrapper {
@*/
public IntWrapper() throws Exception {
}
-
+
/*@ normal_behavior
@ ensures this.value == value;
@*/
public IntWrapper(int value) {
this.value = value;
}
-
+
/*@ normal_behavior
@ ensures \result == value;
@*/
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinal.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptional.xml
similarity index 57%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinal.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptional.xml
index cc6ea0ee0a2..99a5c3f7766 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinal.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptional.xml
@@ -1,13 +1,13 @@
-
-
-
+
+
-
+termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false">
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalUnused.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalUnused.xml
similarity index 60%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalUnused.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalUnused.xml
index 03a4c684155..1d99c3547b9 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalUnused.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalUnused.xml
@@ -1,12 +1,12 @@
-
-
+
-
+termination: diamond" pathCondition="true" pathConditionChanged="false" resultTerm="result_exceptional" exceptionTerm="exc_0" contractParameters="x" preconditionComplied="true" hasNotNullCheck="false" notNullCheckComplied="false">
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalVoid.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalVoid.xml
similarity index 74%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalVoid.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalVoid.xml
index 6152d1b0f6b..2f58ae16b70 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptinalVoid.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/oracle/StaticContractTest_mainExceptionalVoid.xml
@@ -1,12 +1,12 @@
-
-
+
-
+
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java
index 2ee6a3c1835..489fcf778d2 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/staticContractTest/test/StaticContractTest.java
@@ -1,7 +1,7 @@
public class StaticContractTest {
private static int value;
-
+
public static int mainVoidMethod() {
voidMethod();
return value;
@@ -13,7 +13,7 @@ public static int mainVoidMethod() {
public static void voidMethod() {
value = 42;
}
-
+
public static int mainNoArgs() {
return noArgs();
}
@@ -24,7 +24,7 @@ public static int mainNoArgs() {
public static int noArgs() {
return 42;
}
-
+
public static int mainResult(int x) {
return result(x);
}
@@ -36,9 +36,9 @@ public static int mainResult(int x) {
public static int result(int x) {
return x*x;
}
-
-
+
+
public static int mainResultNotSpecified(int x) {
return result(x);
}
@@ -50,35 +50,35 @@ public static int mainResultNotSpecified(int x) {
public static int resultNotSpecified(int x) {
return x*x;
}
-
- public static void mainExceptinalVoid(boolean x) throws Exception {
- exceptinalVoid(x);
+
+ public static void mainExceptionalVoid(boolean x) throws Exception {
+ exceptionalVoid(x);
}
/*@ exceptional_behavior
@ signals_only Exception;
@ signals (Exception) true;
@*/
- public static void exceptinalVoid(boolean x) throws Exception {
+ public static void exceptionalVoid(boolean x) throws Exception {
throw new Exception();
}
-
- public static void mainExceptinalUnused(boolean x) throws Exception {
- exceptinal(x);
+
+ public static void mainExceptionalUnused(boolean x) throws Exception {
+ exceptional(x);
}
-
- public static boolean mainExceptinal(boolean x) throws Exception {
- return exceptinal(x);
+
+ public static boolean mainExceptional(boolean x) throws Exception {
+ return exceptional(x);
}
/*@ exceptional_behavior
@ signals_only Exception;
@ signals (Exception) true;
@*/
- public static boolean exceptinal(boolean x) throws Exception {
+ public static boolean exceptional(boolean x) throws Exception {
throw new Exception();
}
-
+
public static void mainBooleanResultUnused(boolean x) {
booleanResult(x);
}
@@ -89,7 +89,7 @@ public static void mainBooleanResultUnused(boolean x) {
public static boolean booleanResult(boolean x) {
return !x;
}
-
+
public static void mainBooleanResultUnspecifiedUnused(boolean x) {
booleanResultUnspecified(x);
}
@@ -100,20 +100,20 @@ public static void mainBooleanResultUnspecifiedUnused(boolean x) {
public static boolean booleanResultUnspecified(boolean x) {
return !x;
}
-
+
public static void mainExceptionalConstructor() throws Exception {
- new IntWrapper();
+ new IntWrapper();
}
-
+
public static int mainConstructor() {
IntWrapper w = new IntWrapper(42);
return w.value;
}
-
+
public static int mainOnObject(IntWrapper x) {
return x.getValue();
}
-
+
public static class IntWrapper {
public int value;
@@ -123,14 +123,14 @@ public static class IntWrapper {
@*/
public IntWrapper() throws Exception {
}
-
+
/*@ normal_behavior
@ ensures this.value == value;
@*/
public IntWrapper(int value) {
this.value = value;
}
-
+
/*@ normal_behavior
@ ensures \result == value;
@*/
diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml
similarity index 84%
rename from key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml
rename to key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml
index 7057e7ebfce..c73153f380a 100644
--- a/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml
+++ b/key.core.symbolic_execution/src/test/resources/testcase/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml
@@ -1,9 +1,9 @@
-
+
-