summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
Commit message (Collapse)AuthorAge
* Boogie: added features to help with modular verification. In particular, ↵Gravatar Rustan Leino2011-05-13
| | | | define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
|
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
|
* 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.
* Stratified inlining: Added concrete values to error traces. Added an extra ↵Gravatar akashlal2011-02-17
| | | | flag "inferLeastForUnsat".
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
|
* The TPTP backend works for some very limited examplesGravatar MichalMoskal2011-01-18
|
* Add functions generated in lambda-expansion of function body to top-level ↵Gravatar MichalMoskal2010-12-17
| | | | program declarations.
* Removed superfluous app.configGravatar stobies2010-12-06
|
* 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#.
* two automatically generated app.config that I didn't add earlier.Gravatar qadeer2010-11-27
|
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
|
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
|
* Get rid of some CCI dependencies in DriverGravatar MichalMoskal2010-10-07
|
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* Boogie:Gravatar rustanleino2010-09-23
| | | | | | * Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
* Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.Gravatar akashlal2010-09-18
|
* Dafny:Gravatar rustanleino2010-09-14
| | | | | | | | * Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations
* Fix for extractLoopsGravatar akashlal2010-09-04
|
* Added a fix to extract loops code so that it returns a more comprehensive ↵Gravatar qadeer2010-09-03
| | | | map of block names to original blocks.
* fixed bug in extract loops by ensuring that loop extraction is done in ↵Gravatar qadeer2010-09-01
| | | | nesting order
* Added a way of recovering counterexample paths after loop extraction. ↵Gravatar akashlal2010-09-01
| | | | Stable, but still buggy.
* added a new api to Z3apiProcessTheoremProver for asserting axiomsGravatar qadeer2010-08-29
|
* 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: Accidentally created a service references folder in Boogie's folder ↵Gravatar tabarbe2010-08-27
| | | | tree. Fixed that error.
* Boogie: Removed some errors with code contracts (commenting out ↵Gravatar tabarbe2010-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 ↵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: Changed a messed-up refference to Z3api back to its previous state.Gravatar tabarbe2010-08-27
|
* added some more apis to Z3apiGravatar qadeer2010-08-27
| | | | also added a reference from BoogieDriver to z3api
* 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.
* further fixes to Z3api project trying to make it work; still a long way off.Gravatar qadeer2010-08-23
|
* Boogie: Committing changed referencesGravatar tabarbe2010-08-20
|
* Boogie: Removed a completed task commentGravatar tabarbe2010-08-19
|
* Boogie: Committing changed referencesGravatar tabarbe2010-08-13
|
* 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.
* 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
|
* fixed path to the binaries directory; there was an extra .."Gravatar qadeer2010-08-03
|
* Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an ↵Gravatar tabarbe2010-07-30
| | | | internal cce.cs class.
* 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
|
* 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: Repaired a reentrancy error in Z3/Simplify.Gravatar tabarbe2010-07-22
|
* Boogie: The reference to Z3 was dropped during the commit. Here it is back.Gravatar tabarbe2010-07-20
|
* Boogie: Forgot to check in this file. Hope no one tried to rebuild without ↵Gravatar tabarbe2010-07-19
| | | | it. Sorry.
* <Boogie> Removed references to AssemblyInfo.cs files - unnecessary for the ↵Gravatar tabarbe2010-07-16
| | | | building/execution of the program
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 04:46:24 +0000