summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* MergeGravatar t-espave2011-07-26
|\
| * added translation for RightShift and LeftShiftGravatar Unknown2011-07-26
* | bugfix on null assignmentsGravatar t-espave2011-07-26
* | tracking new controlsGravatar t-espave2011-07-26
* | ignoring (some) non-feedback producing event handlersGravatar t-espave2011-07-26
|/
* MergeGravatar t-espave2011-07-26
|\
* | weeding out non-set $exception as feedback handling issuesGravatar t-espave2011-07-26
| * MergeGravatar Rustan Leino2011-07-26
| |\
* | | ui handlers override checked for output geenrationGravatar t-espave2011-07-26
| | * - restored the "old" (as it was before switching from map to list)Gravatar Unknown2011-07-25
| | * - changed heapInst.assignments' type from Map to List (because assignment or...Gravatar Unknown2011-07-25
* | | MergeGravatar t-espave2011-07-25
|\ \ \ | | |/ | |/|
* | | adding checks and code injection for phone feedback checkingGravatar t-espave2011-07-25
| | * MergeGravatar Rustan Leino2011-07-25
| | |\ | | |/ | |/|
| * | MergeGravatar Unknown2011-07-22
| |\ \ | |/ / |/| |
* | | tracking main phone application class and ctorsGravatar t-espave2011-07-22
* | | typoGravatar t-espave2011-07-22
* | | double definition fixGravatar t-espave2011-07-22
* | | Chalice: Check definedness of where-clause of channels (was missing before), ...Gravatar stefanheule2011-07-22
* | | Chalice: Improve smoke testing: look for preconditions of functions, predicat...Gravatar stefanheule2011-07-22
| * | Jennisys: added Jennesys/Jennesys/examples/bak to hgignoreGravatar Unknown2011-07-21
| * | Jennisys:Gravatar Unknown2011-07-21
| | * MergeGravatar Rustan Leino2011-07-21
| | |\
| | * | Dafny: call previous lemma instead of restating itGravatar Rustan Leino2011-07-21
* | | | cleanupGravatar t-espave2011-07-21
| |_|/ |/| |
* | | MergeGravatar t-espave2011-07-21
|\ \ \
* | | | dynamic navigation variable tracking and base page name trackingGravatar Unknown2011-07-21
| * | | Chalice: Only show the "first" smoke warning, as once the prover is able to s...Gravatar stefanheule2011-07-21
* | | | unified URI format across translationsGravatar Unknown2011-07-21
|/ / /
* | | setting $Exception explicitly to null in phone translationGravatar Unknown2011-07-20
* | | fixed a bug on current nav trackingGravatar Unknown2011-07-20
* | | MergeGravatar Jason Koenig2011-07-20
|\| |
* | | MergeGravatar Jason Koenig2011-07-20
|\ \ \
| | * \ MergeGravatar Unknown2011-07-20
| | |\ \
| | * | | - changed the way Valid() is unrolledGravatar Unknown2011-07-20
| | | * | updated translation of catch clauses to use SubtypeGravatar qadeer2011-07-20
| | |/ /
| | * | Added subtyping axiomatization.Gravatar Mike Barnett2011-07-20
| | * | Chalice: Use "/smoke" for the test suite by default to ensure test quality. U...Gravatar stefanheule2011-07-20
| | * | Chalice: improve smoke testing to use the subsumption option only for the "as...Gravatar stefanheule2011-07-20
| | * | Chalice: Improve command line help and allow both "-param" (old) and "/param"...Gravatar stefanheule2011-07-20
| | * | 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
| | * | | edited out phoneplugin from most placesGravatar Unknown2011-07-19
| |/ / /
* | | | Fixed axiom for Take/Update commuting.Gravatar Jason Koenig2011-07-19
| * | | Chalice: Fix all three copyless message passing programs. There were problems...Gravatar stefanheule2011-07-19
| * | | Chalice: Fix two nasty bugs that could lead to contradictions in the Boogie e...Gravatar stefanheule2011-07-19
| * | | Chalice: Fix batch file problem and update reference output.Gravatar stefanheule2011-07-19
| * | | boogie boilerplate code generator for phone verif.Gravatar Unknown2011-07-18