summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* bug fixesGravatar qadeer2011-05-16
|
* Fix break.Gravatar Mike Barnett2011-05-16
|
* new regression outputGravatar Mike Barnett2011-05-16
|\
* \ MergeGravatar Mike Barnett2011-05-16
|\ \
* | | mergeGravatar Mike Barnett2011-05-16
| | |
* | | MergeGravatar Mike Barnett2011-05-16
| | |
| | * Add extern declarations to procedures.Gravatar Mike Barnett2011-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 differentGravatar Mike Barnett2011-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.
| * | MergeGravatar qadeer2011-05-16
| |\ \
| * | | convert assert to requiresGravatar qadeer2011-05-16
|/ / /
| * | Dafny: added some test cases that use natGravatar Rustan Leino2011-05-16
| | |
| * | Dafny: added optional range expressions to logical quantifiers, preparing ↵Gravatar Rustan Leino2011-05-15
|/ / | | | | | | for addition other other comprehensions (like set comprehension)
* | MergeGravatar Rustan Leino2011-05-14
|\ \
* | | Dafny: fixed bug in quantifier bounds discoveryGravatar Rustan Leino2011-05-14
| | |
| * | Boogie build failedGravatar CodeplexBot2011-05-14
|/ /
* | Dafny: fixed typo in parser codeGravatar Rustan Leino2011-05-13
| |
* | MergeGravatar Rustan Leino2011-05-13
|\ \
* | | Boogie: added features to help with modular verification. In particular, ↵Gravatar Rustan Leino2011-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.Gravatar Unknown2011-05-13
| | |
* | | Add source file (Expression Design) for the BVD icon in case anyone ever ↵Gravatar Michal Moskal2011-05-12
| | | | | | | | | | | | needs it
* | | Dafny: fixed bugs in resolution of multi-dimensional arraysGravatar Rustan Leino2011-05-12
| | |
* | | MergeGravatar Rustan Leino2011-05-12
|\ \ \
* | | | Dafny: forbid "decreases *" on ghost loopsGravatar Rustan Leino2011-05-12
| | | |
| | | * MergeGravatar Mike Barnett2011-05-12
| | | |\ | | |_|/ | |/| |
| | | * Trying to fix the bound expression simplifier.Gravatar Mike Barnett2011-05-12
| | | |
| * | | added examples of generics and string support needed by PoirotGravatar 10shb2011-05-12
|/ / /
* | | MergeGravatar Rustan Leino2011-05-11
|\ \ \
* | | | More files for Hg to ignoreGravatar Rustan Leino2011-05-11
| | | |
| * | | first cut at handling genericsGravatar qadeer2011-05-11
| | |/ | |/|
| | * Dafny:Gravatar Rustan Leino2011-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
* | | MergeGravatar Rustan Leino2011-05-11
|\ \ \
* | | | Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵Gravatar Rustan Leino2011-05-11
| |/ / |/| | | | | | | | avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
| * | Dafny: Fixed non-compiling C# code in DafnyRuntime.csGravatar Rustan Leino2011-05-11
| | |
* | | simplified the translation of assignmentsGravatar qadeer2011-05-10
| | |
* | | MergeGravatar Mike Barnett2011-05-10
|\ \ \
* | | | Oops. Last checkin did not contain the changes for the catch clause change whenGravatar Mike Barnett2011-05-10
| | | | | | | | | | | | | | | | translating a method body.
* | | | Changed the way variables corresponding to events are created. If the compilerGravatar Mike Barnett2011-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 /useArrayTheoryGravatar Michal Moskal2011-05-09
| | | |
* | | | always translate enums as ints.Gravatar Mike Barnett2011-05-09
|/ / /
* | | More support for reals, especially real constants.Gravatar Mike Barnett2011-05-08
| | |
* | | Better error handling.Gravatar Mike Barnett2011-05-08
| | | | | | | | | | | | | | | Defined a new Boogie type, Real, that will be used to represent floating point numbers.
* | | MergeGravatar Mike Barnett2011-05-06
|\ \ \
* | | | Cleanup of new LHS simplification and replaced the golden output with theGravatar Mike Barnett2011-05-06
| | | | | | | | | | | | | | | | new regression output.
* | | | simplifying lhs of assignment statements.Gravatar Mike Barnett2011-05-05
| | | |
| * | | added a few more axiomsGravatar qadeer2011-05-04
|/ / /
* | | MergeGravatar qadeer2011-05-04
|\ \ \
* | | | fixed a bug in block coalescer. previously, an unreachable block could have ↵Gravatar qadeer2011-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 succeededGravatar CodeplexBot2011-05-04
|/ / /
* | | Uniquified constant names generated for string literalsGravatar qadeer2011-05-03
| | | | | | | | | | | | Also did some more substitutions to get valid Boogie identifiers
* | | LetVC can get null label2absy from lazy inlining. So, I weakened the ↵Gravatar qadeer2011-05-03
| | | | | | | | | | | | precondition otherwise the checked build was failing
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-30 21:44:00 +0000