Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | Mike Barnett | 2011-08-04 |
|\ | |||
* | | Added new option /captureState (/c) for generating a capture state assumption | Mike Barnett | 2011-08-04 |
| | | | | | | | | after each statement. | ||
| * | Merge | t-espave | 2011-08-04 |
| |\ | |/ |/| | |||
| * | (phone bct) anonymous control support | t-espave | 2011-08-04 |
| | | | | | | | | | | boogie nav graph modular analysis code default uris to lowercase to make life easier | ||
* | | Changed name mangling (again) to avoid name clashes. | Mike Barnett | 2011-08-04 |
| | | | | | | | | If a method's parameters don't have names, give them names! | ||
| * | (phone bct) monitoring pivot controls | t-espave | 2011-08-04 |
| | | |||
| * | (phone bct) moved some code to urihelper | t-espave | 2011-08-03 |
| | | |||
| * | Merge | t-espave | 2011-08-03 |
| |\ | |/ |/| | |||
* | | Increase the name mangling to avoid name clashes in the Boogie program. In IL, | Mike Barnett | 2011-08-03 |
| | | | | | | | | members of a type can have the same name. | ||
| * | (phone bct) user feedback, showing possibly anomalous nav targets | t-espave | 2011-08-03 |
|/ | | | | (bct) '+' invalid in string literals | ||
* | typo | t-espave | 2011-08-03 |
| | |||
* | (phone bct) tracking targets of back key navs. | t-espave | 2011-08-02 |
| | |||
* | Merge | t-espave | 2011-08-02 |
|\ | |||
* | | (phone bct) default URI checks inlined | t-espave | 2011-08-02 |
| | | | | | | | | inlining statistics | ||
| * | Unicode surrogate characters cannot be handled by Boogie. For now (forever?) | Mike Barnett | 2011-08-02 |
| | | | | | | | | just delete them from the identifier that represents each literal string. | ||
* | | (phone bct) methods inlined for modular analysis (fix) | t-espave | 2011-08-02 |
|/ | |||
* | further fixes in the translation of compiletime constants | qadeer | 2011-08-01 |
| | |||
* | Merge | t-espave | 2011-08-01 |
|\ | |||
* | | (phone bct) compute fixpoint for necessary inlined methods (for modular ↵ | t-espave | 2011-08-01 |
| | | | | | | | | analysis) | ||
* | | control parsing creates batch file with several calls to corral for graph ↵ | t-espave | 2011-08-01 |
| | | | | | | | | building. lacks some automation still | ||
| * | Fix in the assertion injector for putting the output on top of the input | Mike Barnett | 2011-08-01 |
| | | | | | | | | | | | | assembly. Fix in the Sink so that the consolidated index of a type parameter is computed correctly. | ||
* | | generating individual corral queries for page navigation | t-espave | 2011-08-01 |
|/ | |||
* | fix for exception when phoneControls are not set | t-espave | 2011-08-01 |
| | |||
* | more phone controls tracked for feedback | t-espave | 2011-07-29 |
| | |||
* | anonymous phone controls fix | t-espave | 2011-07-29 |
| | |||
* | more input/output control handling for phones | t-espave | 2011-07-28 |
| | |||
* | refactored phonehelper | t-espave | 2011-07-28 |
| | |||
* | trivial contract for phone event handlers | t-espave | 2011-07-28 |
| | |||
* | bugfix,nothing was done if no white/blacklist specified | t-espave | 2011-07-28 |
| | |||
* | option bugfix | t-espave | 2011-07-28 |
| | |||
* | Merge | Mike Barnett | 2011-07-27 |
|\ | |||
* | | New project to support "Get Me Here": an assertion injector that puts into a | Mike Barnett | 2011-07-27 |
| | | | | | | | | binary a call to "Contract.Assert(false)". | ||
* | | Implemented a whitelist/blacklist so translator can ignore certain parts of an | Mike Barnett | 2011-07-27 |
| | | | | | | | | assembly. | ||
| * | fixed right/left shift functions decl | t-espave | 2011-07-27 |
| | | |||
| * | solved uri naming issues | t-espave | 2011-07-27 |
| | | |||
| * | not handling property bindings for controls (for now) | t-espave | 2011-07-27 |
| | | |||
| * | Merge | t-espave | 2011-07-27 |
| |\ | |/ |/| | |||
| * | - handler methods with simulated calls | t-espave | 2011-07-27 |
| | | | | | | | | - easy checks on backstack navigation that may make graph innecessary | ||
* | | Updated regressions. | Mike Barnett | 2011-07-27 |
| | | |||
* | | fixed bug in constant translation | qadeer | 2011-07-27 |
|/ | |||
* | Merge | t-espave | 2011-07-26 |
|\ | |||
| * | added translation for RightShift and LeftShift | Unknown | 2011-07-26 |
| | | |||
* | | bugfix on null assignments | t-espave | 2011-07-26 |
| | | |||
* | | tracking new controls | t-espave | 2011-07-26 |
| | | |||
* | | ignoring (some) non-feedback producing event handlers | t-espave | 2011-07-26 |
|/ | | | | inlining handlers so interproc. analyisis genrates less false alarms | ||
* | weeding out non-set $exception as feedback handling issues | t-espave | 2011-07-26 |
| | | | | | unified input handler and feedback override moved up assertions before returns | ||
* | ui handlers override checked for output geenration | t-espave | 2011-07-26 |
| | |||
* | adding checks and code injection for phone feedback checking | t-espave | 2011-07-25 |
| | |||
* | tracking main phone application class and ctors | t-espave | 2011-07-22 |
| | |||
* | typo | t-espave | 2011-07-22 |
| |