Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: handle decreases clause for iterators | 2012-10-02 | |
| | |||
* | Dafny: incomplete snapshot of verification of iterators | 2012-10-02 | |
| | |||
* | Dafny: fixed compilation issue (a datatype is now allowed to be called "d") | 2012-09-29 | |
| | |||
* | Dafny: compile iterators | 2012-09-26 | |
| | |||
* | Dafny: changed iterators to become special cases of classes | 2012-09-25 | |
| | |||
* | Dafny: added iterators; for now, only parsing and resolving (and printing ↵ | 2012-09-25 | |
| | | | | and refining), no compilation or verification | ||
* | Dafny: clone and merge attributes in refinements | 2012-09-12 | |
| | |||
* | Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ↵ | 2012-09-12 | |
| | | | | and axiomatize [][..0] == [] == [][0..] | ||
* | Dafny: did a little to extend the support of labeled statements in ↵ | 2012-09-10 | |
| | | | | refinements (things like multiple labels are still not thought through very well) | ||
* | Dafny: improved checking of inherited postconditions (in refinements) | 2012-09-10 | |
| | |||
* | Boogie: added /tracePOs option for printing out number of proof obligations ↵ | 2012-09-10 | |
| | | | | without also printing out the verification times | ||
* | Merge | 2012-09-10 | |
|\ | |||
* | | Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵ | 2012-09-09 | |
| | | | | | | | | tail-recursive methods | ||
* | | Merge | 2012-09-07 | |
|\ \ | |||
* | | | Dafny: Added detection and support for tail recursive calls (and an ↵ | 2012-09-07 | |
| | | | | | | | | | | | | optional "tailrecursion" attribute). Also, let the cloner also clone attributes. | ||
| * | | Implement support for alternative SMT solvers -- CVC3 and CVC4 | 2012-09-06 | |
| | | | |||
* | | | Merge | 2012-09-05 | |
|\| | | |||
| * | | Moved point at which preprocessed output is shown. | 2012-08-31 | |
| | | | |||
| * | | Shared state is now properly abstracted in requires clauses. | 2012-08-31 | |
| | | | |||
* | | | Dafny: for refinements, don't consider a newly provided predicate body to be ↵ | 2012-08-30 | |
| | | | | | | | | | | | | an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be | ||
* | | | DafnyExtension: changed how "_" is displayed (now display as a keyword, not ↵ | 2012-08-30 | |
| | | | | | | | | | | | | as an identifier definition) | ||
* | | | Dafny: allow "_" as don't-care variable name | 2012-08-30 | |
| | | | |||
| | * | Dafny: allow more corecursive calls for copredicates | 2012-08-30 | |
| |/ |/| | |||
| * | Merge | 2012-08-30 | |
| |\ | |/ |/| | |||
| * | Barriers now handled uniformly via bugle_barrier. | 2012-08-30 | |
| | | | | | | | | | | | | | | | | | | | | | | Improved loop invariant inference so that procedure formal parameters are treated as constants. (This involved fixing a bug where a Formal was being dualised to a LocalVariable.) Fixed problem in GPUVerifyBoogieDriver where source location information was being looked for via a file name, rather than a full path. Cleaned up some code in GPUVerifyBoogieDriver. | ||
* | | Dafny: fixed bug in checking postconditions of functions that mention the ↵ | 2012-08-29 | |
| | | | | | | | | result the function itself | ||
* | | Dafny: fixed contract violation in parser (for non-parsing Lhs production) | 2012-08-29 | |
|/ | |||
* | A small fix in variable definition analysis. | 2012-08-29 | |
| | |||
* | Added generation of invariants to restrict source location to sensible values. | 2012-08-28 | |
| | | | | | Refactored Make...Variable() and FindOrCreate...Variable() functions to take a variable name as a parameter rather than the variable itself. | ||
* | Dafny: fixed contract bug in resolver | 2012-08-27 | |
| | |||
* | Added group information to race error reporting. | 2012-08-22 | |
| | |||
* | Extra debugging output for Houdini | 2012-08-21 | |
| | |||
* | Dafny and Boogie: get rid of 'static' fields in parser | 2012-08-21 | |
| | |||
* | Fixed problem where SOURCE variables were not being generated. | 2012-08-20 | |
| | |||
* | Added functionality for race error reporting. | 2012-08-20 | |
| | |||
* | DafnyExtension: simplified display of type names and field names | 2012-08-17 | |
| | |||
* | DafnyExtension: various improvements | 2012-08-16 | |
| | |||
* | Fixed bug where source location attributes are not being attached to a CHECK | 2012-08-16 | |
| | | | | call, and refactored code to avoid the duplication which caused this error. | ||
* | DafnyExtension: fixed more missing cases for hover texts | 2012-08-15 | |
| | |||
* | Dafny: fixed some bugs in the newly added DafnyExtension code | 2012-08-15 | |
| | |||
* | Dafny: added Statement.SubExpressions getter | 2012-08-15 | |
| | | | | DafnyExtension: added hover text for identifiers | ||
* | Merge | 2012-08-14 | |
|\ | |||
* | | Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵ | 2012-08-14 | |
| | | | | | | | | crashing after certain deletes) | ||
| * | Added GPUVerifyBoogieDriver project. | 2012-08-14 | |
| | | | | | | | | Contributed by Egor Kyshtymov. | ||
| * | Separated race checking into logging and checking calls. This simplifies | 2012-08-14 | |
| | | | | | | | | error reporting. | ||
| * | Removed some dud code for handling nested maps, which we no longer support. | 2012-08-13 | |
| | | |||
| * | Some more code cleanup related to removal of the "divided" option. | 2012-08-13 | |
| | | |||
| * | Removed code related to "divided" option. | 2012-08-13 | |
|/ | |||
* | Merge | 2012-08-13 | |
|\ | |||
* | | Barrier divergence checking now achieved via precondition. | 2012-08-13 | |
| | | | | | | | | | | | | Race checking assertions contain tags to identify them. Attributes are passed correctly through the dualisation process. |