summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* Add tests for -z3multipleErrors from Shuvendu.Gravatar MichalMoskal2011-02-23
|
* Add workaround for cmd raceGravatar MichalMoskal2011-02-23
|
* Dafny: Improved scheme for splitting expressions. Also, report each split ↵Gravatar rustanleino2011-02-19
| | | | in error messages.
* Don't run test21 with the untyped Z3, as this is no longer going to be availableGravatar MichalMoskal2011-02-18
|
* Run dafny and boogie tests by defaultGravatar MichalMoskal2011-02-18
|
* Don't stop when some test failsGravatar MichalMoskal2011-02-18
|
* Allow for running Boogie and Dafny testcases separatelyGravatar MichalMoskal2011-02-18
|
* Remove a testcase for bvInt (feature to be killed soon)Gravatar MichalMoskal2011-02-18
|
* Allow for passing flags to test runsGravatar MichalMoskal2011-02-18
|
* Dafny:Gravatar rustanleino2011-02-17
| | | | | | | | | | | | | | | | | | * Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case). * Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.) * Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type. * More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal") * Add axioms about idempotence of set union and intersection * The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one * In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase * Fixed error in translation of while(*)
* Dafny: added test harness to Test/dafny1/ExtensibleArray.dfyGravatar rustanleino2011-02-16
|
* Dafny: added ExtensibleArray program as a testGravatar rustanleino2011-02-16
|
* Dafny: added alternate version of PriorityQueueGravatar rustanleino2011-02-15
|
* Fix a bug in cloning of nested lambda expressions in AI engineGravatar MichalMoskal2011-02-11
|
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
|
* Dafny: Answer file to go with previously updated test fileGravatar rustanleino2011-02-04
|
* Dafny: every decreases clause implicitly ends with a never-ending sequence ↵Gravatar rustanleino2011-02-03
| | | | of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).
* Dafny: allow self-calls in function postconditions--these simply refer to ↵Gravatar rustanleino2011-02-03
| | | | the result value of the current call
* Dafny: implemented a more precise scheme for allowing use of a function's ↵Gravatar rustanleino2011-02-03
| | | | rep axiom
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
|
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
|
* Add description of {:selective_checking} to the /attrHelp. Fix the testcase.Gravatar MichalMoskal2011-01-13
|
* Dafny: Fixed error in printing an error message. Changed "function method" ↵Gravatar rustanleino2011-01-11
| | | | to "function" in a test case.
* Add new feature: {:selective_checking} on procedures. See testcase for a ↵Gravatar MichalMoskal2010-12-17
| | | | description (it was implemented in VCC before and is quite useful).
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 19:53:38 +0000