summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* Dafny: Added Test/dafny1/PriorityQueue.dfyGravatar rustanleino2010-12-10
|
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* Dafny: Improved default decreases clauses for methods and functionsGravatar rustanleino2010-11-25
| | | | | Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode
* Dafny: Updated VSComp2010/Answer to correspond to recently updated test fileGravatar rustanleino2010-11-21
|
* Chalice: white space delta in test fileGravatar rustanleino2010-11-17
| | | | Dafny: Simplified VSComp2010/Problem4-Queens.dfy from using an inductive ghost-method lemmas to just using an assert
* Forro: revised syntax (this version used in Boogie tutorial at SBMF 2010)Gravatar rustanleino2010-11-17
|
* Introducing Forr?! Forr? is a tiny language that translates to Boogie. The ↵Gravatar rustanleino2010-11-06
| | | | purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie.
* ModelViewer:Gravatar rustanleino2010-11-02
| | | | | | | * map back values introduced by bool_2_U and int_2_U * map back internal names for select/store to [n] and [n:=], where n is the arity of the map * added /break switch to ModelViewer * display more things (including sequences) in Dafny provider
* Updated Answer file to go with the previous check-in.Gravatar rustanleino2010-11-02
|
* Test/dafny1/KatzManna.dfy: Changed mocked up matrix class to use Dafny's ↵Gravatar rustanleino2010-10-27
| | | | built-in array2 class.
* Updated parser.cs files to pick up the new .frame improvements from ↵Gravatar rustanleino2010-10-26
| | | | boogiepartners
* Boogie:Gravatar rustanleino2010-10-26
| | | | | | | | | * Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners. * It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs. Dafny: * Ditto for its Parser.cs/Scanner.cs. * Added ability to provide a custom Errors handler for scanner/parser. * Added Test/dafny1/Cubes.dfy
* Miscellaneous changes:Gravatar rustanleino2010-10-22
| | | | | | | * Also copy CodeContractExtender in PrepareBoogieZip.bat * Added some comments and a new program in Test/textbook * Included refinement keywords in Chalice emacs mode * Used assignment instead of spec statement in DuplicatesVideo.chalice
* Skip unchagned variables in model dumps. Fix testcaseGravatar MichalMoskal2010-10-14
|
* Bug fixes and speed up for doomed program point analysisGravatar schaef2010-10-13
|
* Add missing Clone() when storing incarnation maps; update testcase to make ↵Gravatar MichalMoskal2010-10-12
| | | | | | this clear Construct states in Model properly, nuke direct printing.
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* Boogie:Gravatar rustanleino2010-09-24
| | | | | * Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time.
* 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
* Dafny: Compilation of multi-dimensional arraysGravatar rustanleino2010-09-21
|
* Added test for loop extractionGravatar akashlal2010-09-18
|
* Dafny:Gravatar rustanleino2010-09-17
| | | | | | * Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields
* 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
* added an optimization to extract loops so that only loop targets are treated ↵Gravatar qadeer2010-09-10
| | | | as output variables of the extracted procedure.
* Added tests for extractloopsGravatar akashlal2010-09-04
|
* Dafny: Added Dafny solutions to the VSComp 2010 problemsGravatar rustanleino2010-09-01
|
* Change Synonym type printing to what it was, use a workaround in ↵Gravatar MichalMoskal2010-08-18
| | | | TypeToString() instead. Add test for /typeEncoding:m.
* Boogie: Fixed test 'bitvectors'.Gravatar wuestholz2010-08-14
|
* Updated answer to this regression to reflect the fact that it is now verified.Gravatar tabarbe2010-08-12
|
* Boogie: This reg test was not running verification.Gravatar tabarbe2010-08-12
|
* 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.
* Fix the test to use new name for /z3bv option.Gravatar MichalMoskal2010-08-10
|
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Boogie: That file should not have been in the depot, but rather be created ↵Gravatar tabarbe2010-08-09
| | | | locally
* Boogie: added /z3bv option that overrides the current setting of Z3 options ↵Gravatar stobies2010-08-06
| | | | for better performance on VCs that are heavy on bitvector arithmetic
* Boogie: Added a new simple regression test, "sanity", which runs a single ↵Gravatar tabarbe2010-07-29
| | | | test for Boogie and a single test for Dafny, just to check for grievous runtime errors in the code. (In my porting, I work with code that, in some cases, is not tested until the 3rd or 4th regression test. These 2 test files should make use of that more obscure code and alert me to my errors quickly, rather than making me wait through a full regression cycle.)
* Dafny: better error reporting on resolution of refinements. Replace ↵Gravatar kyessenov2010-07-14
| | | | assertions with "if"s to handle errors gently and add cycle detection check.
* Dafny: Axiom about inverting a set union operation, similar to the recent ↵Gravatar rustanleino2010-07-09
| | | | ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
* Boogie: Added stratified inlining. It is enabled using the flag ↵Gravatar akashlal2010-07-07
| | | | /stratifiedInline:1.
* Dafny:Gravatar rustanleino2010-07-06
| | | | | * changed rule about scoping of out-parameters * added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
* Added a comment noting that this test fails with Z3 2.4.Gravatar mschwerhoff2010-07-06
|
* Dafny: added assertions in the refinement obligation necessitating that the ↵Gravatar kyessenov2010-07-03
| | | | return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
* Dafny: Support class type parameters in refinements. Added another ↵Gravatar kyessenov2010-07-02
| | | | regression test -- a sequence refined by a singly linked list.
* Dafny: added Carrol Morgan's calculator regression test.Gravatar kyessenov2010-07-02
|
* Dafny: support input/output parameters in refined methods.Gravatar kyessenov2010-07-02
|
* Dafny: added a regression test for the refinement extension.Gravatar kyessenov2010-07-02
|
* Dafny:Gravatar rustanleino2010-06-24
| | | | | * For every loop decreases clause N, generate a free loop invariant N <= N0, where N0 is the value of N just before the loop. * Added Test/dafny1/KatzManna.dfy, which contains the 3 programs (and their termination annotations) from the Katz and Manna 1975 paper "A closer look at termination" (which benefits from the feature above).
* Updated the frame files to work with the latest Coco/R. This entails *not* ↵Gravatar mikebarnett2010-06-22
| | | | | | having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files.
* Boogie:Gravatar rustanleino2010-06-22
| | | | | | | | | * Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below). Dafny: * Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are * Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results. * Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
* Dafny:Gravatar rustanleino2010-06-19
| | | | | | * Improved design and implementation of SplitExpr * Fixed some tests in dafny0/Use.dfy * Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-12 06:50:21 +0000