From f683fb53253e69bde044f956b10e2c1f7a754c5a Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 22 Feb 2024 10:31:43 +0100 Subject: [PATCH 1/2] Start fix --- div/Div.java | 10 ++++++++++ .../key/speclang/jml/translation/JMLSpecFactory.java | 1 + 2 files changed, 11 insertions(+) create mode 100644 div/Div.java diff --git a/div/Div.java b/div/Div.java new file mode 100644 index 00000000000..4f7a8525ef8 --- /dev/null +++ b/div/Div.java @@ -0,0 +1,10 @@ +class Div { + /*@ public normal_behavior + @ diverges i >= 0; + @ ensures \result == 0; + @*/ + public int m(int i) { + while (i >= 0) i--; + return i; + } +} 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..24e9eb1954e 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 @@ -933,6 +933,7 @@ public ImmutableSet createFunctionalOperationContracts(String name, IP break; } } + // TODO: Fix #29 FunctionalOperationContract contract1 = cf.func(name, pm, true, pres, clauses.requiresFree, clauses.measuredBy, posts, clauses.ensuresFree, axioms, clauses.assignables, clauses.assignablesFree, clauses.accessibles, clauses.hasMod, From 7472e4abb471fbc099afc5b85dbca7806f4924c2 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 22 Feb 2024 14:28:50 +0100 Subject: [PATCH 2/2] Generate easier to prove contracts for non-trivial diverges --- div/Div.java | 10 ---------- .../key/speclang/jml/translation/JMLSpecFactory.java | 8 +++++--- 2 files changed, 5 insertions(+), 13 deletions(-) delete mode 100644 div/Div.java diff --git a/div/Div.java b/div/Div.java deleted file mode 100644 index 4f7a8525ef8..00000000000 --- a/div/Div.java +++ /dev/null @@ -1,10 +0,0 @@ -class Div { - /*@ public normal_behavior - @ diverges i >= 0; - @ ensures \result == 0; - @*/ - public int m(int i) { - while (i >= 0) i--; - return i; - } -} 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 24e9eb1954e..b7c88be66eb 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 @@ -926,20 +926,22 @@ public ImmutableSet createFunctionalOperationContracts(String name, IP result = result.add(contract); } else { // create two contracts for each diamond and box modality + Map boxPres = new LinkedHashMap<>(pres); for (LocationVariable heap : services.getTypeConverter().getHeapLDT().getAllHeaps()) { if (clauses.requires.get(heap) != null) { + var div = tb.convertToFormula(clauses.diverges); pres.put(heap, - tb.andSC(pres.get(heap), tb.not(tb.convertToFormula(clauses.diverges)))); + tb.andSC(pres.get(heap), tb.not(div))); + boxPres.put(heap, tb.andSC(boxPres.get(heap), div)); break; } } - // TODO: Fix #29 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.hasFreeMod, progVars); contract1 = cf.addGlobalDefs(contract1, abbrvLhs); - FunctionalOperationContract contract2 = cf.func(name, pm, false, clauses.requires, + FunctionalOperationContract contract2 = cf.func(name, pm, false, boxPres, clauses.requiresFree, clauses.measuredBy, posts, clauses.ensuresFree, axioms, clauses.assignables, clauses.assignablesFree, clauses.accessibles, clauses.hasMod, clauses.hasFreeMod, progVars);