summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Update test script shortcuts to work in Powershell (which supplies an ↵Gravatar Christian Klauser2012-03-27
| | | | absolute path as %0 instead of just the scripts name)
* VCC: display bitvectorsGravatar Michal Moskal2012-01-28
|
* MergeGravatar Michal Moskal2012-01-28
|\
* | VCC: fixes in function visibilityGravatar Michal Moskal2012-01-28
| |
| * Dafny: fixed bug in compilation of let expressions.Gravatar Rustan Leino2012-01-26
| |
| * Dafny: Fixed a bug in the resolving of UpdateStmts.Gravatar wuestholz2012-01-25
| |
| * Dafny: Fixed a bug in the printing of let expressions.Gravatar wuestholz2012-01-24
| |
| * MergeGravatar qadeer2012-01-23
| |\
| * | an optimization in dynamic dispatchGravatar qadeer2012-01-23
| | | | | | | | | | | | a hack in event translation
| | * Merge (Make Chalice AST accessible to other tools)Gravatar Christian Klauser2012-01-20
| |/|
| | * Chalice: break main method into multiple methods, so that other tools can ↵Gravatar Christian Klauser2012-01-20
| | | | | | | | | | | | access the Chalice AST.
| * | MergeGravatar Rustan Leino2012-01-19
| |\ \
| * | | Chalice: added more standard file(line,col) error-message output, currently ↵Gravatar Rustan Leino2012-01-19
| | | | | | | | | | | | | | | | under the new /rise4fun switch
| | * | Boogie build succeededGravatar CodeplexBot2012-01-19
| |/ /
| * | Dafny: fixed bug in compilation of generic datatypesGravatar Rustan Leino2012-01-18
| | |
| * | Dafny: improved error location for violations of function postconditionsGravatar Rustan Leino2012-01-18
| | |
| * | Dafny: allow a refinement to provide a function/method body if the ↵Gravatar Rustan Leino2012-01-18
| | | | | | | | | | | | function/method being refined didn't have one
| * | Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2012-01-18
| | |
| * | Dafny: added signature checking to refinementGravatar Rustan Leino2012-01-17
| | |
| * | Dafny: allow parallel statements with an empty list of bound variablesGravatar Rustan Leino2012-01-17
| | |
| * | Dafny: parallel statements:Gravatar Rustan Leino2012-01-17
| | | | | | | | | | | | | | | | | | | | | - removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases - also allow old/fresh in ensures clauses of parallel statements - allow TypeRhs and choose expressions in Call/Proof parallel statements - disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements)
* | | VCC/BVD: what were these null checks all over about?Gravatar Michal Moskal2012-01-17
|/ /
* | MergeGravatar Rustan Leino2012-01-16
|\ \
* | | Dafny: Recheck specifications that contain refined (extended) predicates, ↵Gravatar Rustan Leino2012-01-16
| | | | | | | | | | | | even if they are contained inside a split expression. Superposition is thought to be sound.
| * | Mark the procedure translated from the module's entry pointGravatar Mike Barnett2012-01-15
|/ / | | | | | | with the attribute {:entrypoint}.
* | Dafny: handle refinement of nested tokens that come from SpliExpr (still ↵Gravatar Rustan Leino2012-01-12
| | | | | | | | need to deal with unsplit expressions, like quantifiers)
* | Dafny: make full predicate definitions available only inside a module ↵Gravatar Rustan Leino2012-01-11
| | | | | | | | (outside is just an implication: the predicate implies the body known so far)
* | Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
| | | | | | | | see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
* | Boogie build succeededGravatar CodeplexBot2012-01-11
| |
* | Dafny: fixed bugs in contract types, and a code bug that caused a contract ↵Gravatar Rustan Leino2012-01-10
| | | | | | | | to fail
* | MergeGravatar Rustan Leino2012-01-10
|\ \
* | | Dafny: some bug fixesGravatar Rustan Leino2012-01-10
| | |
* | | Dafny VSX: fixed compilation inconsistencyGravatar Rustan Leino2012-01-10
| | |
* | | Dafny: allow class-member declarations at top level of any module (not just ↵Gravatar Rustan Leino2012-01-10
| | | | | | | | | | | | the default module); these go into the (new) default class of each module
* | | Dafny: added test case for refinement and predicates (and fixed a parsing bug)Gravatar Rustan Leino2012-01-10
| | |
| * | Make a copy of a struct value being passed to a methodGravatar Mike Barnett2012-01-10
| | | | | | | | | | | | whether the method is generic or not.
* | | Dafny: allow definitions and uses of parameter-less predicates to go without ↵Gravatar Rustan Leino2012-01-10
| | | | | | | | | | | | parentheses
| * | Fix call to struct copy ctor.Gravatar Mike Barnett2012-01-10
| | |
| * | Fixed struct copy constructor implementation.Gravatar Mike Barnett2012-01-10
| | |
* | | Dafny: added predicatesGravatar Rustan Leino2012-01-10
|/ /
* | MergeGravatar Rustan Leino2012-01-09
|\ \
* | | Dafny: added support for simple superposition refinementsGravatar Rustan Leino2012-01-09
| | |
| * | Boogie build failedGravatar CodeplexBot2012-01-10
|/ /
* | MergeGravatar Rustan Leino2012-01-09
|\ \
* | | Dafny: changed translation to be sensitive to refinement inheritance; this ↵Gravatar Rustan Leino2012-01-09
| | | | | | | | | | | | feature is now functional, provided the refining module does not add or change anything
* | | Boogie: fixed proof-obligation countingGravatar Rustan Leino2012-01-09
| | |
* | | Boogie: output number of proof obligations (asserts) along with timing ↵Gravatar Rustan Leino2012-01-09
| | | | | | | | | | | | information when using the /trace option
| * | Change the copy constructor for struct types so that it returns the copyGravatar Mike Barnett2012-01-09
|/ / | | | | | | | | of the struct value. This way it can do an allocation within the copy ctor (if that is the design choice for structs, which it currently is).
* | Dafny: disallow changes of datatypes in refinementsGravatar Rustan Leino2012-01-09
| |
* | Dafny: finished refinement cloning transformationsGravatar Rustan Leino2012-01-07
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-22 03:31:03 +0000