Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | 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. | |||
* | Refactored how checksums are computed. | wuestholz | 2014-07-13 | |
| | ||||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 | |
| | ||||
* | Worked on adding support for "canned errors". | wuestholz | 2014-07-07 | |
| | ||||
* | Worked on adding support for "canned errors". | wuestholz | 2014-07-06 | |
| | ||||
* | Did some refactoring, fixed minor issues, and made it apply the more ↵ | wuestholz | 2014-07-06 | |
| | | | | advanced verification result caching even for implementations with errors. | |||
* | Fixed issue involving axioms in the dependency analysis used for ↵ | wuestholz | 2014-07-03 | |
| | | | | verification result caching. | |||
* | Fixed issue in verification result caching. | wuestholz | 2014-06-26 | |
| | ||||
* | Add some pretty-printing, on by default. Turn off with the flag "/pretty:0" | Dan Rosén | 2014-06-24 | |
| | | | | | | When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off. | |||
* | Worked on an extension of the existing verification result caching. | wuestholz | 2014-06-23 | |
| | ||||
* | Implemented an additional type check for assumption variables. | wuestholz | 2014-05-27 | |
| | ||||
* | Add support for assumption variables. | wuestholz | 2014-04-21 | |
| | ||||
* | added variable hiding | qadeer | 2014-04-16 | |
| | | | | added annotation on an atomic action about the phases in which it exists | |||
* | Added option to avoid unrolling irreducible loops | akashlal | 2014-04-06 | |
| | ||||
* | Fixed tokens to improve error message produce for type errors in non-inlined ↵ | Rustan Leino | 2014-02-25 | |
| | | | | function bodies | |||
* | Fixed errors in the use of Code Contracts | Rustan Leino | 2014-02-10 | |
| | ||||
* | Added functionality to rename state captures when programs are unrolled. | Ally Donaldson | 2014-01-17 | |
| | ||||
* | various updates and tighter integration of QED stuff into mainline | qadeer | 2013-12-19 | |
| | ||||
* | fixed type checking errors in QED stuff | qadeer | 2013-12-14 | |
| | ||||
* | fixes to type checking code | qadeer | 2013-12-11 | |
| | ||||
* | some refactoring of QED stuff | qadeer | 2013-12-10 | |
| | ||||
* | some minor fixes | qadeer | 2013-08-21 | |
| | ||||
* | extended inlining to deal with codeexprs | qadeer | 2013-08-14 | |
| | ||||
* | cleaned up the OG code | qadeer | 2013-08-07 | |
| | | | | enabled it to be always on | |||
* | Fixed several build errors in the 'Checked' configuration. | wuestholz | 2013-08-05 | |
| | ||||
* | Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵ | wuestholz | 2013-07-22 | |
| | | | | code (as opposed to contracts). | |||
* | All ...Seq classes now gone | Ally Donaldson | 2013-07-22 | |
| | ||||
* | ExprSeq: farewell | Ally Donaldson | 2013-07-22 | |
| | ||||
* | RESeq: farewell | Ally Donaldson | 2013-07-22 | |
| | ||||
* | BlockSeq: farewell | Ally Donaldson | 2013-07-22 | |
| | ||||
* | StringSeq: farewell | Ally Donaldson | 2013-07-22 | |
| | ||||
* | CmdSeq: farewell | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Started to remove ...Seq classes | Ally Donaldson | 2013-07-22 | |
| | ||||
* | More refactoring | Ally Donaldson | 2013-07-22 | |
| | ||||
* | More refactoring | Ally Donaldson | 2013-07-22 | |
| | ||||
* | More refactoring | Ally Donaldson | 2013-07-22 | |
| | ||||
* | More refactoring | Ally Donaldson | 2013-07-22 | |
| | ||||
* | More refactoring: PureCollections.Sequence not used anymore. | Ally Donaldson | 2013-07-22 | |
| | ||||
* | More refactoring towards replacing PureCollections.Sequence with List | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Refactoring of TypeVariableSeq | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Changed Has method of PureSequence to Contains to make refactoring easier. | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Refactoring of VariableSeq and TypeSeq | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Requires/EnsuresSeq replaced by List<Requires/Ensures> | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Refactored RequiresSeq and EnsuresSeq so that they wrap List<Requires> and ↵ | Ally Donaldson | 2013-07-22 | |
| | | | | List<Ensures>, respectively, as a first step towards simply using the List versions. | |||
* | Large refactoring of Hashtable to Dictionary. | Ally Donaldson | 2013-07-22 | |
| | ||||
* | Added an attribute to set the time limit for implementations. | wuestholz | 2013-07-12 | |
| | ||||
* | Worked on the parallelization (task cancellation). | wuestholz | 2013-07-09 | |
| | ||||
* | Added support in the abstract interpreter for an attribute {:identity}, ↵ | Rustan Leino | 2013-07-05 | |
| | | | | which says that a function is an identity function. | |||
* | Did some refactoring in the execution engine. | wuestholz | 2013-06-14 | |
| | ||||
* | Worked on improving program snapshot verification. | wuestholz | 2013-06-10 | |
| |