summaryrefslogtreecommitdiff
path: root/Test/test21
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
* 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.
* Set the following tests to expected failure under lit. Having theseGravatar Dan Liew2014-05-19
| | | | | | | | | | | | | | | reported is unnecessary noise right now. Someone needs to fix these tests but I'm not the author. Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl Boogie :: test21/Maps2.bpl Boogie :: test21/test3_AddMethod_conv.bpl
* Remove old python testing scriptsGravatar Dan Liew2014-05-11
|
* Enabled "Verify Boogie 2" lit tests. Note the following tests failGravatar Dan Liew2014-05-07
| | | | | | | | because they were never properly tested in the the old testing infrastructure. test21/Maps2.bpl test21/test3_AddMethod_conv.bpl
* Fixed bug in printing real literalsGravatar Rustan Leino2014-02-10
|
* do monomorphic checkingGravatar qadeer2013-11-22
|
* 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
* 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)
* Don't run test21 with the untyped Z3, as this is no longer going to be availableGravatar MichalMoskal2011-02-18
|
* 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.
* 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-12-01 03:04:17 +0000