Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | Added "procedure-copy bounding" for lazy inlining | Unknown | 2011-08-10 | |
| | | | | ||||
| | * | | Merge | qadeer | 2011-08-10 | |
| | |\ \ | | |/ / | |/| | | ||||
| * | | | (phone) slicing to avoid self loops | t-espave | 2011-08-09 | |
| | | | | ||||
| | * | | Merge | qadeer | 2011-08-09 | |
| | |\ \ | ||||
| | * | | | further updates to bit vector analysis | qadeer | 2011-08-09 | |
| | | | | | ||||
| * | | | | phone nav building stats | t-espave | 2011-08-09 | |
| | | | | | ||||
| * | | | | phone nav building "doc" | t-espave | 2011-08-09 | |
| | |/ / | |/| | | ||||
| * | | | (phone) fully automated phone nav graph building | t-espave | 2011-08-09 | |
| | | | | ||||
| | * | | Merge | qadeer | 2011-08-09 | |
| | |\ \ | | |/ / | |/| | | ||||
| | * | | more changes to bitvector analysis | qadeer | 2011-08-09 | |
| | | | | ||||
| * | | | Merge | t-espave | 2011-08-08 | |
| |\| | | ||||
| * | | | (phone bct) filtering out nonpages for boogie queries, faster but maybe a ↵ | t-espave | 2011-08-08 | |
|/ / / | | | | | | | | | | | | | | | | | | | less precise preparing boogie code for static unrolls filtering out some navigations | |||
| * | | another bug fix in bct | qadeer | 2011-08-08 | |
| | | | ||||
| * | | added a new file and fixed a bug in bct | qadeer | 2011-08-08 | |
| | | | ||||
| * | | Merge | qadeer | 2011-08-08 | |
| |\ \ | |/ / |/| | | ||||
| * | | various changes to boogie for bitvector analysis and bctprovider | qadeer | 2011-08-08 | |
| | | | ||||
| | * | Fix null-ref | Michal Moskal | 2011-08-07 | |
| | | | ||||
* | | | Added option "getMeHere" so that calls to GetMeHere.Assert(e) become "assert e" | Mike Barnett | 2011-08-06 | |
|/ / | | | | | | | | | | | | | (which really could be done just by defining it that way in an assembly either via a contract or else by inlining it). But more importantly the option causes all assertions to be translated as assumptions. Still to do: postconditions should be translated as "free ensures". | |||
* | | fixed a bug in delegate dispatcher name for generic invoke methods | qadeer | 2011-08-05 | |
| | | ||||
* | | further updates to bctprovider | qadeer | 2011-08-05 | |
| | | ||||
* | | (phone bct) nav graph building (mostly) automated | t-espave | 2011-08-05 | |
| | | ||||
* | | (phone bct) nav graph building (mostly) automated | t-espave | 2011-08-05 | |
| | | ||||
* | | Merge | Aleksandar Milicevic | 2011-08-05 | |
|\ \ | ||||
* | | | Jennisys: | Aleksandar Milicevic | 2011-08-05 | |
| | | | | | | | | | | | | - small fixes to the modular synthesis | |||
| * | | first add | qadeer | 2011-08-05 | |
| | | | ||||
| * | | fixed the key signing problem with houdini | qadeer | 2011-08-05 | |
| | | | | | | | | | | | | started adding bct provider | |||
| * | | further changes for making houdini work | qadeer | 2011-08-04 | |
| | | | ||||
| * | | Merge | qadeer | 2011-08-04 | |
| |\ \ | ||||
| * | | | cleaned up houdini options | qadeer | 2011-08-04 | |
| | | | | ||||
| | * | | Merge | Rustan Leino | 2011-08-04 | |
| | |\ \ | ||||
| | | * \ | 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! | |||
| | * | | | Merge | qadeer | 2011-08-04 | |
| | |\ \ \ | ||||
| | * | | | | full port of houdini project | qadeer | 2011-08-04 | |
| | | | | | | ||||
| * | | | | | Merge | t-espave | 2011-08-04 | |
| |\ \ \ \ \ | | | |/ / / | | |/| | | | ||||
| * | | | | | (phone bct) monitoring pivot controls | t-espave | 2011-08-04 | |
| | | | | | | ||||
| | * | | | | Chalice: Add comment to a broken test-case. | stefanheule | 2011-08-04 | |
| | | | | | | ||||
| | | | * | | Dafny: added reverse*reverse=id example to test suite | Rustan Leino | 2011-08-04 | |
| | | | | | | ||||
| | | | * | | Dafny: for VS mode, let lexer allow "?" | Rustan Leino | 2011-08-04 | |
| | | | | | | ||||
| | * | | | | Chalie: Fix Visual Studio integration and add note about JVM stack size ↵ | stefanheule | 2011-08-04 | |
| |/ / / / |/| | | | | | | | | | | | | | | problems. | |||
| | * | | | Merge | qadeer | 2011-08-03 | |
| | |\ \ \ | |_|/ / / |/| | | | | ||||
| | * | | | ported Houdini to C#, added Houdini project to the Boogie solution | qadeer | 2011-08-03 | |
| | | | | | ||||
* | | | | | Merge | Aleksandar Milicevic | 2011-08-03 | |
|\ \ \ \ \ | ||||
* | | | | | | Jennisys: | Aleksandar Milicevic | 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 | 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. |