summaryrefslogtreecommitdiff
path: root/Source/Boogie.sln
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
* Try to fix the "out-of-the-box" build of Boogie under Visual Studio. It turnsGravatar Dan Liew2015-01-29
| | | | | | | | | | | | out we had the repository set up in "MSBuild-Integrated package" mode[1] (missing packages won't fetched unless the user explicitly allows it for the solution) but what we want is "Automatic package restore" (provided NuGet is setup correctly automatically fetch the missing packages). I've followed the migration guide [2] and it appears that now Visual Studio will try to automatically fetch after making this change. [1] http://docs.nuget.org/consume/package-restore [2] http://docs.nuget.org/Consume/Package-Restore/Migrating-to-Automatic-Package-Restore
* Minor changes to the "Checked" build configurationGravatar wuestholz2015-01-09
|
* Updated to Staged HoudiniGravatar Ally Donaldson2015-01-08
|
* Introduce unit tests which use NUnit. NUnit is now a dependencyGravatar Dan Liew2014-11-17
| | | | | | | | | so developers need to install it via NuGet. There aren't many tests yet. Just a few for Core and Basetypes but hopefully more will be added in the future. More information can be found in Source/UnitTests/README.md
* MergeGravatar qadeer2014-07-15
|
* fixed some tests in ogGravatar qadeer2014-07-11
| | | | | added another test in linear (based on bug reported by Chris) removed the QED build configuration
* added the QED build configurationGravatar qadeer2013-12-02
|
* factored the concurrency checking code into a separate projectGravatar qadeer2013-11-22
|
* Split up the model viewer into a library and an application and added some ↵Gravatar wuestholz2013-07-14
| | | | functionality.
* Did some refactoring in the Boogie driver.Gravatar wuestholz2013-06-03
|
* Adding fixedpoint engine backendGravatar Ken McMillan2013-05-07
|
* bunch of refactoringsGravatar Unknown2012-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 ↵Gravatar boehmes2012-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 backendGravatar boehmes2012-09-27
|
* testing a fix in SIGravatar qadeer2012-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.Gravatar Ken McMillan2012-06-05
|\
| * Some changes to support expanded use of z3api.Gravatar Ken McMillan2012-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 tracesGravatar qadeer2012-02-25
|/ | | | removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
* moved GPUVerify into its own solutionGravatar qadeer2011-11-08
|
* Fixed test failures in the "Checked" configuration.Gravatar wuestholz2011-09-19
|
* Added GPUVerify projectGravatar Unknown2011-09-02
|
* ported Houdini to C#, added Houdini project to the Boogie solutionGravatar qadeer2011-08-03
|
* release build should not have z3api being builtGravatar Unknown2011-07-28
|
* Added a new solution configuration, Checked, that builds the Checked ↵Gravatar mikebarnett2011-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".Gravatar MichalMoskal2011-01-18
|
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-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.Gravatar MichalMoskal2010-10-12
|
* Starting work on Boogie Model Viewer.Gravatar MichalMoskal2010-10-12
|
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* created a new build target called z3apidebug.Gravatar qadeer2010-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 ↵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: Added Z3api to the build configuration.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: 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: 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: Committing changed referencesGravatar tabarbe2010-08-20
|
* Added the port of Z3api. It is simply a port to the latest version of ↵Gravatar qadeer2010-08-20
| | | | Microsoft.Z3.dll and to C#. It does not work yet.
* Boogie: Committing changed referencesGravatar tabarbe2010-08-13
|
* Also build Boogie and Dafny projects in 32-bit configurations.Gravatar rustanleino2010-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 ↵Gravatar tabarbe2010-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 ↵Gravatar tabarbe2010-07-23
| | | | references of simplify's dependents.
* Boogie: Committing my port of the SMTLib projectGravatar tabarbe2010-07-22
|
* Boogie: Committing ported version of Z3.Gravatar tabarbe2010-07-20
|
* Boogie: I have successfully ported the AbsInt project. It passes all ↵Gravatar tabarbe2010-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 portGravatar tabarbe2010-07-14
|
* <Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the ↵Gravatar tabarbe2010-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 ↵Gravatar akashlal2010-07-07
| | | | /stratifiedInline:1.
* Added prover plugin for Isabelle/HOL.Gravatar sboehme2009-12-14
|
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 07:47:40 +0000