summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Implemented the command line switch /useArrayTheory. This switch should be ↵Gravatar qadeer2010-01-21
| | | | used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
* Chalice: Implemented -vs switch, for use when running Chalice from inside ↵Gravatar rustanleino2010-01-15
| | | | Visual Studio
* Dafny:Gravatar rustanleino2010-01-14
| | | | | | | * Allow (and currently ignore) "ghost" modifier. * Fixed bug in boxing. * Check for div-by-zero error for modulo operator. * Improved emacs and latex modes.
* 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
| | | | fixed minor bug in Chalice grammar
* Doomed checking now uses the counterexample trace to minimize the number of ↵Gravatar schaef2009-12-18
| | | | theorem prover calls (See useCE in notdoomed.bpl).
* Allow ":" in addition to "returns" in function definitions. Make the ↵Gravatar MichalMoskal2009-12-17
| | | | | | | | pretty-printer use ":" not "returns". Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions. Consequently foo(int,y:bool) is no longer allowed. Update the testsuite to match that.
* Add makefile for running tests, allows "make -j4" to utilize multiple cores.Gravatar MichalMoskal2009-12-17
| | | | | Change the runtest.bat to report the testname in "succeeded/failed" message, so one can make sense of the multiple core output.
* Remove vcc1 testcase that never worked with Boogie2 and is testing obsolete ↵Gravatar MichalMoskal2009-12-17
| | | | bvInt handling in Boogie
* 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 _all_ the attributes of an assert this time add simpletypes to the visitor
* print attributes in AssertCmd.EmitGravatar mkawa2009-12-02
|
* Added code to (once again) print out prover warnings (under the ↵Gravatar rustanleino2009-11-26
| | | | /proverWarning switch).
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
| | | | | | | | | | | | | | | | | | | | * If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior * Made Dafny check loops for termination by default. Previously, this was done only if the loop had a decreases clause. To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *". * Allow "reads *" to say that the function may read anything at all (sound, but not very useful) * Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated * Added some previously omitted well-definedness checks. * Fixed some bugs in the resolver that caused some type errors not to be reported * Added some messages to go with some (previously rather opaquely reported) errors * Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted) * Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked. The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.
* Added resolution and translation of algebraic datatypes and (in function ↵Gravatar rustanleino2009-11-20
| | | | | | bodies) match expressions. Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
* 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 ↵Gravatar rustanleino2009-11-19
| | | | | | StandardVisitor while visiting commands). This solves Issue #6266.
* 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 ↵Gravatar schaef2009-11-18
| | | | statements and writes them the stdout. Line numbers are only displayed for bpl input.
* 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 ↵Gravatar mikebarnett2009-11-10
| | | | that it assumes the CCI sources are in a particular relative location to the BCT sources.)
* Changed error message to have correct program name.Gravatar mikebarnett2009-11-10
| | | | | Deleted custom host, just use the default host. Write output file to current directory, use "foo.bpl" as the output file name for the input assembly "foo".
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
| | | | Included VSI-Benchmarks in standard tests.
* 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 ↵Gravatar rustanleino2009-11-06
| | | | | | | | | | | | and seq. Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43). Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed. Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy. Added a space in the pretty printing of Boogie coercion expressions.
* Applied patch 4316, which fixes an unsoundness in the axiomatization of ↵Gravatar rustanleino2009-11-05
| | | | sequences (for both Dafny and Chalice). This in turn fixes issue 5876.
* The Dafny call statement now automatically declares left-hand sides as local ↵Gravatar rustanleino2009-11-05
| | | | variables, if they were not already local variables.
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to ↵Gravatar rustanleino2009-11-05
| | | | | | | "!(x in S)". Changed Dafny test files to use the new operator. Included the file b8.dfy into the VSI-Benchmarks test harness.
* Added loop invariants to make VSI-Benchmarks/b8.dfy verify. (Still to do: ↵Gravatar rustanleino2009-11-04
| | | | uncomment a couple of the desired loop invariants.)
* 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
| | | | | | added first test cases for doomed (including the ones from smoke) minor bug fixes minor speed-ups
* 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
| | | | | | caused malformed Boogie and malformed VCs. In particular, the problem arose in the CEV $file_name_is declarations. Such characters are now replaced by a percent sign followed by a four-digit hexadecimal number representing the Unicode value of the character. This fixes issue #6057.
* - 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 ↵Gravatar rustanleino2009-10-16
| | | | LHS's of CALL and RECEIVE statements (as was already done for FORK statements).
* Sieve of Eratosthenes, written in Chalice.Gravatar rustanleino2009-10-15
|
* Changed how Boogie looks for Z3: first look in the directory where Boogie ↵Gravatar rustanleino2009-10-14
| | | | | | is being executed from, then look in "c:\Program Files\Microsoft Research\Z3-2.x\bin" for x := 5,4,3,2,1,0. This fixes Issue Tracker item 5446.
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie ↵Gravatar rustanleino2009-10-14
| | | | | | filename starts with a digit, don't just prepend it to a QID, but prepend another character ('_') first. This fixes issue 5278 in the Issue Tracker.
* Fixed bugs in inlining, and added a test case.Gravatar rustanleino2009-10-14
| | | | This solves issue 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.
* In the TypeDeclCollector, call RegisterType for the bound variables in a ↵Gravatar stobies2009-10-12
| | | | quantifier. This makes sure that we get the proper DEFTYPEs for bit vector variables, even when they are not used in operator expressions. Fixes issue #5741.
* - fixed a positioning bug in Parser.scalaGravatar jansmans2009-10-07
| | | | - CopyLessMessagePassing-with-ack2.chalice verifies (i.e. separate channel for acknowledgements)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-08 23:45:01 +0000