Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | 2011-08-04 | |
|\ | |||
* | | Added new option /captureState (/c) for generating a capture state assumption | 2011-08-04 | |
| | | | | | | | | after each statement. | ||
| * | Merge | 2011-08-04 | |
| |\ | |/ |/| | |||
| * | (phone bct) anonymous control support | 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. | 2011-08-04 | |
| | | | | | | | | If a method's parameters don't have names, give them names! | ||
* | | Merge | 2011-08-04 | |
|\ \ | |||
* | | | full port of houdini project | 2011-08-04 | |
| | | | |||
| | * | Merge | 2011-08-04 | |
| | |\ | | |/ | |/| | |||
| | * | (phone bct) monitoring pivot controls | 2011-08-04 | |
| | | | |||
| * | | Chalice: Add comment to a broken test-case. | 2011-08-04 | |
| | | | |||
| * | | Chalie: Fix Visual Studio integration and add note about JVM stack size ↵ | 2011-08-04 | |
| | | | | | | | | | | | | problems. | ||
* | | | Merge | 2011-08-03 | |
|\| | | |||
* | | | ported Houdini to C#, added Houdini project to the Boogie solution | 2011-08-03 | |
| | | | |||
| * | | Merge | 2011-08-03 | |
| |\ \ | |||
| * | | | Jennisys: | 2011-08-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | - moved modularization and method unification stuff to their own modules - improved the modular synthesis so that whole branches can be delegated to existing methods. | ||
| | | * | (phone bct) moved some code to urihelper | 2011-08-03 | |
| | | | | |||
| | | * | Merge | 2011-08-03 | |
| | | |\ | | | |/ | | |/| | |||
| | * | | Increase the name mangling to avoid name clashes in the Boogie program. In IL, | 2011-08-03 | |
| | | | | | | | | | | | | | | | | members of a type can have the same name. | ||
| | | * | (phone bct) user feedback, showing possibly anomalous nav targets | 2011-08-03 | |
| | |/ | | | | | | | | | | (bct) '+' invalid in string literals | ||
| | * | Merge | 2011-08-03 | |
| | |\ | |||
| | * | | typo | 2011-08-03 | |
| | | | | |||
| | | * | Chalice: Add regression tests for all fixed bugs and separate the tests in ↵ | 2011-08-03 | |
| | | | | | | | | | | | | | | | | 'examples' into "read" examples and general tests. | ||
| | | * | Chalice: only show warning about misleading smoke warnings if there are ↵ | 2011-08-03 | |
| | | | | | | | | | | | | | | | | actually smoke warnings. | ||
| | | * | Chalice: Improve command line interface. Unknown options are no longer ↵ | 2011-08-03 | |
| | | | | | | | | | | | | | | | | silently passed to Boogie (but passing them to Boogie is still possible with /boogieOpt), and Chalice shows a message when it expects input from stdin. | ||
| | | * | Chalice VS integration: recognize string literals | 2011-08-03 | |
| | |/ | |/| | |||
| * | | Merge | 2011-08-02 | |
| |\| | |||
| * | | Jennisys: implemented a unification algorithm that tries to find an existing | 2011-08-02 | |
| | | | | | | | | | | | | method that matches (specification-wise) a synthesized one | ||
| | * | (phone bct) tracking targets of back key navs. | 2011-08-02 | |
| | | | |||
| | * | Merge | 2011-08-02 | |
| | |\ | |_|/ |/| | | |||
| | * | (phone bct) default URI checks inlined | 2011-08-02 | |
| | | | | | | | | | | | | inlining statistics | ||
* | | | Unicode surrogate characters cannot be handled by Boogie. For now (forever?) | 2011-08-02 | |
| | | | | | | | | | | | | just delete them from the identifier that represents each literal string. | ||
| | * | (phone bct) methods inlined for modular analysis (fix) | 2011-08-02 | |
| |/ |/| | |||
* | | Chalice: Add sbt to the repository. | 2011-08-02 | |
| | | |||
* | | Chalice: Chalice is now built using sbt (simple built tool). | 2011-08-02 | |
| | | |||
* | | further fixes in the translation of compiletime constants | 2011-08-01 | |
| | | |||
* | | Merge | 2011-08-01 | |
|\ \ | |||
* | | | (phone bct) compute fixpoint for necessary inlined methods (for modular ↵ | 2011-08-01 | |
| | | | | | | | | | | | | analysis) | ||
* | | | control parsing creates batch file with several calls to corral for graph ↵ | 2011-08-01 | |
| | | | | | | | | | | | | building. lacks some automation still | ||
| * | | Fix in the assertion injector for putting the output on top of the input | 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 | 2011-08-01 | |
|/ / | |||
* | | Merge | 2011-08-01 | |
|\| | |||
* | | fix for exception when phoneControls are not set | 2011-08-01 | |
| | | |||
| * | Merge | 2011-07-29 | |
| |\ | |/ |/| | |||
| * | Jennisys: (1) fixed a bug in "TryInferConditionals"; (2) added synthesized ↵ | 2011-07-29 | |
| | | | | | | | | modular code | ||
| * | Jennisys: | 2011-07-29 | |
| | | | | | | | | | | | | - finished the initial version of the modular code for constructors (excluding the unification part where it tries to find an existing function that meets the required spec) | ||
* | | more phone controls tracked for feedback | 2011-07-29 | |
| | | |||
* | | anonymous phone controls fix | 2011-07-29 | |
| | | |||
* | | Merge | 2011-07-28 | |
|\ \ | |||
* | | | more input/output control handling for phones | 2011-07-28 | |
| | | | |||
| * | | release build should not have z3api being built | 2011-07-28 | |
| | | |