Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Boogie: Basetypes port 2/3: Committing new source file, deleting old one | 2010-08-27 | |
| | |||
* | Boogie: Basetypes port 1/3: Committing new sources | 2010-08-27 | |
| | |||
* | Boogie: Renaming the Basetypes sources in preparation for my port commit. | 2010-08-27 | |
| | |||
* | Bug fixes and logging for z3api | 2010-08-27 | |
| | |||
* | Addint ignore file for GIT | 2010-08-27 | |
| | |||
* | added some more apis to Z3api | 2010-08-27 | |
| | | | | also added a reference from BoogieDriver to z3api | ||
* | Added a (temporary) CCE file so that Z3Api can build. | 2010-08-27 | |
| | |||
* | simplified the push-pop business | 2010-08-27 | |
| | |||
* | minor error | 2010-08-27 | |
| | |||
* | Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵ | 2010-08-27 | |
| | | | | files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min. | ||
* | Boogie: Graph port 2/3: Committing new source file, deleting old one | 2010-08-27 | |
| | |||
* | Boogie: Graph port 1/3: Committing new sources | 2010-08-27 | |
| | |||
* | Boogie: Renaming the Graph files in preparation for the commit of my port. | 2010-08-27 | |
| | |||
* | Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵ | 2010-08-26 | |
| | | | | Core to jive with recent changes made to the cce class. | ||
* | Boogie: AIFramework port part 2/3: Committing needed source file, deleting ↵ | 2010-08-26 | |
| | | | | unnecessarry one. | ||
* | Boogie: AIFramework port part 1/3: Committing new sources. | 2010-08-26 | |
| | |||
* | Boogie: Renaming the AIFramework sources in preparation for committal of my ↵ | 2010-08-26 | |
| | | | | port of the project | ||
* | Minor additions to z3api | 2010-08-26 | |
| | |||
* | bug fixes in z3api | 2010-08-26 | |
| | |||
* | Boogie build failed | 2010-08-25 | |
| | |||
* | fixed z3api so that it works on small examples now. | 2010-08-24 | |
| | |||
* | Boogie build failed | 2010-08-24 | |
| | |||
* | Chalice: working out mask transfers between concrete and abstract heaps -- ↵ | 2010-08-24 | |
| | | | | next goal is to make this verify! | ||
* | Chalice: | 2010-08-24 | |
| | | | | | * fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals * example of finding duplicate elements in a sequence using a bitset | ||
* | Chalice: exhale spec statement post condition in refinement block ↵ | 2010-08-23 | |
| | | | | translation; tag global coupling assertions (bug fix) | ||
* | Chalice: copy concrete values for every permission in coupling invariants of ↵ | 2010-08-23 | |
| | | | | "this" | ||
* | Report a bug in Z3 instead of evil input "?" | 2010-08-23 | |
| | |||
* | Added a short description of new flags added to Boogie. | 2010-08-23 | |
| | |||
* | Disabled an expensive contract check. Instead, only check things that are ↵ | 2010-08-23 | |
| | | | | actually used. | ||
* | Chalice: | 2010-08-23 | |
| | | | | | | * added celebrity example (theory of sequences is still weak to prove basic things...) * bug in Chalice: old in while loops is ignored, needs to be fixed if ever want to complete DSW example * evil input from Z3 makes subsequent refinement proofs unsound; need to debug before building upon DSW.chalice; the error is triggered when adding parent field to Node | ||
* | further fixes to Z3api project trying to make it work; still a long way off. | 2010-08-23 | |
| | |||
* | Boogie build failed | 2010-08-23 | |
| | |||
* | Fixed external references to other projects in the solution. | 2010-08-23 | |
| | | | | Added version.cs to the project. | ||
* | Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces ↵ | 2010-08-22 | |
| | | | | evil input again... | ||
* | Chalice: start of a DSW refinement | 2010-08-22 | |
| | |||
* | Chalice: refining lists doesn't quite work yet... | 2010-08-22 | |
| | |||
* | Chalice: limited functions are still problematic (see Calculator.chalice) | 2010-08-22 | |
| | |||
* | Chalice: | 2010-08-22 | |
| | | | | * coupling invariants work (with certain restrictions as described in TODO comments) | ||
* | Boogie build failed | 2010-08-21 | |
| | |||
* | Chalice: | 2010-08-21 | |
| | | | | | * fix a compilation problem (scalac relied on old binaries) * combinator parser and state don't work well together -- added higher-order parser for method transform | ||
* | server-side rename | 2010-08-21 | |
| | |||
* | Boogie: Changed reference of Z3api.csproj to the differently-GUIDded ↵ | 2010-08-20 | |
| | | | | Core.csproj, rather than Core.sscproj's old GUID. | ||
* | Boogie: Committing changed references | 2010-08-20 | |
| | |||
* | Boogie: Adding required source file, deleting no-longer-necessarry one | 2010-08-20 | |
| | |||
* | Boogie: Committing changed source files | 2010-08-20 | |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | 2010-08-20 | |
| | | | | *The deletion part of the rename did not occur | ||
* | Boogie: Renaming core sources in preparation for port commit | 2010-08-20 | |
| | |||
* | Added the port of Z3api. It is simply a port to the latest version of ↵ | 2010-08-20 | |
| | | | | Microsoft.Z3.dll and to C#. It does not work yet. | ||
* | Boogie: Fixed some doubly-inherited-contract occurrences. | 2010-08-20 | |
| | |||
* | Boogie: Fixed some doubly-inherited-contract occurrences. | 2010-08-20 | |
| |