Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | added another sample | 2015-06-17 | ||
| | | | ||||
| * | | 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 | ||
| | | ||||
* | | Add a test case. | 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 | ||
| | | | ||||
| * | | Merge pull request #14 from cpitclaudel/clean-prover-exit | 2015-06-09 | ||
| |\ \ | | |/ | |/| | Stop truncating the prover logs | |||
* / | | 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 | ||
|/ | ||||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-05-27 | ||
|\ | ||||
* | | bug fix in pop | 2015-05-27 | ||
| | | ||||
| * | Allow for extra instrumentation on program before vc gen | 2015-05-25 | ||
| | | ||||
| * | Improve support for diagnosing timeouts. | 2015-05-22 | ||
|/ | ||||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | 2015-05-20 | ||
|\ | ||||
* | | added more specifications | 2015-05-20 | ||
| | | ||||
| * | 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 | ||
| | | ||||
| * | SecureVC: example | 2015-05-07 | ||
| | | ||||
| * | 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 add build status icon for the Windows build. | 2015-04-28 | ||
| | | ||||
| * | 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 | ||
|/ | ||||
* | renamed og to civl | 2015-04-22 | ||
| | ||||
* | Better error message | 2015-04-21 | ||
| |