summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Added subtyping axiomatization.Gravatar Mike Barnett2011-07-20
|
* Chalice: Use "/smoke" for the test suite by default to ensure test quality. ↵Gravatar stefanheule2011-07-20
| | | | Update all reference outputs accordingly.
* Chalice: improve smoke testing to use the subsumption option only for the ↵Gravatar stefanheule2011-07-20
| | | | "assert false" statements.
* Chalice: Improve command line help and allow both "-param" (old) and ↵Gravatar stefanheule2011-07-20
| | | | "/param" (new), similar to Boogie.
* Chalice: Uniform usage of Boogie syntax for functions.Gravatar stefanheule2011-07-20
|
* MergeGravatar Unknown2011-07-19
|\
| * - added synthesized code for the examplesGravatar Unknown2011-07-19
| |
| * - added synthesis of Repr stuff (it generates Repr invariants,Gravatar Unknown2011-07-19
| | | | | | | | | | | | | | | | | | and updates the Repr fields at the end of every constructor) - refactoring: - removed ExprConst - change the implementation to use HeapModel and HeapInstance (as opposed to propagating heap/env/ctx)
* | edited out phoneplugin from most placesGravatar Unknown2011-07-19
| | | | | | | | | | havoc'ing uri when navigation cannot be determined (partial) added boilerplate boogie code
* | Chalice: Fix all three copyless message passing programs. There were ↵Gravatar stefanheule2011-07-19
| | | | | | | | problems in the specification (all three programs) and the program itself ("..with-ack2"). Furthermore, if only two types of messages can be sent, a boolean flag is now used instead of an integer (to simplify the specifications).
* | Chalice: Fix two nasty bugs that could lead to contradictions in the Boogie ↵Gravatar stefanheule2011-07-19
| | | | | | | | encoding for certain programs. See workitems 10203 and 10204.
* | Chalice: Fix batch file problem and update reference output.Gravatar stefanheule2011-07-19
| |
* | boogie boilerplate code generator for phone verif.Gravatar Unknown2011-07-18
| |
* | bugfix, was not setting control handlersGravatar Unknown2011-07-18
| |
* | Chalice: Smoke testing to find unreachable code, preconditions that are ↵Gravatar stefanheule2011-07-18
| | | | | | | | equivalent to false and assumptions that introduce contradictions. Can be used with the command line switch "-smoke".
* | Chalice: Also exhale correctly in two steps for multiple contracts (e.g. two ↵Gravatar stefanheule2011-07-18
| | | | | | | | preconditions), and include missing well-formedness assumption afer async method calls.
* | Chalice: Fix a problem with permission expressions. Prevsiously, exhaling ↵Gravatar stefanheule2011-07-18
| | | | | | | | "acc(o.f,100-rd) && acc(o.f,rd)" resulted in a contradiction. This is now solved by using a two-step exhale (loosely speaking, read permissions and functional properties are exhaled first, and only afterwards all other permissions). Extended testcases appropriately.
* | MergeGravatar Jason Koenig2011-07-15
|\ \
* \ \ MergeGravatar Jason Koenig2011-07-15
|\ \ \
* | | | Reverting accidental modification in changeset 58325a6e6ed3.Gravatar Jason Koenig2011-07-15
| | | |
* | | | Fixed regression test failures due to removal of bodiless methods and functions.Gravatar Jason Koenig2011-07-15
| | | |
| | * | potentially useful boogie stubs, commented out since they may conflict with ↵Gravatar Unknown2011-07-15
| | | | | | | | | | | | | | | | {:extern}
| | * | MergeGravatar Unknown2011-07-15
| | |\ \
| | * | | - keeping track of BCT name changes to controlsGravatar Unknown2011-07-15
| |/ / / | | | | | | | | | | | | - injecting navigation changes code
| | * | MergeGravatar Unknown2011-07-16
| | |\ \
| | * | | Suppress generation of Drop(s, 0). This expression caused unnecessary ↵Gravatar Unknown2011-07-16
| | | | | | | | | | | | | | | | | | | | verification problems, even though the axioms should be sufficient to handle this case (and also trigger).
| | | * | MergeGravatar qadeer2011-07-15
| | | |\ \
| | | * | | commenting out axiom generationGravatar qadeer2011-07-15
| | |/ / / | |/| | |
* | | | | Added compilation support for multisets and sequences from arrays.Gravatar Jason Koenig2011-07-15
| | | | |
| * | | | MergeGravatar Unknown2011-07-15
| |\ \ \ \
| * | | | | initial page detection and initGravatar Unknown2011-07-15
| | | | | |
| | * | | | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵Gravatar wuestholz2011-07-15
| | | |_|/ | | |/| | | | | | | | | | | | some trailing whitespace.
| | * | | MergeGravatar Unknown2011-07-14
| | |\ \ \
| | * | | | - implemented synthesizing constructors with if conditionsGravatar Unknown2011-07-14
| | | | | | | | | | | | | | | | | | | | | | | | - added some number examples (Number.jen)
* | | | | | Fixed failing regression tests.Gravatar Jason Koenig2011-07-14
| | | | | |
* | | | | | MergeGravatar Jason Koenig2011-07-14
|\ \ \ \ \ \ | | |_|/ / / | |/| | | |
* | | | | | MergeGravatar Jason Koenig2011-07-14
|\ \ \ \ \ \
* | | | | | | Strengthened axioms for multisets and sequences.Gravatar Jason Koenig2011-07-14
| | | | | | |
* | | | | | | Fixed bug where wellformedness for E in multiset(E) was checked in the "old" ↵Gravatar Jason Koenig2011-07-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | context.
| | | | | | * MergeGravatar qadeer2011-07-14
| | | | | | |\ | | | |_|_|_|/ | | |/| | | |
| | | | | | * temporarily quantifying out axioms generationGravatar qadeer2011-07-14
| | | | | | |
| | | * | | | some uri tracking statements injectedGravatar Unknown2011-07-14
| | | | | | |
| | * | | | | MergeGravatar Mike Barnett2011-07-14
| | |\| | | |
| | * | | | | Add a translation for switch statements.Gravatar Mike Barnett2011-07-14
| | | |_|_|/ | | |/| | | | | | | | | | | | | | | Updated regression output due to Shaz's changes for exception handling.
| | | * | | more static URI detectionGravatar Unknown2011-07-14
| | | |\ \ \ | | | |/ / / | | |/| | |
| | | * | | - navigation event detectionGravatar Unknown2011-07-14
| | | | | | | | | | | | | | | | | | | | | | | | - (some) URI declaration/instantiation and use detection
| | * | | | MergeGravatar qadeer2011-07-13
| | |\ \ \ \ | | |/ / / / | |/| | | |
| | | | * | - finished evaluating expressionsGravatar Unknown2011-07-13
| | |_|/ / | |/| | |
| | * | | removed extraneous commented codeGravatar qadeer2011-07-13
| | | | |
| | * | | implemented Mike's proposal for dynamic dispatch for finally blocksGravatar qadeer2011-07-13
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-07 22:33:31 +0000