summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
...
| * 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
| | |\
| | | * Minor additions to VC genGravatar Akash Lal2015-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
| | * 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.
| | * 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.
| | * 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
| | | |
| | | * 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
| | |
| | * 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
| | | |
| | * | 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
| |/
| * Allow for extra instrumentation on program before vc genGravatar Akash Lal2015-05-25
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-22
| |
| * 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
| |
* | added interpretation of floating point constants to the parserGravatar Dietrich2015-05-18
| |
| * Make it not return cached verification results for timed-out implementations ↵Gravatar Valentin Wüstholz2015-05-18
| | | | | | | | when timeout diagnostics are enabled.
| * Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 01:21:51 +0000