summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Boogie: Removed an incorrect Ensures clause on a void method.Gravatar tabarbe2010-08-27
|
* fixed bug with function name look upGravatar qadeer2010-08-27
|
* Boogie: Changed the cce classes into one separate project, which every other ↵Gravatar tabarbe2010-08-27
| | | | project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
* Boogie: Adding an autobuild and regression cmd file for Boogie and Dafny - ↵Gravatar tabarbe2010-08-27
| | | | Cleans and builds both projects, then executes the regressions if the build succeeded. If the build had failed, it will stop the script.
* Boogie: Added Z3api to the build configuration.Gravatar tabarbe2010-08-27
|
* Boogie: Changed a messed-up refference to Z3api back to its previous state.Gravatar tabarbe2010-08-27
|
* Boogie: Basetypes port 3/3: Committing changed referencesGravatar tabarbe2010-08-27
| | | | Z3api.csproj shouldn't get in the way this time 'round.
* Boogie: Basetypes port 2/3: Committing new source file, deleting old oneGravatar tabarbe2010-08-27
|
* Boogie: Basetypes port 1/3: Committing new sourcesGravatar tabarbe2010-08-27
|
* Boogie: Renaming the Basetypes sources in preparation for my port commit.Gravatar tabarbe2010-08-27
|
* Bug fixes and logging for z3apiGravatar akashlal2010-08-27
|
* Addint ignore file for GITGravatar stobies2010-08-27
|
* added some more apis to Z3apiGravatar qadeer2010-08-27
| | | | also added a reference from BoogieDriver to z3api
* Added a (temporary) CCE file so that Z3Api can build.Gravatar mikebarnett2010-08-27
|
* simplified the push-pop businessGravatar qadeer2010-08-27
|
* minor errorGravatar qadeer2010-08-27
|
* Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵Gravatar tabarbe2010-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 oneGravatar tabarbe2010-08-27
|
* Boogie: Graph port 1/3: Committing new sourcesGravatar tabarbe2010-08-27
|
* Boogie: Renaming the Graph files in preparation for the commit of my port.Gravatar tabarbe2010-08-27
|
* Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵Gravatar tabarbe2010-08-26
| | | | Core to jive with recent changes made to the cce class.
* Boogie: AIFramework port part 2/3: Committing needed source file, deleting ↵Gravatar tabarbe2010-08-26
| | | | unnecessarry one.
* Boogie: AIFramework port part 1/3: Committing new sources.Gravatar tabarbe2010-08-26
|
* Boogie: Renaming the AIFramework sources in preparation for committal of my ↵Gravatar tabarbe2010-08-26
| | | | port of the project
* Minor additions to z3apiGravatar akashlal2010-08-26
|
* bug fixes in z3apiGravatar qadeer2010-08-26
|
* Boogie build failedGravatar codeplexbot2010-08-25
|
* fixed z3api so that it works on small examples now.Gravatar qadeer2010-08-24
|
* Boogie build failedGravatar codeplexbot2010-08-24
|
* Chalice: working out mask transfers between concrete and abstract heaps -- ↵Gravatar kyessenov2010-08-24
| | | | next goal is to make this verify!
* Chalice:Gravatar kyessenov2010-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 ↵Gravatar kyessenov2010-08-23
| | | | translation; tag global coupling assertions (bug fix)
* Chalice: copy concrete values for every permission in coupling invariants of ↵Gravatar kyessenov2010-08-23
| | | | "this"
* Report a bug in Z3 instead of evil input "?"Gravatar kyessenov2010-08-23
|
* Added a short description of new flags added to Boogie.Gravatar akashlal2010-08-23
|
* Disabled an expensive contract check. Instead, only check things that are ↵Gravatar akashlal2010-08-23
| | | | actually used.
* Chalice:Gravatar kyessenov2010-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.Gravatar qadeer2010-08-23
|
* Boogie build failedGravatar codeplexbot2010-08-23
|
* Fixed external references to other projects in the solution.Gravatar mikebarnett2010-08-23
| | | | Added version.cs to the project.
* Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces ↵Gravatar kyessenov2010-08-22
| | | | evil input again...
* Chalice: start of a DSW refinementGravatar kyessenov2010-08-22
|
* Chalice: refining lists doesn't quite work yet...Gravatar kyessenov2010-08-22
|
* Chalice: limited functions are still problematic (see Calculator.chalice)Gravatar kyessenov2010-08-22
|
* Chalice:Gravatar kyessenov2010-08-22
| | | | * coupling invariants work (with certain restrictions as described in TODO comments)
* Boogie build failedGravatar codeplexbot2010-08-21
|
* Chalice:Gravatar kyessenov2010-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 renameGravatar kyessenov2010-08-21
|
* Boogie: Changed reference of Z3api.csproj to the differently-GUIDded ↵Gravatar tabarbe2010-08-20
| | | | Core.csproj, rather than Core.sscproj's old GUID.
* Boogie: Committing changed referencesGravatar tabarbe2010-08-20
|