Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update URL to boogie-partners to its new location on GitHub. | 2015-06-28 | |
| | |||
* | Fix issue #16 reported by @crazykt | 2015-06-28 | |
| | | | | | | | | | | Previously when Boogie was passed the ``-proc:<NAME>`` argument on the command line it would verify any procedure whose name contained ``<NAME>`` which doesn't seem like correct behaviour. Now Boogie only tries to verify a procedure only if its name matches ``<NAME>`` exactly. I've added several test cases to check Boogie behaves as expected. | ||
* | Normalise line endings using a .gitattributes file. Unfortunately | 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. | ||
* | Remove dead file. | 2015-06-28 | |
| | |||
* | removed a stray Console.WriteLine that Ken had earlier checked in by | 2015-06-25 | |
| | | | | mistake. | ||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-06-20 | |
|\ | |||
* | | Fix for reading fixpoint back into boogie exprs | 2015-06-20 | |
| | | |||
* | | Missing braces | 2015-06-20 | |
| | | |||
| * | modified desugaring so that in commutatitivity checks copies of original | 2015-06-17 | |
| | | | | | | | | codeexpr is made. | ||
| * | fixed bug reported by Chris | 2015-06-15 | |
| | | |||
| * | adding z3name option | 2015-06-15 | |
|/ | |||
* | Minor changes | 2015-06-12 | |
| | |||
* | Fix issue with computation of statement checksums for lambda expressions. | 2015-06-12 | |
| | |||
* | Fix issue in checksum computation for lambda expressions. | 2015-06-12 | |
| | |||
* | Fix minor issue with diagnosing timeouts. | 2015-06-12 | |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-06-11 | |
|\ | |||
| * | relaxed the check for created and hidden layers for skip actions | 2015-06-10 | |
| | | |||
| * | fixed crash | 2015-06-10 | |
| | | |||
* | | various changes for duality from dead codeplex repo | 2015-06-09 | |
| | | |||
| * | Stop truncating the prover logs | 2015-06-09 | |
|/ | | | | | | | | | | | | | | | | | | | | | | | | As it stands, Boogie abruptly aborts the prover by calling Kill() on the associated process after receiving responses to all of its queries. In most cases this is fine, but in general this is pretty bad: it yields to all sorts of output corruption when user-supplied options require z3 to write output to an auxiliary file (say, using /z3opt:TRACE=true). This explains why VCC's Axiom Profiler often complains about a missing [eof] after running Boogie with /z3opt:TRACE=true. This patch fixes it by only falling back to Kill if the process seems to have become unresponsive. That is, it starts by cleanly closing the process input, which signals the end of the interactive session. It then waits for a clean exit for 2s, and only after that does it resort to calling Kill(). I've striven for minimal modifications to the logic, so the patch still universally swallows errors that might occur while closing the underlying stream, and still calls Kill() (I wouldn't be against Boogie just hanging if z3 hangs too). On my tests, z3 exits cleanly pretty much instantly after input is closed anyway, so I don't expect the timeout to fire often (which would be one more reason to actually remove that timeout, and condition Boogie's exit on that of z3 IMO). | ||
* | Improve support for diagnosing timeouts. | 2015-06-08 | |
| | |||
* | Fix minor issue. | 2015-06-05 | |
| | |||
* | Improve support for diagnosing timeouts. | 2015-06-05 | |
| | |||
* | Fix for SI: initialize extraRecBound | 2015-06-05 | |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-06-01 | |
|\ | |||
* | | Simplified StratifiedVC interface | 2015-06-01 | |
| | | |||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-05-31 | |
| |\ | |/ |/| | |||
| * | added assume about gate after calls and parallel calls | 2015-05-31 | |
| | | |||
* | | Improve heuristics for diagnosing timeouts. | 2015-05-31 | |
|/ | |||
* | Allow for extra instrumentation on program before vc gen | 2015-05-25 | |
| | |||
* | Improve support for diagnosing timeouts. | 2015-05-22 | |
| | |||
* | Minor changes | 2015-05-20 | |
| | |||
* | Minor refactoring | 2015-05-20 | |
| | |||
* | Improve support for diagnosing timeouts. | 2015-05-20 | |
| | |||
* | Improve support for diagnosing timeouts. | 2015-05-19 | |
| | |||
* | Make it not return cached verification results for timed-out implementations ↵ | 2015-05-18 | |
| | | | | when timeout diagnostics are enabled. | ||
* | Add some experimental support for diagnosing timeouts. | 2015-05-18 | |
| | |||
* | Minor refactoring | 2015-05-17 | |
| | |||
* | Make caching of verification results more fine-grained for changes that ↵ | 2015-05-17 | |
| | | | | affect preconditions. | ||
* | Fix for printFixedPoint when dealing with functions | 2015-05-13 | |
| | |||
* | Fix for secureVCGen | 2015-05-07 | |
| | |||
* | Make it preserve the fact that the value of an assumption variable never ↵ | 2015-05-06 | |
| | | | | becomes logically weaker after a havoc. | ||
* | Fix for AbsHoudini | 2015-05-01 | |
| | |||
* | AbsHoudini: made disjunct bound a parameter | 2015-05-01 | |
| | |||
* | Add support for 'verified_under' attributes on procedure calls and invariants. | 2015-04-29 | |
| | |||
* | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a | 2015-04-26 | |
| | | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error | ||
* | Minor fixes for AbsHoudini | 2015-04-23 | |
| | |||
* | Better error message | 2015-04-21 | |
| | |||
* | patched ghost checking | 2015-04-18 | |
| | |||
* | changed aux attribute to ghost | 2015-04-18 | |
| |