summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵Gravatar akashlal2010-09-05
| | | | that it has reached the recursion bound.
* Delete unreachable Blocks of an Impl before calling ExtractLoops().Gravatar akashlal2010-09-05
| | | | This helps avoid a crash inside NewComputeDominators().
* Fixed a performance issue with StratifiedInliningGravatar akashlal2010-09-05
|
* Added tests for extractloopsGravatar akashlal2010-09-04
|
* Fix for extractLoopsGravatar akashlal2010-09-04
|
* Henrique's addition to the the ErrorHandler API to retrieve modelsGravatar qadeer2010-09-03
|
* Chalice: incorporate another regression testGravatar kyessenov2010-09-03
|
* more fixes to ExtractLoopsGravatar qadeer2010-09-03
|
* 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.
* Changed the interface of Parse so that it can consume a program from a StreamGravatar akashlal2010-09-03
|
* bunch of fixes related to Boogie error model generation from the Z3 error ↵Gravatar qadeer2010-09-03
| | | | model generation
* Vim: add keywords to ChaliceGravatar kyessenov2010-09-02
|
* VS 2010: add "spec" as keyword in ChaliceGravatar kyessenov2010-09-02
|
* Chalice: added Duplicates refinement from Verification Corner videoGravatar kyessenov2010-09-02
|
* Chalice: fix in refinement loop target resolution; added "spec" as a keyword ↵Gravatar kyessenov2010-09-02
| | | | synonym to "var"
* Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ↵Gravatar akashlal2010-09-02
| | | | instead of uninterpreted predicates.
* fixed bug in extract loops by ensuring that loop extraction is done in ↵Gravatar qadeer2010-09-01
| | | | nesting order
* Minor fix to my previous commitGravatar akashlal2010-09-01
|
* Added a way of recovering counterexample paths after loop extraction. ↵Gravatar akashlal2010-09-01
| | | | Stable, but still buggy.
* Version-stamp CCE assemblyGravatar stobies2010-09-01
|
* Boogie build succeededGravatar codeplexbot2010-09-01
|
* Added a new class LoopProcedure to represent the procedures representing ↵Gravatar qadeer2010-09-01
| | | | extracted loops.
* Dafny: Added Dafny solutions to the VSComp 2010 problemsGravatar rustanleino2010-09-01
|
* VS2010 mode for Dafny and Boogie: updated, for example to properly deal ↵Gravatar rustanleino2010-09-01
| | | | with string literals
* Boogie build succeededGravatar codeplexbot2010-08-31
|
* Dafny: added a command-line option to change the prelude fileGravatar sboehme2010-08-30
|
* 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.
* BeginCheck now adds context.Axioms as well as the conjecture to the context.Gravatar qadeer2010-08-29
| | | | Also started using the new quantifier api.
* Added a constructor to a contract class otherwise the compiler complained ↵Gravatar mikebarnett2010-08-28
| | | | about the default nullary one calling its base class nullary ctor, and there wasn't one.
* Boogie: Accidentally created a service references folder in Boogie's folder ↵Gravatar tabarbe2010-08-27
| | | | tree. Fixed that error.
* Boogie: Simplify: Added a contracts class that I forgot in the initial porting.Gravatar tabarbe2010-08-27
|
* Dafny: fallback to ShallowType (elements of IndexField arrays seem to have ↵Gravatar sboehme2010-08-27
| | | | Type null)
* Boogie: Commented out all occurences of repeated inherited contracts - makes ↵Gravatar tabarbe2010-08-27
| | | | fewer error messages when compiling with runtime checking on.
* 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).
* Dafny: added inlined functions making reads and updates of the heap explicitGravatar sboehme2010-08-27
|
* Boogie: Removed an incorrect Ensures clause on a void method.Gravatar tabarbe2010-08-27
|
* fixed bug with function name look upGravatar qadeer2010-08-27
|
* 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: Adding an autobuild and regression cmd file for Boogie and Dafny - ↵Gravatar tabarbe2010-08-27
| | | | Cleans and builds both projects, then executes the regressions if the build succeeded. If the build had failed, it will stop the script.
* Boogie: Added Z3api to the build configuration.Gravatar tabarbe2010-08-27
|
* Boogie: Changed a messed-up refference to Z3api back to its previous state.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: Basetypes port 2/3: Committing new source file, deleting old oneGravatar tabarbe2010-08-27
|
* Boogie: Basetypes port 1/3: Committing new sourcesGravatar tabarbe2010-08-27
|
* Boogie: Renaming the Basetypes sources in preparation for my port commit.Gravatar tabarbe2010-08-27
|
* Bug fixes and logging for z3apiGravatar akashlal2010-08-27
|
* Addint ignore file for GITGravatar stobies2010-08-27
|
* added some more apis to Z3apiGravatar qadeer2010-08-27
| | | | also added a reference from BoogieDriver to z3api
* Added a (temporary) CCE file so that Z3Api can build.Gravatar mikebarnett2010-08-27
|
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-18 05:31:39 +0000