summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Fixes to vim highlightingGravatar Dan Rosén2014-07-07
|
* New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
|
* DafnyExtension: Minor change to deal with a change in the Boogie ↵Gravatar wuestholz2014-06-20
| | | | command-line options
* Made the snapshotable trees test "unsupported" instead of "unresolved".Gravatar wuestholz2014-06-05
|
* Fixed issues with absolute file names in the expected output for the lit tests.Gravatar wuestholz2014-06-04
|
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Fixed bug in resolution, where type proxies involved in equality tests did ↵Gravatar Rustan Leino2014-05-07
| | | | | | not get assigned. (Issue #35) Fixed Main detection--a method "Main" with type parameters cannot be a program entry point.
* Fixed some bugs where various attributes were not properly visited during ↵Gravatar Rustan Leino2014-05-05
| | | | type checking.
* DafnyExtension: Made it display the compilation output in the VS output pane.Gravatar wuestholz2014-04-21
|
* Add support for assumption variables.Gravatar wuestholz2014-04-21
|
* DafnyExtension: Added some support for logging program snapshots that are ↵Gravatar wuestholz2014-04-21
| | | | sent to the verifier.
* Fixed bug #33.Gravatar Rustan Leino2014-04-19
|
* Version 1.8.2.10419, binary release and (except for the "include" update in ↵Gravatar Rustan Leino2014-04-19
| | | | the previous check-in) rise4fun
* Members included from different files are now internally marked with an ↵Gravatar Rustan Leino2014-04-19
| | | | | | | IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features. Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines). Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked.
* Fixed bug #32 dafny.codeplex.com.Gravatar Rustan Leino2014-04-15
|
* Cleaned up some no longer needed parentheses in test fileGravatar Rustan Leino2014-04-15
|
* Run-time real supportGravatar Rustan Leino2014-04-13
|
* Compile realsGravatar Rustan Leino2014-04-13
|
* Allow reals in decreases clausesGravatar Rustan Leino2014-04-08
|
* MergeGravatar Rustan Leino2014-04-04
|\
* | Fixed refinement of modify statementsGravatar Rustan Leino2014-04-04
| |
| * Partial support for slicing a sequence using lengths, rather than indices.Gravatar Bryan Parno2014-04-04
|/ | | | Will get cleaner once we have tuple support.
* Adjusted mergeGravatar Rustan Leino2014-04-04
|
* MergeGravatar Rustan Leino2014-04-04
|\
* | Also include lower set bounds (bounding a set from below) in witness guesses ↵Gravatar Rustan Leino2014-04-04
| | | | | | | | for assign/let such-that.
* | Support the transition from "modify Frame;" to "modify Frame { Body }" by ↵Gravatar Rustan Leino2014-04-04
| | | | | | | | refinement.
* | Changed an error from a verification error to a syntactic (resolution) errorGravatar Rustan Leino2014-04-04
| |
* | Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
| |
* | Added "modify" statement.Gravatar Rustan Leino2014-04-03
| | | | | | | | In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
| * Basic support for datatype-update syntatic sugarGravatar Bryan Parno2014-04-03
|/
* DafnyExtension: Fixed a concurrency issue.Gravatar wuestholz2014-04-03
|
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
| | | | Minor changes in a test file.
* Bumped version to 1.8.1.10324. To go onto rise4fun and as a binary drop.Gravatar Rustan Leino2014-03-24
|
* MergeGravatar Rustan Leino2014-03-24
|\
* | Reduced noise in BVD display of temporary variables of the translationGravatar Rustan Leino2014-03-24
| |
| * Auto-set type arguments of built-in collection types, just like for ↵Gravatar Rustan Leino2014-03-21
| | | | | | | | user-defined types.
| * Fixed typo in latex style fileGravatar Rustan Leino2014-03-20
|/
* Added axiom to transfer array element-type information onto the elements ↵Gravatar Rustan Leino2014-03-20
| | | | | | themselves. Other serendipitous axiom improvements.
* Fixed problem with propagating allocation information about array elements.Gravatar Rustan Leino2014-03-20
| | | | Improved situation with (reducing bogosity of) type checking of "object".
* Propagate literals through equality operations.Gravatar Nada Amin2014-03-19
|
* MergeGravatar Rustan Leino2014-03-17
|\
* | Fixed resolution bug where "var x := x" was allowed.Gravatar Rustan Leino2014-03-17
| |
* | Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵Gravatar Rustan Leino2014-03-17
| | | | | | | | to VarDeclStmt.Locals
* | AST refactoring:Gravatar Rustan Leino2014-03-17
| | | | | | | | | | Changed VarDecl to no longer inherit from Statement. Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement.
| * MergeGravatar Nada Amin2014-03-12
| |\ | |/ |/|
| * Improve computations, in particular compositionality. Isolated useless ↵Gravatar Nada Amin2014-03-12
| | | | | | | | literals around if-then-else as a surprising source of practical hanging.
| * change computation weight to 3. Tests still pass.Gravatar Nada Amin2014-03-11
| |
* | Added a test case from the ACL2 bookGravatar Rustan Leino2014-03-10
|/
* Removed an apparently unneeded trigger.Gravatar Rustan Leino2014-03-06
|
* Moved the (long running) CloudMake test files to their own directoryGravatar Rustan Leino2014-02-28
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 15:09:51 +0000