| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | various updates |  qadeer | 2013-12-09 |
| | | |||
| * | changed the output path for the QED build configuration to the Binaries folder | qadeer | 2013-12-08 |
| | | |||
| * | added the QED build configuration | qadeer | 2013-12-02 |
| | | |||
| * | 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 |
| | | |||
| * | Did some refactoring in the Boogie driver. | wuestholz | 2013-06-03 |
| | | |||
| * | Output to Boogie\Binaries even in the Release version |  Unknown | 2013-01-25 |
| | | |||
| * | 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 | ||
| * | cleaned up houdini options | qadeer | 2011-08-04 |
| | | |||
| * | Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to ↵ |  Unknown | 2011-07-05 |
| | | | | | the Z3 version to use | ||
| * | 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. | ||
| * | The TPTP backend works for some very limited examples | MichalMoskal | 2011-01-18 |
| | | |||
| * | Removed superfluous app.config | stobies | 2010-12-06 |
| | | |||
| * | 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#. | ||
| * | 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. | ||
| * | Get rid of some CCI dependencies in Driver | MichalMoskal | 2010-10-07 |
| | | |||
| * | Update to VS2010. | MichalMoskal | 2010-10-07 |
| | | |||
| * | Added a fix to extract loops code so that it returns a more comprehensive ↵ | qadeer | 2010-09-03 |
| | | | | | map of block names to original blocks. | ||
| * | fixed bug in extract loops by ensuring that loop extraction is done in ↵ | qadeer | 2010-09-01 |
| | | | | | nesting order | ||
| * | added a new api to Z3apiProcessTheoremProver for asserting axioms | qadeer | 2010-08-29 |
| | | |||
| * | 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: Accidentally created a service references folder in Boogie's folder ↵ | tabarbe | 2010-08-27 |
| | | | | | tree. Fixed that error. | ||
| * | 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: Changed a messed-up refference to Z3api back to its previous state. | tabarbe | 2010-08-27 |
| | | |||
| * | added some more apis to Z3api | qadeer | 2010-08-27 |
| | | | | | also added a reference from BoogieDriver to z3api | ||
| * | 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. | ||
| * | further fixes to Z3api project trying to make it work; still a long way off. | qadeer | 2010-08-23 |
| | | |||
| * | Boogie: Committing changed references | tabarbe | 2010-08-20 |
| | | |||
| * | Boogie: Committing changed references | tabarbe | 2010-08-13 |
| | | |||
| * | fixed path to the binaries directory; there was an extra .." | qadeer | 2010-08-03 |
| | | |||
| * | Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an ↵ | tabarbe | 2010-07-30 |
| | | | | | internal cce.cs class. | ||
| * | Made consistent the way all of the C# projects sign themselves and include ↵ | mikebarnett | 2010-07-30 |
| | | | | | the version information. | ||
| * | Changed reference to AbsInt from a dll reference to a project reference. | mikebarnett | 2010-07-28 |
| | | |||
| * | 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: Repaired a reentrancy error in Z3/Simplify. | tabarbe | 2010-07-22 |
| | | |||
| * | Boogie: The reference to Z3 was dropped during the commit. Here it is back. | tabarbe | 2010-07-20 |
| | | |||
| * | <Boogie> Removed references to AssemblyInfo.cs files - unnecessary for the ↵ | tabarbe | 2010-07-16 |
| | | | | | building/execution of the program | ||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |