Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Adding fixedpoint engine backend | Ken McMillan | 2013-05-07 |
| | |||
* | bunch of refactorings | Unknown | 2012-10-03 |
| | | | | | | | | | - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs | ||
* | Removed AIFramework from Boogie -- use native trivial or native ↵ | boehmes | 2012-09-27 |
| | | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped. | ||
* | Removed abandoned Isabelle prover backend | boehmes | 2012-09-27 |
| | |||
* | testing a fix in SI | qadeer | 2012-06-07 |
| | | | | | also changing back the output path in BoogieDriver also disabling z3api for now since it does not build | ||
* | Trying to merge with recent changes, failing. | Ken McMillan | 2012-06-05 |
|\ | |||
| * | Some changes to support expanded use of z3api. | Ken McMillan | 2012-06-05 |
| | | | | | | | | | | | | | | | | | | | | Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after). | ||
* | | further fixes related to using uninterpreted function for error traces | qadeer | 2012-02-25 |
|/ | | | | removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution | ||
* | moved GPUVerify into its own solution | qadeer | 2011-11-08 |
| | |||
* | Fixed test failures in the "Checked" configuration. | wuestholz | 2011-09-19 |
| | |||
* | Added GPUVerify project | Unknown | 2011-09-02 |
| | |||
* | ported Houdini to C#, added Houdini project to the Boogie solution | qadeer | 2011-08-03 |
| | |||
* | release build should not have z3api being built | Unknown | 2011-07-28 |
| | |||
* | Added a new solution configuration, Checked, that builds the Checked ↵ | mikebarnett | 2011-03-07 |
| | | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration. | ||
* | Copy SMTLib "prover" as a basis for TPTP "prover". | MichalMoskal | 2011-01-18 |
| | |||
* | Factored out the ParserHelper class into a separate project and updated the ↵ | wuestholz | 2010-12-02 |
| | | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#. | ||
* | Put Model.cs in separate assembly. Fix signing/versioning with it. | MichalMoskal | 2010-10-12 |
| | |||
* | Starting work on Boogie Model Viewer. | MichalMoskal | 2010-10-12 |
| | |||
* | Update to VS2010. | MichalMoskal | 2010-10-07 |
| | |||
* | created a new build target called z3apidebug. | qadeer | 2010-08-29 |
| | | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver. | ||
* | Boogie: Changed the cce classes into one separate project, which every other ↵ | tabarbe | 2010-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: Added Z3api to the build configuration. | tabarbe | 2010-08-27 |
| | |||
* | Boogie: Basetypes port 3/3: Committing changed references | tabarbe | 2010-08-27 |
| | | | | Z3api.csproj shouldn't get in the way this time 'round. | ||
* | Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵ | tabarbe | 2010-08-27 |
| | | | | files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min. | ||
* | Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵ | tabarbe | 2010-08-26 |
| | | | | Core to jive with recent changes made to the cce class. | ||
* | Boogie: Committing changed references | tabarbe | 2010-08-20 |
| | |||
* | Added the port of Z3api. It is simply a port to the latest version of ↵ | qadeer | 2010-08-20 |
| | | | | Microsoft.Z3.dll and to C#. It does not work yet. | ||
* | Boogie: Committing changed references | tabarbe | 2010-08-13 |
| | |||
* | Also build Boogie and Dafny projects in 32-bit configurations. | rustanleino | 2010-07-30 |
| | | | | Don't insist on DafnyDriver picking up the LKG version (1.0.21125.0) of the Spec# runtime (in fact, most builders will probably have 1.0.21126.0). | ||
* | Boogie: VCGeneration port part 3/3: Updating sources to reference new ↵ | tabarbe | 2010-07-28 |
| | | | | project; making Core work with the port by removing the nonnull requirements on one abstract method. | ||
* | Boogie: Committing my port of simplify, along with the slightly changed ↵ | tabarbe | 2010-07-23 |
| | | | | references of simplify's dependents. | ||
* | Boogie: Committing my port of the SMTLib project | tabarbe | 2010-07-22 |
| | |||
* | Boogie: Committing ported version of Z3. | tabarbe | 2010-07-20 |
| | |||
* | Boogie: I have successfully ported the AbsInt project. It passes all ↵ | tabarbe | 2010-07-16 |
| | | | | | | regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL. Address any error complaints to t-abarbe@microsoft.com | ||
* | Boogie/Isabelle: Committing Isabelle port | tabarbe | 2010-07-14 |
| | |||
* | <Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the ↵ | tabarbe | 2010-07-14 |
| | | | | | | | changes made to the .csproj and Boogie.sln file that are necessary for the port. My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me. </BoogieDriver> </Boogie> | ||
* | Boogie: Added stratified inlining. It is enabled using the flag ↵ | akashlal | 2010-07-07 |
| | | | | /stratifiedInline:1. | ||
* | Added prover plugin for Isabelle/HOL. | sboehme | 2009-12-14 |
| | |||
* | Initial set of files. | mikebarnett | 2009-07-15 |