Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Normalise line endings using a .gitattributes file. Unfortunately | Dan Liew | 2015-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. | ||
* | Minor changes | Valentin Wüstholz | 2015-06-12 |
| | |||
* | Fix issue with computation of statement checksums for lambda expressions. | Valentin Wüstholz | 2015-06-12 |
| | |||
* | Fix issue in checksum computation for lambda expressions. | Valentin Wüstholz | 2015-06-12 |
| | |||
* | Minor change | wuestholz | 2015-01-26 |
| | |||
* | Did more refactoring. | wuestholz | 2014-09-23 |
| | |||
* | Add alpha equivalence check for Expr, and use it when lambda lifting | Dan Rosén | 2014-08-01 |
| | |||
* | Fix nasty bug introduced by commit 61a94f409975. | Dan Liew | 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. | ||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 |
| | |||
* | Fixed issue involving axioms in the dependency analysis used for ↵ | wuestholz | 2014-07-03 |
| | | | | verification result caching. | ||
* | Changed the 'verifySnapshots' command-line option to accept a numeric ↵ | wuestholz | 2014-06-20 |
| | | | | argument instead of a boolean one. | ||
* | Change class 'LambdaVisitor' to attach checksum to expanded lambda functions. | wuestholz | 2014-03-17 |
| | |||
* | Changed all lambda-expression rewriting to be done as a pre-processing step ↵ | Rustan Leino | 2014-02-28 |
| | | | | | | before real verification. Fixed treatment of lambda-expression attributes. | ||
* | Changed return type of VisitLambdaExpr to just Expr | Rustan Leino | 2014-02-27 |
| | |||
* | All ...Seq classes now gone | Ally Donaldson | 2013-07-22 |
| | |||
* | ExprSeq: farewell | Ally Donaldson | 2013-07-22 |
| | |||
* | Started to remove ...Seq classes | Ally Donaldson | 2013-07-22 |
| | |||
* | Large refactoring of Hashtable to Dictionary. | Ally Donaldson | 2013-07-22 |
| | |||
* | Make set iteration order deterministic | Michal Moskal | 2011-12-07 |
| | | | | Make the set class generic | ||
* | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |