summaryrefslogtreecommitdiff
path: root/Test/textbook
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.
* Converted textbook tests to lit tests.Gravatar Dan Liew2014-04-08
|
* Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
|
* Added some Dafny and Boogie test cases, including Turing's factorial ↵Gravatar Rustan Leino2011-11-03
| | | | program, Hoare's classic FIND, and some induction tests for negative integers
* 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
* 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.
* 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-05-17 11:03:26 +0000