| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add alpha equivalence check for Expr, and use it when lambda lifting |  Dan Rosén | 2014-08-01 |
| | | |||
| * | enabled merging of yield calls |  qadeer | 2014-07-20 |
| | | |||
| * | added support for facoring out calls to yield checkers; this will help avoid ↵ | qadeer | 2014-07-20 |
| | | | | | quadratic space complexity | ||
| * | minor change | qadeer | 2014-07-19 |
| | | |||
| * | treiber stack fixed | qadeer | 2014-07-18 |
| | | |||
| * | some clean up | qadeer | 2014-07-16 |
| | | |||
| * | Merge | qadeer | 2014-07-15 |
| |\ | |||
| * | | updated the linear type system based on Chris' design with linear, ↵ | qadeer | 2014-07-15 |
| | | | | | | | | | linear_in, linear_out | ||
| | * | 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. | ||
| * | fixed a regression failure | qadeer | 2014-07-15 |
| | | |||
| * | merge | qadeer | 2014-07-15 |
| |\ | |||
| * | | simplified yield type chcking and added treiber stack (not fully done) | qadeer | 2014-07-15 |
| | | | |||
| | * | Fixed a minor issue. | wuestholz | 2014-07-14 |
| | | | |||
| | * | Refactored how checksums are computed. | wuestholz | 2014-07-13 |
| |/ | |||
| * | added tests | qadeer | 2014-07-12 |
| | | |||
| * | fixed some tests in og | qadeer | 2014-07-11 |
| | | | | | | added another test in linear (based on bug reported by Chris) removed the QED build configuration | ||
| * | Worked on the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | | |||
| * | Worked on the more advanced verification result caching (ignore comments for ↵ | wuestholz | 2014-07-10 |
| | | | | | computing statement checksums). | ||
| * | Worked on the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | | |||
| * | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 |
| | | |||
| * | Worked on adding support for "canned errors". | wuestholz | 2014-07-07 |
| | | |||
| * | Added more tests and worked on adding support for "canned errors". | wuestholz | 2014-07-06 |
| | | |||
| * | 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. | ||
| * | Made it collect more statistics about the more advanced verification result ↵ | wuestholz | 2014-07-04 |
| | | | | | caching. | ||
| * | Implemented an optimization for assignments to assumption variables that are ↵ | wuestholz | 2014-07-04 |
| | | | | | injected by the verification result caching for calls within loops. | ||
| * | Made it not include free preconditions when producing partially verified ↵ | wuestholz | 2014-07-03 |
| | | | | | preconditions. | ||
| * | Fixed issue involving axioms in the dependency analysis used for ↵ | wuestholz | 2014-07-03 |
| | | | | | verification result caching. | ||
| * | Made it collect more statistics about the more advanced verification result ↵ | wuestholz | 2014-07-01 |
| | | | | | caching. | ||
| * | Made it collect some statistics about the more advanced verification result ↵ | wuestholz | 2014-06-30 |
| | | | | | caching. | ||
| * | a fix in Inline method; it should look for inline attribute only on ↵ | qadeer | 2014-06-28 |
| | | | | | procedures and implementations | ||
| * | Added a program cache (used by the more advanced verification result caching). | wuestholz | 2014-06-28 |
| | | |||
| * | Minor refactoring | wuestholz | 2014-06-28 |
| | | |||
| * | Changed the verification result cache to use the built-in 'MemoryCache' class. | wuestholz | 2014-06-28 |
| | | |||
| * | OnModel now carries the result of the prover call | akashlal | 2014-06-28 |
| | | |||
| * | Fix in SI while dealing with timeouts | akashlal | 2014-06-27 |
| | | |||
| * | Optimized the way that assertions are marked as partially verified. | wuestholz | 2014-06-26 |
| | | |||
| * | Fixed issue in verification result caching. | wuestholz | 2014-06-26 |
| | | |||
| * | Optimized the way that dependency checkums are computed. | 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 |
| | | |||
| * | Changed the 'verifySnapshots' command-line option to accept a numeric ↵ | wuestholz | 2014-06-20 |
| | | | | | argument instead of a boolean one. | ||
| * | Fixed crash in resolver | Rustan Leino | 2014-06-19 |
| | | |||
| * | Fix bug in BigDec.FromString() which would not parse negative | Dan Liew | 2014-06-18 |
| | | | | | | | | | numbers correctly. For example BigDec.FromString("-1.5") would be interpreted as -0.5 due to the incorrect way the method handles the fractional part of the string. | ||
| * | Added mechanism for getting the variables referenced by a loop (not just the ↵ | Ally Donaldson | 2014-06-09 |
| | | | | | modified vars) | ||
| * | Fixed a bug in revised mod set analysis | Ally Donaldson | 2014-06-06 |
| | | |||
| * | Refactored modset analysis to avoid the use of static fields. Static fields ↵ | Ally Donaldson | 2014-06-06 |
| | | | | | cause data races when we run parts of Boogie that both do mod set analysis at the same time. | ||
| * | Merge | Ally Donaldson | 2014-06-06 |
| |\ | |||
| * | | Small refactoring | Ally Donaldson | 2014-06-06 |
| | | | |||
| * | | Made VarsAssignedInLoop public, since it can be useful in computing modifies ↵ | Ally Donaldson | 2014-06-06 |
| | | | | | | | | | sets elsewhere. | ||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |