issues Search Results · repo:mattulbrich/dive language:Java
Filter by
122 results
(57 ms)122 results
inmattulbrich/dive (press backspace or delete to remove)Updates to a heap are handled as a LetTerm with substitution heap - store... The Term representation of heap is a
ApplTerm. The SubstitutionVisitor, only substitutes VarTerms. So the heap update is ignored ...
SpringVaS
- Opened on Mar 10, 2022
- #206
I observed that in one particular PVC, a match term is created that cannot be matched and thus raises an exception upon
script interpretation. It happens in the PVC List.size/Null of the ListExample AlgoVerList.dfy ...
- 1
- Opened on Apr 1, 2021
- #205
The following cannot be proved by boogie:
### project:
class C { var f : int; }
### decls:
o : C
a : array int
### sequent:
|- o.f == o.f@$heap[a[0] := 0]
### result:
prove
The translation is incomplete ...
backend
bug
mattulbrich
- Opened on Oct 21, 2020
- #194
The following lemma raises an exception.
lemma l1(s: seq int ) ensures (|s|==|s|) {}
The stacktrace is essentially:
java.lang.ArrayIndexOutOfBoundsException: Index 0 out of bounds for length 0
at edu.kit.iti.algover.util.Util$ReadOnlyArrayList.get(Util.java:457) ...
backend
bug
- 2
- Opened on Oct 15, 2020
- #192
To apply a rule a term has to be select in the sequent view even for rules which are not applied on terms like
addHypothesis . This should not be necessary
JonasKlamroth
- Opened on Aug 26, 2020
- #189
Currently the assignment to r is overlooked in the following such that this verifies (and should not):
method m()
{
var r := [42];
while(r[0] 0) {
r[0] := 0;
}
assert r[0] == 42; ...
backend
bug
- 1
- Opened on Jun 17, 2020
- #185
It appears that a style range is computed wrong when the curly braces in the code don t match. E. g. removing lines. It
might be enough to catch the exception. exception
bug
fx-gui
- 2
- Opened on Jun 10, 2020
- #180
1) Syntax s := s[i := v] for updating sequences not supported
2) Dash minus |- is read as turnstile ⊢ . Particularly in s := s[0..|s|-1] This is not expected behavior. sequpdate
readasstencil
- 4
- Opened on Jun 10, 2020
- #179
Simple data type parameters of a method (call by value) should not be writable within that method. False can be proven.
immutableparams
- Opened on Jun 10, 2020
- #178
The following should be parsable in Dafny, but are not all in DIVE:
lemma m(x: int, y:int, z:int)
- [x] requires x == y == z
- [x] requires x y z
- [x] requires x y == z
- [x] requires x == y ...
- 3
- Opened on May 20, 2020
- #176
Learn how you can use GitHub Issues to plan and track your work.
Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub IssuesProTip!
Press the /
key to activate the search input again and adjust your query.Learn how you can use GitHub Issues to plan and track your work.
Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub IssuesProTip!
Restrict your search to the title by using the in:title qualifier.