summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the ↵Gravatar MichalMoskal2010-08-06
| | | | -z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
* More line ending fixups.Gravatar MichalMoskal2010-08-06
|
* Fixup line-endings.Gravatar MichalMoskal2010-08-06
|
* Boogie: added /z3bv option that overrides the current setting of Z3 options ↵Gravatar stobies2010-08-06
| | | | for better performance on VCs that are heavy on bitvector arithmetic
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
| | | | svn-ignoring some build artifacts
* Boogie: cleanup option handling code for Z3Gravatar stobies2010-08-05
|
* Commiting Michal's fix for VCGravatar stobies2010-08-05
|
* Dafny: Made line endings consistentGravatar tabarbe2010-08-04
|
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Dafny: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Boogie: Code Contracts runtime checking was turned on in AbsInt. I turned ↵Gravatar tabarbe2010-08-04
| | | | it back off.
* Fixed some infelicities in the project files.Gravatar mikebarnett2010-08-04
|
* Dafny: Port commit part 1.5/2: Committing changed files outside of the Dafny ↵Gravatar tabarbe2010-08-04
| | | | | | dir. Do not attempt to regenerate the Parser and Scanner files before the port of Boogie/Core is done, as these have undergone changes, but will not be committed until after the Core port.
* Dafny: This file is required by DafnyPipeline.Gravatar tabarbe2010-08-03
|
* Dafny: Port commit part 1/2: Committing changed files.Gravatar tabarbe2010-08-03
| | | | Do not attempt to regenerate the Parser and Scanner files before the port of Boogie/Core is done, as these have undergone changes, but will not be committed until after the Core port.
* Dafny: Renaming the DafnyPipeline source files in preparation for the commit ↵Gravatar tabarbe2010-08-03
| | | | of my port of that project.
* Defunct project.Gravatar mikebarnett2010-08-03
|
* fixed path to the binaries directory; there was an extra .."Gravatar qadeer2010-08-03
|
* Boogie: The deletion of those files did not hold, lemme try again.Gravatar tabarbe2010-07-30
|
* Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an ↵Gravatar tabarbe2010-07-30
| | | | internal cce.cs class.
* Boogie: Removed cce.cs's from the provers, because they all reference ↵Gravatar tabarbe2010-07-30
| | | | projects which have a (more up-to-date) copy of cce.cs.
* 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).
* Sign both of the Dafny projects and have Dafny.exe get a version number as well.Gravatar mikebarnett2010-07-30
|
* Made consistent the way all of the C# projects sign themselves and include ↵Gravatar mikebarnett2010-07-30
| | | | the version information.
* Changed reference to AbsInt from a dll reference to a project reference.Gravatar mikebarnett2010-07-28
|
* Dafny: DafnyDriver port part 3/3: Updating sources to reference new project.Gravatar tabarbe2010-07-28
|
* Dafny: DafnyDriver port part 2/3: Adding new dependent file, removing ↵Gravatar tabarbe2010-07-28
| | | | unnecessary one.
* Dafny: DafnyDriver port part 1/3: Replacing old source files with ported versionGravatar tabarbe2010-07-28
|
* Dafny/DafnyDriver: Renaming source files in preparation for port commitGravatar tabarbe2010-07-28
|
* 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: VCGeneration port part 2/3: Adding new dependent files, removing ↵Gravatar tabarbe2010-07-28
| | | | unnecessary one.
* Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵Gravatar tabarbe2010-07-28
| | | | version
* Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵Gravatar tabarbe2010-07-28
| | | | ported C# version
* Fixed reference to VCGeneration project. Mistakenly checked in project files ↵Gravatar mikebarnett2010-07-28
| | | | were pointing to the yet-to-exist C# version.
* Boogie: Changed references from binary to project references.Gravatar tabarbe2010-07-27
|
* Boogie Provers: Changed the references from binary to project references.Gravatar tabarbe2010-07-27
|
* Also traverse bodies of function definitions when performing lambda expansion.Gravatar sboehme2010-07-23
|
* Boogie: AssemblyInfo.cs is no longer required for the build; cce.cs is.Gravatar tabarbe2010-07-23
|
* Boogie: Committing my port of simplify, along with the slightly changed ↵Gravatar tabarbe2010-07-23
| | | | references of simplify's dependents.
* Boogie: Renaming Simplify.sscproj and source files in preparation for ↵Gravatar tabarbe2010-07-23
| | | | committing my port of Simplify.csproj.
* Boogie: One last file to add for the port commit. Also, AssemblyInfo.ssc is ↵Gravatar tabarbe2010-07-22
| | | | no longer necessarry.
* Boogie: Committing my port of the SMTLib projectGravatar tabarbe2010-07-22
|
* Boogie: Renaming the source files for the SMTLib project in preparation for ↵Gravatar tabarbe2010-07-22
| | | | commiting my port of the project.
* Boogie: This file is no longer necessary, with how the csproj file is ↵Gravatar tabarbe2010-07-22
| | | | structured.
* Boogie: Repaired a reentrancy error in Z3/Simplify.Gravatar tabarbe2010-07-22
|
* Boogie: Looks like the default namespace should be Microsoft.Boogie.Z3, ↵Gravatar tabarbe2010-07-22
| | | | rather than Provers.Z3. I updated that.
* Boogie: Changed the assembly name for the Z3 project to Provers.Z3.dll, so ↵Gravatar tabarbe2010-07-22
| | | | that it matches the namespace.
* Boogie: Fixing incorrect referencing of Microsoft.Contracts (the Code ↵Gravatar tabarbe2010-07-21
| | | | Contracts dll) in AbsInt, Isabelle, and Z3
* Boogie: Forgot this file when I checked in the port of Z3. (cce = Code ↵Gravatar tabarbe2010-07-21
| | | | Contracts Extensions - utility methods for the port that are not present in Code Contracts.)
* Boogie: The reference to Z3 was dropped during the commit. Here it is back.Gravatar tabarbe2010-07-20
|
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-12 14:16:24 +0000