Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge FixpointVC changes with mainline | 2014-10-08 | |
|\ | |||
| * | Added "extra recursion bound" to FixedpointVC to support Corral. | 2014-10-08 | |
| | | |||
* | | Did more refactoring and addressed several todos. | 2014-09-23 | |
| | | |||
* | | Did more refactoring. | 2014-09-23 | |
| | | |||
* | | Did some refactoring. | 2014-09-23 | |
|/ | |||
* | Fix nasty bug introduced by commit 61a94f409975. | 2014-07-15 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs. | ||
* | Conjecture printing for duality and child user time tracking. | 2014-05-26 | |
| | |||
* | Merge extra recuresion bound changes for FixedPointVC | 2014-04-21 | |
|\ | |||
* | | Added /printFixedPoint option | 2014-04-14 | |
| | | |||
| * | Added extra recursion bound and preconditions to FixedpointVC. | 2014-03-17 | |
|/ | |||
* | Fixedpoint VC fix. | 2014-02-19 | |
| | |||
* | Fixed bugs in fixedpoint VC gen (including thread problem). | 2013-12-19 | |
| | |||
* | Fixedpoint VC catch up with recent changes | 2013-11-11 | |
| | |||
* | Merge duality changes to mainline | 2013-11-09 | |
|\ | |||
| * | handling timeouts for fixedpoint engines | 2013-11-09 | |
| | | |||
* | | ExprSeq: farewell | 2013-07-22 | |
| | | |||
* | | BlockSeq: farewell | 2013-07-22 | |
| | | |||
* | | CmdSeq: farewell | 2013-07-22 | |
| | | |||
* | | Started to remove ...Seq classes | 2013-07-22 | |
| | | |||
* | | More refactoring | 2013-07-22 | |
| | | |||
* | | More refactoring towards replacing PureCollections.Sequence with List | 2013-07-22 | |
| | | |||
* | | Large refactoring of Hashtable to Dictionary. | 2013-07-22 | |
| | | |||
* | | Refactored variable2sequenceNumber to use Dictionary | 2013-07-22 | |
| | | |||
* | | Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵ | 2013-07-22 | |
| | | | | | | | | plain Hashtable. | ||
* | | Did some refactoring in the execution engine and worked on the parallelization. | 2013-07-01 | |
|/ | |||
* | Fixes for duality under corral | 2013-06-14 | |
| | |||
* | Adding background model to fixedpoint counterexamples and small code ↵ | 2013-05-29 | |
| | | | | contracts fixes | ||
* | Getting fixed point backend to work with Corral. | 2013-05-29 | |
| | |||
* | Working on fixedpoint backend | 2013-05-20 | |
| | |||
* | new files for fixedpoint engine backend | 2013-05-07 | |