Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | bug fixes | 2011-05-16 | |
| | |||
* | Fix break. | 2011-05-16 | |
| | |||
* | new regression output | 2011-05-16 | |
|\ | |||
* \ | Merge | 2011-05-16 | |
|\ \ | |||
* | | | merge | 2011-05-16 | |
| | | | |||
* | | | Merge | 2011-05-16 | |
| | | | |||
| | * | Add extern declarations to procedures. | 2011-05-16 | |
| | | | | | | | | | | | | | | | | | | Normalize method bodies so anonymous delegates are gone. Some attempts at simplifying. New regression output. | ||
| | * | Mark procedures/functions as "extern" if they are defined in a different | 2011-05-16 | |
| | | | | | | | | | | | | | | | | | | | | | assembly than the one under translation. Normalize method bodies so anonymous delegates do not appear, but instead show up as the nested classes/methods that implement them. Beginning of some simplfication for nested expressions. | ||
| * | | Merge | 2011-05-16 | |
| |\ \ | |||
| * | | | convert assert to requires | 2011-05-16 | |
|/ / / | |||
| * | | Dafny: added some test cases that use nat | 2011-05-16 | |
| | | | |||
| * | | Dafny: added optional range expressions to logical quantifiers, preparing ↵ | 2011-05-15 | |
|/ / | | | | | | | for addition other other comprehensions (like set comprehension) | ||
* | | Merge | 2011-05-14 | |
|\ \ | |||
* | | | Dafny: fixed bug in quantifier bounds discovery | 2011-05-14 | |
| | | | |||
| * | | Boogie build failed | 2011-05-14 | |
|/ / | |||
* | | Dafny: fixed typo in parser code | 2011-05-13 | |
| | | |||
* | | Merge | 2011-05-13 | |
|\ \ | |||
* | | | Boogie: added features to help with modular verification. In particular, ↵ | 2011-05-13 | |
| | | | | | | | | | | | | define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations. | ||
* | | | Cleaner version of ghost loop termination example. | 2011-05-13 | |
| | | | |||
* | | | Add source file (Expression Design) for the BVD icon in case anyone ever ↵ | 2011-05-12 | |
| | | | | | | | | | | | | needs it | ||
* | | | Dafny: fixed bugs in resolution of multi-dimensional arrays | 2011-05-12 | |
| | | | |||
* | | | Merge | 2011-05-12 | |
|\ \ \ | |||
* | | | | Dafny: forbid "decreases *" on ghost loops | 2011-05-12 | |
| | | | | |||
| | | * | Merge | 2011-05-12 | |
| | | |\ | | |_|/ | |/| | | |||
| | | * | Trying to fix the bound expression simplifier. | 2011-05-12 | |
| | | | | |||
| * | | | added examples of generics and string support needed by Poirot | 2011-05-12 | |
|/ / / | |||
* | | | Merge | 2011-05-11 | |
|\ \ \ | |||
* | | | | More files for Hg to ignore | 2011-05-11 | |
| | | | | |||
| * | | | first cut at handling generics | 2011-05-11 | |
| | |/ | |/| | |||
| | * | Dafny: | 2011-05-11 | |
| | | | | | | | | | | | | | | | | | | * added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword) * check that arrays are not null when accessed * added dafny1/FindZero.dfy test case | ||
* | | | Merge | 2011-05-11 | |
|\ \ \ | |||
* | | | | Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵ | 2011-05-11 | |
| |/ / |/| | | | | | | | | avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation | ||
| * | | Dafny: Fixed non-compiling C# code in DafnyRuntime.cs | 2011-05-11 | |
| | | | |||
* | | | simplified the translation of assignments | 2011-05-10 | |
| | | | |||
* | | | Merge | 2011-05-10 | |
|\ \ \ | |||
* | | | | Oops. Last checkin did not contain the changes for the catch clause change when | 2011-05-10 | |
| | | | | | | | | | | | | | | | | translating a method body. | ||
* | | | | Changed the way variables corresponding to events are created. If the compiler | 2011-05-10 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | has already generated a field with the same name as the event (as it does for events that do *not* declare their own adder/remover methods), then a variable is generated from that field. Otherwise a variable is created using the event name. Changed the catch handler for translating a method body so any exception causes that method implementation to be skipped, but the translation to continue. Since the procedure has already been declared this means that the translated program might be underspecified since some method implementations might be missing, but at least the program should be able to be given to Boogie. | ||
| * | | | Don't set logic to UFNIA when /useArrayTheory | 2011-05-09 | |
| | | | | |||
* | | | | always translate enums as ints. | 2011-05-09 | |
|/ / / | |||
* | | | More support for reals, especially real constants. | 2011-05-08 | |
| | | | |||
* | | | Better error handling. | 2011-05-08 | |
| | | | | | | | | | | | | | | | Defined a new Boogie type, Real, that will be used to represent floating point numbers. | ||
* | | | Merge | 2011-05-06 | |
|\ \ \ | |||
* | | | | Cleanup of new LHS simplification and replaced the golden output with the | 2011-05-06 | |
| | | | | | | | | | | | | | | | | new regression output. | ||
* | | | | simplifying lhs of assignment statements. | 2011-05-05 | |
| | | | | |||
| * | | | added a few more axioms | 2011-05-04 | |
|/ / / | |||
* | | | Merge | 2011-05-04 | |
|\ \ \ | |||
* | | | | fixed a bug in block coalescer. previously, an unreachable block could have ↵ | 2011-05-04 | |
| | | | | | | | | | | | | | | | | as a target a block that was coalesced. this caused a contract to fail downstream (under checked build). in the new behavior, the new blocks after coalescing only contain reachable blocks. | ||
| * | | | Boogie build succeeded | 2011-05-04 | |
|/ / / | |||
* | | | Uniquified constant names generated for string literals | 2011-05-03 | |
| | | | | | | | | | | | | Also did some more substitutions to get valid Boogie identifiers | ||
* | | | LetVC can get null label2absy from lazy inlining. So, I weakened the ↵ | 2011-05-03 | |
| | | | | | | | | | | | | precondition otherwise the checked build was failing |