summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Implemented the command line switch /useArrayTheory. This switch should be u...Gravatar qadeer2010-01-21
* Chalice: Implemented -vs switch, for use when running Chalice from inside Vi...Gravatar rustanleino2010-01-15
* Dafny:Gravatar rustanleino2010-01-14
* Dafny: updated to reflect Boogie's new parsing of function argumentsGravatar rustanleino2010-01-07
* Chalice: updated Prelude to match new Boogie parsing of function parameters; ...Gravatar rustanleino2010-01-06
* Doomed checking now uses the counterexample trace to minimize the number of t...Gravatar schaef2009-12-18
* Allow ":" in addition to "returns" in function definitions. Make the pretty-p...Gravatar MichalMoskal2009-12-17
* Add makefile for running tests, allows "make -j4" to utilize multiple cores.Gravatar MichalMoskal2009-12-17
* Remove vcc1 testcase that never worked with Boogie2 and is testing obsolete b...Gravatar MichalMoskal2009-12-17
* Added prover plugin for Isabelle/HOL.Gravatar sboehme2009-12-14
* Revert the matching depth limit change from previous checkin: would break VCC.Gravatar MichalMoskal2009-12-10
* Z3 parameters to help it bail out of fruitless searches fasterGravatar mkawa2009-12-05
* print attributes in AssertCmd.EmitGravatar mkawa2009-12-02
* Added code to (once again) print out prover warnings (under the /proverWarnin...Gravatar rustanleino2009-11-26
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
* Added resolution and translation of algebraic datatypes and (in function bodi...Gravatar rustanleino2009-11-20
* Setting up test cases for BCTGravatar schaef2009-11-20
* (no commit message)Gravatar schaef2009-11-20
* Support {:PossiblyUnreachable} attribute on assertsGravatar MichalMoskal2009-11-20
* Fixed bug in inlining (procedure *definitions* had been traversed by Standard...Gravatar rustanleino2009-11-19
* doomed stuff: minor bug fixes / improved output / more test casesGravatar schaef2009-11-19
* modified the doom checking. It is now able to report only the relevant statem...Gravatar schaef2009-11-18
* Update use of CCI's API for decompiling the IL model to the Code Model.Gravatar mikebarnett2009-11-17
* Swapped previous file (Datatypes.bpl) for the correct test file (Datatypes.dfy).Gravatar rustanleino2009-11-14
* Changed solution to include the CCI projects from Codeplex. (Still flaky in t...Gravatar mikebarnett2009-11-10
* Changed error message to have correct program name.Gravatar mikebarnett2009-11-10
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
* Fixes crash when modifies set includes a variable twice.Gravatar mkawa2009-11-07
* Added a sequence update expression in Dafny.Gravatar rustanleino2009-11-06
* Redesigned the encoding of Dafny generics, including the built-in types set a...Gravatar rustanleino2009-11-06
* Applied patch 4316, which fixes an unsoundness in the axiomatization of seque...Gravatar rustanleino2009-11-05
* The Dafny call statement now automatically declares left-hand sides as local ...Gravatar rustanleino2009-11-05
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "...Gravatar rustanleino2009-11-05
* Added loop invariants to make VSI-Benchmarks/b8.dfy verify. (Still to do: un...Gravatar rustanleino2009-11-04
* Look for Boogie.exe also in Program Files (x86)Gravatar MichalMoskal2009-11-03
* vc:doomed does not use the console anymore to report resultsGravatar schaef2009-11-02
* Fixed PreLoopHeap counting bug.Gravatar rustanleino2009-10-31
* Initial version of VSI Benchmarks 1 - 8Gravatar RMonahan2009-10-30
* Use the new F# names for bigint typeGravatar MichalMoskal2009-10-30
* Update F# binaries to Oct09 CTPGravatar MichalMoskal2009-10-30
* Fixed problem where Dafny filenames with unusual characters in filenames had ...Gravatar rustanleino2009-10-29
* - Sieve.chalice verifies + executes fasterGravatar jansmans2009-10-20
* - the "-gen" option works only if the program verifiesGravatar jansmans2009-10-16
* Implicitly declare as local variables undeclared variables occurring as LHS's...Gravatar rustanleino2009-10-16
* Sieve of Eratosthenes, written in Chalice.Gravatar rustanleino2009-10-15
* Changed how Boogie looks for Z3: first look in the directory where Boogie is...Gravatar rustanleino2009-10-14
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie filenam...Gravatar rustanleino2009-10-14
* Fixed bugs in inlining, and added a test case.Gravatar rustanleino2009-10-14
* In the TypeDeclCollector, call RegisterType for the bound variables in a quan...Gravatar stobies2009-10-12
* - fixed a positioning bug in Parser.scalaGravatar jansmans2009-10-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-22 21:28:43 +0000