summaryrefslogtreecommitdiff
path: root/Test/inline
Commit message (Expand)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* more tests for houdini /inlineDepthGravatar shuvendu2014-09-19
* additional tests for houdini /inlineDepthGravatar shuvendu2014-09-18
* Removed old test infrastructure files except forGravatar Dan Liew2014-05-28
* Fix lit test suite when running Boogie under a path that containsGravatar Dan Liew2014-05-27
* Enabled the inline lit tests. In order to support expansion2.bplGravatar Dan Liew2014-05-07
* Patch by Nathan Chong: iterative version of remove empty blocks algorithm. T...Gravatar Ally Donaldson2013-12-02
* inlining is now done in rhs of assignments for codeexprsGravatar qadeer2013-08-15
* Extended codeexpr inlining to deal with nested codeexprGravatar qadeer2013-08-15
* updated answer filesGravatar Unknown2013-01-25
* Refactored code that generates an axiom for a function, and changed the prett...Gravatar Rustan Leino2013-01-17
* bug fix for interaction between inlining and loopsGravatar Unknown2013-01-04
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Update test suite for commit 8a59fbb7ee34.Gravatar Peter Collingbourne2012-08-14
* Boogie: Changed Expr.Not to keep swap arguments rather change direction of op...Gravatar Rustan Leino2011-12-12
* fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
* changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
* added the option /inlineDepth:n. This option defaults to -1. If the user prov...Gravatar qadeer2011-11-13
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* Remove a testcase for bvInt (feature to be killed soon)Gravatar MichalMoskal2011-02-18
* Dafny:Gravatar rustanleino2010-09-14
* Boogie:Gravatar rustanleino2010-02-20
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
* Allow ":" in addition to "returns" in function definitions. Make the pretty-p...Gravatar MichalMoskal2009-12-17
* Fixed bug in inlining (procedure *definitions* had been traversed by Standard...Gravatar rustanleino2009-11-19
* Redesigned the encoding of Dafny generics, including the built-in types set a...Gravatar rustanleino2009-11-06
* Fixed bugs in inlining, and added a test case.Gravatar rustanleino2009-10-14
* 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 ar...Gravatar rustanleino2009-08-07
* Fixed problem where nullary function with definition had caused a crash.Gravatar rustanleino2009-08-07
* Removed a temporary file that is created by the test script.Gravatar rustanleino2009-08-06
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 17:34:38 +0000