summaryrefslogtreecommitdiff
path: root/Test/test2
Commit message (Collapse)AuthorAge
* Added a test and a todo.Gravatar wuestholz2015-01-02
|
* Add alpha equivalence check for Expr, and use it when lambda liftingGravatar Dan Rosén2014-08-01
|
* Removed old test infrastructure files except forGravatar Dan Liew2014-05-28
| | | | | | | | | ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
* Fix lit test suite when running Boogie under a path that containsGravatar Dan Liew2014-05-27
| | | | spaces.
* Remove old python testing scriptsGravatar Dan Liew2014-05-11
|
* Unbreak the tests in test2 for batch file testing infrastructureGravatar Dan Liew2014-05-10
|
* Enabled VC Generation lit tests.Gravatar Dan Liew2014-05-07
|
* Add support for assumption variables.Gravatar wuestholz2014-04-21
|
* Changed all lambda-expression rewriting to be done as a pre-processing step ↵Gravatar Rustan Leino2014-02-28
| | | | | | before real verification. Fixed treatment of lambda-expression attributes.
* Fixed bug in handling of break statementsGravatar Rustan Leino2014-02-10
|
* Fixed another :never_pattern bug related to nested quantifiersGravatar Rustan Leino2013-12-16
|
* Fixed bug in never_pattern functionality. In the new design, never_pattern ↵Gravatar Rustan Leino2013-12-16
| | | | does not assemble any nopats from nested quantifiers/lambdas.
* Patch by Nathan Chong: iterative version of remove empty blocks algorithm. ↵Gravatar Ally Donaldson2013-12-02
| | | | This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems.
* do monomorphic checkingGravatar qadeer2013-11-22
|
* MergeGravatar Pantazis Deligiannis2013-07-15
|\
* | Added an attribute to set the time limit for implementations.Gravatar wuestholz2013-07-12
| |
| * added python scripts (work in unix and windows) for testing Z3 and CVC4 to ↵Gravatar Pantazis Deligiannis2013-07-07
|/ | | | many of the test suite dirs
* Changed the prover interface to report traces for time outs and out of memory.Gravatar wuestholz2013-05-30
|
* Fixed bug in the cutting of back edges (that manifested itself whenever the ↵Gravatar Rustan Leino2013-05-29
| | | | first block in a procedure was the target of a back edge)
* removed call forall and * args to callsGravatar Unknown2013-02-23
|
* Boogie: added type 'real' with overloaded arithmetic operations plus real ↵Gravatar boehmes2012-09-27
| | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
* Boogie: new syntax for integer division and modulus: use div and mod instead ↵Gravatar boehmes2012-09-27
| | | | of / and %
* Updated the 'Answer' file for test2.Gravatar wuestholz2011-12-02
|
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ↵Gravatar wuestholz2011-12-02
| | | | | | not replaced after lambda expansion. (reported by Florian Egli)
* Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵Gravatar Rustan Leino2011-10-27
| | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
* Added "free call" statements that don't check the precondition in the caller.Gravatar wuestholz2011-09-14
|
* Fix a bug in cloning of nested lambda expressions in AI engineGravatar MichalMoskal2011-02-11
|
* Add description of {:selective_checking} to the /attrHelp. Fix the testcase.Gravatar MichalMoskal2011-01-13
|
* 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).
* 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
* 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
* Change Synonym type printing to what it was, use a workaround in ↵Gravatar MichalMoskal2010-08-18
| | | | TypeToString() instead. Add test for /typeEncoding:m.
* Boogie:Gravatar rustanleino2010-05-15
| | | | | | | | | | * Added support for polymorphism in lambda expressions * Little clean-up here and there * Added 'then' keyword to emacs and latex modes Dafny: * Added support for fine-grained framing, using the back-tick syntax from Region Logic * Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
* Dafny: Added definedness checks for all statements (previously, some were ↵Gravatar rustanleino2010-03-13
| | | | | | missing) Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
* Boogie:Gravatar rustanleino2010-02-20
| | | | | | | | | | | * Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case) * Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads. * Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized * Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1 Boogie refactoring: * Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand * Cleaned up some parsing of command-line options
* Fix up the polymorphic case for lambda; it probably still isn't quite correct.Gravatar MichalMoskal2010-02-19
|
* Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda ↵Gravatar MichalMoskal2010-02-19
| | | | expressions; they might not yet fully work for polymorphic maps.
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
|
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
| | | | Controlled by the option /coalesceBlocks (default is to perform the optimization).
* Updated Answer files, in synch with my recent edits 31961.Gravatar rustanleino2009-08-16
|
* Removed Output files. These are created on a local machine when the tests ↵Gravatar rustanleino2009-08-07
| | | | are run.
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 23:43:04 +0000