summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Move release to unstableGravatar Benjamin Barenblat2016-04-01
|
* Package Boogie programs for experimentalGravatar Benjamin Barenblat2016-04-01
|
* Package Boogie library for experimentalGravatar Benjamin Barenblat2016-04-01
|
* Make DFSG-cleanGravatar Benjamin Barenblat2016-03-31
|
* Try to unbreak the tests added inGravatar Dan Liew2015-06-28
| | | | 7f4e6b0fab58bb3028cd0f1734fc97b3feafefdf under Windows.
* Update URL to boogie-partners to its new location on GitHub.Gravatar Dan Liew2015-06-28
|
* Fix issue #16 reported by @crazyktGravatar Dan Liew2015-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.
* Add travis file to gitattributes file.Gravatar Dan Liew2015-06-28
|
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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.Gravatar Dan Liew2015-06-28
|
* removed a stray Console.WriteLine that Ken had earlier checked in byGravatar qadeer2015-06-25
| | | | mistake.
* updated with Serdar's changesGravatar qadeer2015-06-25
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar akashlal2015-06-20
|\
* | Fix for reading fixpoint back into boogie exprsGravatar akashlal2015-06-20
| |
* | Missing bracesGravatar akashlal2015-06-20
| |
| * added another sampleGravatar qadeer2015-06-17
| |
| * modified desugaring so that in commutatitivity checks copies of originalGravatar qadeer2015-06-17
| | | | | | | | codeexpr is made.
| * fixed bug reported by ChrisGravatar qadeer2015-06-15
| |
| * adding z3name optionGravatar Ken McMillan2015-06-15
|/
* Minor changesGravatar Valentin Wüstholz2015-06-12
|
* Fix issue with computation of statement checksums for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
|
* Add a test case.Gravatar Valentin Wüstholz2015-06-12
|
* Fix issue in checksum computation for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
|
* Fix minor issue with diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-12
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Ken McMillan2015-06-11
|\
| * relaxed the check for created and hidden layers for skip actionsGravatar qadeer2015-06-10
| |
| * fixed crashGravatar qadeer2015-06-10
| |
| * Merge pull request #14 from cpitclaudel/clean-prover-exitGravatar RustanLeino2015-06-09
| |\ | | | | | | Stop truncating the prover logs
* | | various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
|/ /
| * Stop truncating the prover logsGravatar Clément Pit--Claudel2015-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.Gravatar Valentin Wüstholz2015-06-08
|
* Fix minor issue.Gravatar Valentin Wüstholz2015-06-05
|
* Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-05
|
* Fix for SI: initialize extraRecBoundGravatar Akash Lal2015-06-05
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar akashlal2015-06-01
|\
* | Simplified StratifiedVC interfaceGravatar akashlal2015-06-01
| |
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar qadeer2015-05-31
| |\ | |/ |/|
| * added assume about gate after calls and parallel callsGravatar qadeer2015-05-31
| |
* | Improve heuristics for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-31
|/
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar qadeer2015-05-27
|\
* | bug fix in popGravatar qadeer2015-05-27
| |
| * Allow for extra instrumentation on program before vc genGravatar Akash Lal2015-05-25
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-22
|/
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar qadeer2015-05-20
|\
* | added more specificationsGravatar qadeer2015-05-20
| |
| * Minor changesGravatar Valentin Wüstholz2015-05-20
| |
| * Minor refactoringGravatar Valentin Wüstholz2015-05-20
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-20
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-19
| |
| * Make it not return cached verification results for timed-out implementations ↵Gravatar Valentin Wüstholz2015-05-18
| | | | | | | | when timeout diagnostics are enabled.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 05:28:59 +0000