summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator
Commit message (Collapse)AuthorAge
* MergeGravatar Mike Barnett2011-08-04
|\
* | Added new option /captureState (/c) for generating a capture state assumptionGravatar Mike Barnett2011-08-04
| | | | | | | | after each statement.
| * MergeGravatar t-espave2011-08-04
| |\ | |/ |/|
| * (phone bct) anonymous control supportGravatar t-espave2011-08-04
| | | | | | | | | | boogie nav graph modular analysis code default uris to lowercase to make life easier
* | Changed name mangling (again) to avoid name clashes.Gravatar Mike Barnett2011-08-04
| | | | | | | | If a method's parameters don't have names, give them names!
| * (phone bct) moved some code to urihelperGravatar t-espave2011-08-03
| |
| * MergeGravatar t-espave2011-08-03
| |\ | |/ |/|
* | Increase the name mangling to avoid name clashes in the Boogie program. In IL,Gravatar Mike Barnett2011-08-03
| | | | | | | | members of a type can have the same name.
| * (phone bct) user feedback, showing possibly anomalous nav targetsGravatar t-espave2011-08-03
|/ | | | (bct) '+' invalid in string literals
* typoGravatar t-espave2011-08-03
|
* (phone bct) tracking targets of back key navs.Gravatar t-espave2011-08-02
|
* MergeGravatar t-espave2011-08-02
|\
* | (phone bct) default URI checks inlinedGravatar t-espave2011-08-02
| | | | | | | | inlining statistics
| * Unicode surrogate characters cannot be handled by Boogie. For now (forever?)Gravatar Mike Barnett2011-08-02
| | | | | | | | just delete them from the identifier that represents each literal string.
* | (phone bct) methods inlined for modular analysis (fix)Gravatar t-espave2011-08-02
|/
* further fixes in the translation of compiletime constantsGravatar qadeer2011-08-01
|
* MergeGravatar t-espave2011-08-01
|\
* | (phone bct) compute fixpoint for necessary inlined methods (for modular ↵Gravatar t-espave2011-08-01
| | | | | | | | analysis)
| * Fix in the assertion injector for putting the output on top of the inputGravatar Mike Barnett2011-08-01
|/ | | | | | assembly. Fix in the Sink so that the consolidated index of a type parameter is computed correctly.
* fix for exception when phoneControls are not setGravatar t-espave2011-08-01
|
* more phone controls tracked for feedbackGravatar t-espave2011-07-29
|
* anonymous phone controls fixGravatar t-espave2011-07-29
|
* more input/output control handling for phonesGravatar t-espave2011-07-28
|
* refactored phonehelperGravatar t-espave2011-07-28
|
* trivial contract for phone event handlersGravatar t-espave2011-07-28
|
* bugfix,nothing was done if no white/blacklist specifiedGravatar t-espave2011-07-28
|
* option bugfixGravatar t-espave2011-07-28
|
* MergeGravatar Mike Barnett2011-07-27
|\
* | Implemented a whitelist/blacklist so translator can ignore certain parts of anGravatar Mike Barnett2011-07-27
| | | | | | | | assembly.
| * fixed right/left shift functions declGravatar t-espave2011-07-27
| |
| * solved uri naming issuesGravatar t-espave2011-07-27
| |
| * not handling property bindings for controls (for now)Gravatar t-espave2011-07-27
| |
| * MergeGravatar t-espave2011-07-27
| |\ | |/ |/|
| * - handler methods with simulated callsGravatar t-espave2011-07-27
| | | | | | | | - easy checks on backstack navigation that may make graph innecessary
* | fixed bug in constant translationGravatar qadeer2011-07-27
|/
* 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
|/ | | | inlining handlers so interproc. analyisis genrates less false alarms
* weeding out non-set $exception as feedback handling issuesGravatar t-espave2011-07-26
| | | | | unified input handler and feedback override moved up assertions before returns
* ui handlers override checked for output geenrationGravatar t-espave2011-07-26
|
* adding checks and code injection for phone feedback checkingGravatar t-espave2011-07-25
|
* tracking main phone application class and ctorsGravatar t-espave2011-07-22
|
* double definition fixGravatar t-espave2011-07-22
| | | | changed functions to maps for control properties
* cleanupGravatar t-espave2011-07-21
|
* dynamic navigation variable tracking and base page name trackingGravatar Unknown2011-07-21
|
* unified URI format across translationsGravatar Unknown2011-07-21
|
* fixed a bug on current nav trackingGravatar Unknown2011-07-20
| | | | refactored methodcall visitor a bit
* updated translation of catch clauses to use SubtypeGravatar qadeer2011-07-20
|