summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Boogie: Peephole optimization to reduce depth of formulas created during VC ↵Gravatar rustanleino2010-02-15
| | | | generation. This reduces the chances of Boogie causing a stack overflow.
* eliminated the line printing version number in the golden outputGravatar qadeer2010-02-13
|
* Dafny:Gravatar rustanleino2010-02-13
| | | | | | * Allow ghost methods (all "ghost" keywords are currently parsed and then ignored) * Improved and made more automatic the treatment of "use" functions (a good next step would be to automatically infer which functions would make good "use" functions) * Include preconditions in all definedness checks of function-call expressions
* (no commit message)Gravatar qadeer2010-02-12
|
* 1. Fixed bug in StandardVisitor.sscGravatar qadeer2010-02-09
| | | | | | 2. Hoisted the call to inlining into BoogieDriver.ssc 3. Implemented a simple dead variable elimination 4. Perform inlining only for those procedures whose verification is not skipped
* Boogie: /useArrayTheory currently implies /monomorphizeGravatar rustanleino2010-02-09
|
* Fix a bug in checking for {:inline} procedure attribute. Resolves #6993.Gravatar MichalMoskal2010-02-08
|
* Use reflection to read version string from assembly when displaying logo ↵Gravatar stobies2010-02-08
| | | | information
* Removed Unicode chars from Assembly attributes - they are not liked too much ↵Gravatar stobies2010-02-08
| | | | by explorer
* Preparing Isabelle plugin sources for VCC release.Gravatar stobies2010-02-08
|
* Dafny: Added if-then-else expressions (replacing and extending the previous ↵Gravatar rustanleino2010-02-04
| | | | | | | | boolean-only if-then-else expressions) Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter) Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::' Dafny: Check for division-by-zero for both '/' and '%'
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
|
* Dafny: Added support for big integers.Gravatar rustanleino2010-01-28
|
* bugfixGravatar schaef2010-01-28
|
* Added experimental feature /DoomDebug. Can be test using ↵Gravatar schaef2010-01-28
| | | | Test/doomed/doomdebug.bpl
* Fixed bug in DEFTYPE declarations for maps. Made sure that argument and ↵Gravatar qadeer2010-01-28
| | | | result types of maps are declared before the type of the map itself.
* 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.)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-13 06:57:13 +0000