Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | |||
* | adding references to the floating point type wherever references to the real ↵ | Dietrich | 2015-04-17 |
| | | | | type exist. This remains a work in progress | ||
* | Add alpha equivalence check for Expr, and use it when lambda lifting | Dan Rosén | 2014-08-01 |
| | |||
* | Fix Boogie so it compiled with mono. Patch by Dan Liew. | Ally Donaldson | 2014-01-14 |
| | |||
* | removed bitvector analysis from Boogie | qadeer | 2013-12-08 |
| | | | | an advanced version has been moved to Corral | ||
* | added the QED build configuration | qadeer | 2013-12-02 |
| | |||
* | factored the concurrency checking code into a separate project | qadeer | 2013-11-22 |
| | |||
* | a minor refactoring + implemented mover checking | qadeer | 2013-10-25 |
| | |||
* | Removed the remaining pure collections. | wuestholz | 2013-07-23 |
| | |||
* | CVC4 Parser | pantazis | 2013-06-12 |
| | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | |||
* | Improvements to Staged Houdini | allydonaldson | 2013-05-29 |
| | |||
* | Staged Houdini | allydonaldson | 2013-04-30 |
| | |||
* | first check in of Owicki-Gries and linear sets | Unknown | 2013-01-24 |
| | |||
* | 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. | ||
* | Dafny and Boogie: get rid of 'static' fields in parser | Rustan Leino | 2012-08-21 |
| | |||
* | various changes to boogie for bitvector analysis and bctprovider | qadeer | 2011-08-08 |
| | |||
* | Re-enabled quantifier checking in the Checked configuration. | mikebarnett | 2011-03-16 |
| | |||
* | Turn off quantifier checking in the runtime checking. | mikebarnett | 2011-03-14 |
| | |||
* | 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. | ||
* | Added version.cs as link to those projects that were missing it | stobies | 2010-12-06 |
| | | | | Select 4.0 client profile on all projects | ||
* | 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#. | ||
* | Get rid of F# dependencies - use System.Numerics and a custom Rational ↵ | MichalMoskal | 2010-12-02 |
| | | | | structure instead | ||
* | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | qadeer | 2010-12-01 |
| | |||
* | Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵ | qadeer | 2010-11-27 |
| | | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0. | ||
* | 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: Removed some errors with code contracts (commenting out ↵ | tabarbe | 2010-08-27 |
| | | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however). | ||
* | 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: 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. | ||
* | Fixed external references to other projects in the solution. | mikebarnett | 2010-08-23 |
| | | | | Added version.cs to the project. | ||
* | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |