Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fixed bug with uniformity analysis for havoc. Allowed barrier invariants to | 2012-09-28 | |
| | | | | | support a more expressive class of expressions. Refactored thread id creation functions. | ||
* | Barrier invariants can now refer to local variables that are uniform. | 2012-09-26 | |
| | |||
* | Merge | 2012-09-24 | |
|\ | |||
* | | Fixed issue with uniformity analysis and block merging. Uniformity analysis | 2012-09-24 | |
| | | | | | | | | now enabled by default. | ||
| * | Merge | 2012-09-24 | |
|/| | |||
| * | Added detailed trace functionality. | 2012-09-24 | |
| | | | | | | | | | | Improved error reporting. Tidied up code. | ||
* | | Support for barrier invariants. | 2012-09-24 | |
| | | |||
* | | Fixed a bug with empty big blocks. | 2012-09-21 | |
| | | |||
* | | Merge | 2012-09-21 | |
|\ \ | |||
* | | | Added support for invariants about shared state. | 2012-09-21 | |
| | | | | | | | | | | | | | | | | | | Reworked implementation of barriers. Started on support for barrier invariants. | ||
| * | | Merge | 2012-09-19 | |
| |\ \ | |/ / |/| | | |||
| * | | Boogie: improved parser makefile | 2012-09-19 | |
| | | | |||
* | | | When uniformity analysis is disabled, no procedures (even the kernel entry | 2012-09-19 | |
| | | | | | | | | | | | | | | | point) will be regarded as uniform. This simplification avoids various edge cases. | ||
* | | | Merge | 2012-09-18 | |
|\| | | |||
* | | | Uniformity analysis. Patch by Peter Collingbourne. | 2012-09-18 | |
| | | | |||
* | | | Dualisation modified so that global arrays are not dualised, and group-shared | 2012-09-18 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | arrays are turned into 2D maps with first index type bool. Thread 1 always indexes into "true", while threads 2 indexes into "samegroup" (a formula which is true iff threads 1 and 2 are in the same group). Thus if the threads are in different groups they operate on different shared arrays, but if they are in the same group they operate on the same shared array. This paves the way for implementing support for barrier invariants. | ||
| * | | Merge | 2012-09-17 | |
| |\ \ | |/ / |/| | | |||
| * | | Allow custom operators on a line | 2012-09-17 | |
| | | | |||
* | | | During dualisation, | 2012-09-17 | |
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | x := y; now becomes x$1 := y$1; x$2 := y$2; instead of x$1, x$2 := y$1, y$2; This is to make way for further changes. | ||
| * | Allow several calculation operators (for the whole calculation) | 2012-09-16 | |
| | | |||
| * | Allowing calc as hint (without braces) | 2012-09-16 | |
| | | |||
| * | Renamed terms into lines (according to the proposal), fixed some contracts | 2012-09-16 | |
| | | |||
* | | Added creation of source variable pre- and post- conditions. | 2012-09-16 | |
| | | | | | | | | | | Changed style of error messages. Cleaned up error reporting code. | ||
| * | Error reporting for calculation steps | 2012-09-14 | |
| | | |||
| * | Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵ | 2012-09-14 | |
| | | | | | | | | t<i> op t<i + 1>), generated during resolution; first version of the translation | ||
| * | Merge | 2012-09-14 | |
| |\ | |/ |/| | |||
| * | Pretty-print calc statements | 2012-09-14 | |
| | | |||
| * | Resolve and clone calc statements; fixed a small grammar bug | 2012-09-13 | |
| | | |||
| * | Added calc statement to the AST and the grammar (first attempt) | 2012-09-13 | |
| | | |||
* | | 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 | |
|/ |