summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/FixedpointVC.cs
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.
* various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
|
* Fix for printFixedPoint when dealing with functionsGravatar Akash Lal2015-05-13
|
* Merge FixpointVC changes with mainlineGravatar Ken McMillan2014-10-08
|\
| * Added "extra recursion bound" to FixedpointVC to support Corral.Gravatar Ken McMillan2014-10-08
| |
* | Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
| |
* | Did more refactoring.Gravatar wuestholz2014-09-23
| |
* | Did some refactoring.Gravatar wuestholz2014-09-23
|/
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-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.Gravatar Ken McMillan2014-05-26
|
* Merge extra recuresion bound changes for FixedPointVCGravatar Ken McMillan2014-04-21
|\
* | Added /printFixedPoint optionGravatar Ken McMillan2014-04-14
| |
| * Added extra recursion bound and preconditions to FixedpointVC.Gravatar Ken McMillan2014-03-17
|/
* Fixedpoint VC fix.Gravatar Ken McMillan2014-02-19
|
* Fixed bugs in fixedpoint VC gen (including thread problem).Gravatar Ken McMillan2013-12-19
|
* Fixedpoint VC catch up with recent changesGravatar Ken McMillan2013-11-11
|
* Merge duality changes to mainlineGravatar Ken McMillan2013-11-09
|\
| * handling timeouts for fixedpoint enginesGravatar Ken McMillan2013-11-09
| |
* | ExprSeq: farewellGravatar Ally Donaldson2013-07-22
| |
* | BlockSeq: farewellGravatar Ally Donaldson2013-07-22
| |
* | CmdSeq: farewellGravatar Ally Donaldson2013-07-22
| |
* | Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
| |
* | More refactoringGravatar Ally Donaldson2013-07-22
| |
* | More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
| |
* | Large refactoring of Hashtable to Dictionary.Gravatar Ally Donaldson2013-07-22
| |
* | Refactored variable2sequenceNumber to use DictionaryGravatar Ally Donaldson2013-07-22
| |
* | Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵Gravatar Ally Donaldson2013-07-22
| | | | | | | | plain Hashtable.
* | Did some refactoring in the execution engine and worked on the parallelization.Gravatar wuestholz2013-07-01
|/
* Fixes for duality under corralGravatar Ken McMillan2013-06-14
|
* Adding background model to fixedpoint counterexamples and small code ↵Gravatar Ken McMillan2013-05-29
| | | | contracts fixes
* Getting fixed point backend to work with Corral.Gravatar Ken McMillan2013-05-29
|
* Working on fixedpoint backendGravatar Ken McMillan2013-05-20
|
* new files for fixedpoint engine backendGravatar Unknown2013-05-07