Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵ | 2012-06-14 | |
| | | | | for special characters in identifiers | ||
* | Merge | 2012-06-14 | |
|\ | |||
* | | Dafny: fixed a couple of compiler bugs | 2012-06-14 | |
| | | |||
* | | Dafny: cleaned up test scripts a little | 2012-06-14 | |
| | | |||
| * | Merge | 2012-06-13 | |
| |\ | |/ |/| | |||
| * | Dafny: allow parallel assignments to assign to the same LHS if the RHS match. | 2012-06-13 | |
| | | |||
* | | Merge | 2012-06-13 | |
|\| | |||
* | | Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to ↵ | 2012-06-13 | |
| | | | | | | | | check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P". | ||
| * | Dafny: liberalized equality to work when the types could possibly be the same | 2012-06-13 | |
| | | | | | | | | (i.e. a != b is allowed when a: array<int> and b: array<T>) | ||
* | | Dafny: added another version of the majority finding algorithm to the test suite | 2012-06-12 | |
|/ | |||
* | Dafny: beefed up allocation axioms for boxes stored in fields | 2012-06-12 | |
| | |||
* | Dafny: allow types to be qualified with the name of the module that declares ↵ | 2012-06-11 | |
| | | | | them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member) | ||
* | Dafny: added some test programs | 2012-06-08 | |
| | |||
* | Dafny/Boogie/BVD: made Dafny plug-in for BVD work again | 2012-06-08 | |
| | |||
* | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵ | 2012-06-01 | |
| | | | | | | | assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change. | ||
* | Dafny: Added map comprehensions and updated display syntax | 2012-05-31 | |
| | |||
* | Merge | 2012-05-29 | |
|\ | |||
* | | Dafny: fixed regression tests | 2012-05-29 | |
| | | |||
* | | Dafny: Added maps to regression tests. | 2012-05-29 | |
| | | |||
| * | Fixed the regression for deterministicExtractLoops. | 2012-05-25 | |
| | | |||
| * | Merge | 2012-05-25 | |
| |\ | |||
| * | | Adding an option for deterministicExtractLoops, that uses an alternate way ↵ | 2012-05-25 | |
|/ / | | | | | | | | | | | to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory. | ||
| * | updated test | 2012-05-24 | |
| | | |||
| * | more refactoring in stratified inlining | 2012-05-24 | |
|/ | |||
* | Dafny: more correct checking of co-inductive productivity | 2012-05-18 | |
| | |||
* | Merge | 2012-05-01 | |
|\ | |||
* | | Dafny: added support for co-recursive calls | 2012-05-01 | |
| | | |||
| * | Update to match the new model printing format | 2012-04-30 | |
| | | |||
| * | UseLabels=false when stratified inline is on | 2012-04-29 | |
|/ | |||
* | eliminated class ErrorModel | 2012-04-28 | |
| | |||
* | removed proccopybounding code | 2012-04-28 | |
| | | | | stratified inliinig is now run always with /doNotUseLabels | ||
* | removed the lazy inline test directory | 2012-04-28 | |
| | |||
* | removed lazy inlining | 2012-04-28 | |
| | |||
* | Dafny: fixed unsoundness having to do with a function depending on the ↵ | 2012-04-27 | |
| | | | | allocation state | ||
* | Dafny: added resolution tests cases for inductive datatypes | 2012-04-27 | |
| | |||
* | Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵ | 2012-04-25 | |
| | | | | | | | handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now) | ||
* | Added test to stratified inlining. | 2012-04-24 | |
| | | | | Don't use UNSAT core for the refinement step. | ||
* | Fixed bug with triply nested maps and polymorphism (reported as Item # 10218). | 2012-04-04 | |
| | |||
* | small fix | 2012-04-04 | |
| | | | | added regressions | ||
* | Dafny: support assign-such-that in var declarations in refinements | 2012-03-15 | |
| | |||
* | Dafny: fixed lack of assign-such-that restriction in parallel statement | 2012-03-15 | |
| | |||
* | Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; | 2012-03-15 | |
| | |||
* | Dafny: added StoreAndRetrieve refinement example | 2012-03-15 | |
| | |||
* | Boogie: Simplified (and liberalized) parsing of string literals as attribute ↵ | 2012-03-12 | |
| | | | | parameters | ||
* | Boogie: temporarily disabled the "datatypes" test cases, until a null ↵ | 2012-03-12 | |
| | | | | dereference error in the Boogie code gets resolved | ||
* | updated Boogie strings so that they can refer to \" (and more) | 2012-03-12 | |
| | | | | fixed BCT :value | ||
* | Dafny: removed a now-inferred type-parameter instantiation in a test file | 2012-03-07 | |
| | |||
* | Dafny: added ghost modules (the meaning is simply that such a module will ↵ | 2012-03-07 | |
| | | | | | | | not be compiled) Dafny: improved :autocontracts heuristic for detecting "simple query method" Dafny: fixed some bugs | ||
* | Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic ↵ | 2012-03-05 | |
| | | | | specifications | ||
* | Merge | 2012-03-02 | |
|\ |