summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵Gravatar MichalMoskal2010-08-18
| | | | use separate Z3 type per Boogie type
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
|
* Boogie: Removed mistaken duplication of a type parameterGravatar tabarbe2010-08-16
|
* Stratified inlining: Changed recursion into a loop.Gravatar akashlal2010-08-16
|
* Bug fix for stratified inlining trace generationGravatar akashlal2010-08-16
|
* Added more options for stratified inliningGravatar akashlal2010-08-16
|
* Boogie: Committing changed referencesGravatar tabarbe2010-08-13
|
* Boogie: Adding 1 more necessary source file for VCExpr, removing an ↵Gravatar tabarbe2010-08-13
| | | | unnecessary one
* Boogie: Committing new source code for VCExprGravatar tabarbe2010-08-13
|
* Boogie: Renaming VCExpr sources in preparation for port commitGravatar tabarbe2010-08-13
|
* Added methods to read a file from any Stream objectGravatar akashlal2010-08-12
|
* Added the option /extractLoops to extract loops as procedure calls. If ↵Gravatar qadeer2010-08-11
| | | | either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
* Fixed a contractGravatar akashlal2010-08-10
|
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Boogie: Sorry about that - no need for the conditional compilationGravatar tabarbe2010-08-09
|
* Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.csGravatar tabarbe2010-08-09
|
* Boogie: Fixed a few line endingsGravatar tabarbe2010-08-06
|
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 06:29:28 +0000