summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
| * | | added a fix to check all layers: created layer of actions or layers inGravatar Shaz Qadeer2015-10-01
| | | | | | | | | | | | | | | | requires, ensures, or asserts
| | * | Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-10-01
| |/ /
| * | another fix requested by ChrisGravatar Shaz Qadeer2015-10-01
| | | | | | | | | | | | verification is performed now for all created layers
| * | Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-09-30
| | |
| * | updateGravatar Shaz Qadeer2015-09-28
| | |
| * | cleaned up some namesGravatar Shaz Qadeer2015-09-28
| | |
| * | a bug fixGravatar Shaz Qadeer2015-09-27
| | |
| * | fixed a small bugGravatar Shaz Qadeer2015-09-27
| | |
| * | removed a warningGravatar Shaz Qadeer2015-09-26
| | |
| * | added introduced and ghost local variablesGravatar Shaz Qadeer2015-09-25
| | |
| | * Modified BigFloat to avoid evaluating the floating point value before ↵Gravatar Checkmate502015-09-23
| | | | | | | | | | | | sending it to z3
| | * Added initial support for float additionGravatar Checkmate502015-09-17
| | |
| * | fixed my earlier to make it nicerGravatar Shaz Qadeer2015-09-03
| | |
| * | fixed a crash when there is no collectorGravatar Shaz Qadeer2015-09-02
| | |
| * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
| |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect
| * | | Added /verifySnapshots:3, which prints recycled errors messages with the ↵Gravatar Rustan Leino2015-08-28
| | | | | | | | | | | | | | | | source locations of the new code.
| | | * Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
| | | |
| | * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Shuvendu Lahiri2015-07-20
| | |\ \
| | | * | Added another test.Gravatar Valentin Wüstholz2015-07-20
| | | | |
| | | * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Akash Lal2015-07-20
| | | |\ \
| | | * | | Minor additions to VC genGravatar Akash Lal2015-07-20
| |_|/ / / |/| | | |
| | | * | Added more tests.Gravatar Valentin Wüstholz2015-07-20
| |_|/ / |/| | |
| | * | fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
| |/ / |/| |
| | * Modified internal abstract float representation to allow user-defined ↵Gravatar Dietrich2015-07-13
| | | | | | | | | | | | mantissa and exponent
* | | 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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 23:05:10 +0000