summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Dafny: fixed mergeGravatar Rustan Leino2012-10-04
* MergeGravatar Rustan Leino2012-10-04
|\
* | Dafny: complete implementation of iteratorsGravatar Rustan Leino2012-10-03
* | Dafny: automatically update iterator _new field upon allocationsGravatar Rustan Leino2012-10-03
* | Dafny: fixed compiler bug in array allocation (reported as boogie:397957)Gravatar Rustan Leino2012-10-03
* | Dafny: good error locations for yield statements; other iterator improvements...Gravatar Rustan Leino2012-10-03
* | Dafny: more part of verifying iteratorsGravatar Rustan Leino2012-10-03
| * changed the signing to ..\InterimKey.snkGravatar qadeer2012-10-03
| * bunch of refactoringsGravatar Unknown2012-10-03
* | Dafny: changed iterator body to resolve to implicit fields rather than to the...Gravatar Rustan Leino2012-10-02
* | Dafny: handle decreases clause for iteratorsGravatar Rustan Leino2012-10-02
* | Dafny: incomplete snapshot of verification of iteratorsGravatar Rustan Leino2012-10-02
| * Fixed GPUVerify solution.Gravatar Unknown2012-10-01
| * MergeGravatar Unknown2012-10-01
| |\
| * | Fix to abstract interpretation to match Boogie.Gravatar Unknown2012-10-01
* | | Dafny: fixed compilation issue (a datatype is now allowed to be called "d")Gravatar Rustan Leino2012-09-29
| | * MergeGravatar Nadia Polikarpova2012-09-29
| | |\
| | | * Boogie: added /vcsLoad flag as a convenient way to set /vcsCores proportional...Gravatar Unknown2012-09-28
| | |/ | |/|
| * | MergeGravatar Unknown2012-09-28
| |\ \
| * | | Fixed bug with uniformity analysis for havoc. Allowed barrier invariants toGravatar Unknown2012-09-28
| | * | Dafny: Removed assembly reference to 'AIFramework'.Gravatar wuestholz2012-09-28
| | * | Fixed the build.Gravatar wuestholz2012-09-28
| | * | Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
| | * | Added BigDec as representation for (floating-point) decimal valuesGravatar boehmes2012-09-27
| | * | Boogie: new syntax for integer division and modulus: use div and mod instead ...Gravatar boehmes2012-09-27
| | * | Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
| | * | Removed abandoned Isabelle prover backendGravatar boehmes2012-09-27
| |/ /
| * | Barrier invariants can now refer to local variables that are uniform.Gravatar Unknown2012-09-26
* | | Dafny: compile iteratorsGravatar Rustan Leino2012-09-26
* | | Dafny: changed iterators to become special cases of classesGravatar Rustan Leino2012-09-25
* | | Dafny: added iterators; for now, only parsing and resolving (and printing and...Gravatar Rustan Leino2012-09-25
| | * MergeGravatar Nadia Polikarpova2012-09-25
| | |\ | | |/ | |/|
| * | MergeGravatar Unknown2012-09-24
| |\ \
| * | | Fixed issue with uniformity analysis and block merging. Uniformity analysisGravatar Unknown2012-09-24
| | * | MergeGravatar Egor Kyshtymov2012-09-24
| |/| |
| | * | Added detailed trace functionality.Gravatar Egor Kyshtymov2012-09-24
| * | | Support for barrier invariants.Gravatar Unknown2012-09-24
| | | * Use expression splitting for checking calculation stepsGravatar Nadia Polikarpova2012-09-23
| | | * Bugfix in the translation of calc statements (oops), added more resolution an...Gravatar Nadia Polikarpova2012-09-21
| | | * Added tests for parsing and resolution of calc statementsGravatar Nadia Polikarpova2012-09-21
| | | * MergeGravatar Nadia Polikarpova2012-09-21
| | | |\ | | |_|/ | |/| |
| * | | Fixed a bug with empty big blocks.Gravatar Unknown2012-09-21
| * | | MergeGravatar Unknown2012-09-21
| |\ \ \
| * | | | Added support for invariants about shared state.Gravatar Unknown2012-09-21
| | | | * MergeGravatar Nadia Polikarpova2012-09-20
| | | | |\ | | | |_|/ | | |/| |
| | | | * Allow a single != in a calcGravatar Nadia Polikarpova2012-09-20
| | * | | MergeGravatar Unknown2012-09-19
| | |\ \ \ | | |/ / / | |/| | |
| | * | | Boogie: improved parser makefileGravatar Unknown2012-09-19
| | | | * Not reusing RelOp parser in CalcOp to avoid the conflict between !in and !Gravatar Nadia Polikarpova2012-09-19
| | | | * Well-formedness check for calc linesGravatar Nadia Polikarpova2012-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 10:54:37 +0000