debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
* \| \|	Merge branch 'master' of https://github.com/boogie-org/boogie	akashlal	2015-06-20
\|\ \ \
* \| \| \|	Fix for reading fixpoint back into boogie exprs	akashlal	2015-06-20
\| \| \| \|
* \| \| \|	Missing braces	akashlal	2015-06-20
\| \| \| \|
\| * \| \|	added another sample	qadeer	2015-06-17
\| \| \| \|
\| * \| \|	modified desugaring so that in commutatitivity checks copies of original	qadeer	2015-06-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	codeexpr is made.
\| * \| \|	fixed bug reported by Chris	qadeer	2015-06-15
\| \| \| \|
\| * \| \|	adding z3name option	Ken McMillan	2015-06-15
\|/ / /
* \| \|	Minor changes	Valentin Wüstholz	2015-06-12
\| \| \|
* \| \|	Fix issue with computation of statement checksums for lambda expressions.	Valentin Wüstholz	2015-06-12
\| \| \|
* \| \|	Add a test case.	Valentin Wüstholz	2015-06-12
\| \| \|
* \| \|	Fix issue in checksum computation for lambda expressions.	Valentin Wüstholz	2015-06-12
\| \| \|
* \| \|	Fix minor issue with diagnosing timeouts.	Valentin Wüstholz	2015-06-12
\| \| \|
* \| \|	Merge branch 'master' of https://github.com/boogie-org/boogie	Ken McMillan	2015-06-11
\|\ \ \
\| * \| \|	relaxed the check for created and hidden layers for skip actions	qadeer	2015-06-10
\| \| \| \|
\| * \| \|	fixed crash	qadeer	2015-06-10
\| \| \| \|
\| * \| \|	Merge pull request #14 from cpitclaudel/clean-prover-exit	RustanLeino	2015-06-09
\| \|\ \ \ \| \| \|/ / \| \|/\| \|	Stop truncating the prover logs
* / \| \|	various changes for duality from dead codeplex repo	U-REDMOND\kenmcmil	2015-06-09
\|/ / /
\| * /	Stop truncating the prover logs	Clément Pit--Claudel	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.	Valentin Wüstholz	2015-06-08
\| \|
* \|	Fix minor issue.	Valentin Wüstholz	2015-06-05
\| \|
* \|	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-06-05
\| \|
* \|	Fix for SI: initialize extraRecBound	Akash Lal	2015-06-05
\| \|
* \|	Merge branch 'master' of https://github.com/boogie-org/boogie	akashlal	2015-06-01
\|\ \
* \| \|	Simplified StratifiedVC interface	akashlal	2015-06-01
\| \| \|
\| * \|	Merge branch 'master' of https://github.com/boogie-org/boogie	qadeer	2015-05-31
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	added assume about gate after calls and parallel calls	qadeer	2015-05-31
\| \| \|
* \| \|	Improve heuristics for diagnosing timeouts.	Valentin Wüstholz	2015-05-31
\|/ /
* \|	Merge branch 'master' of https://github.com/boogie-org/boogie	qadeer	2015-05-27
\|\ \
* \| \|	bug fix in pop	qadeer	2015-05-27
\| \| \|
\| * \|	Allow for extra instrumentation on program before vc gen	Akash Lal	2015-05-25
\| \| \|
\| * \|	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-05-22
\|/ /
\| *	added some float addition tests	Dietrich	2015-05-22
\| \|
* \|	Merge branch 'master' of https://github.com/boogie-org/boogie	qadeer	2015-05-20
\|\ \
* \| \|	added more specifications	qadeer	2015-05-20
\| \| \|
\| * \|	Minor changes	Valentin Wüstholz	2015-05-20
\| \| \|
\| * \|	Minor refactoring	Valentin Wüstholz	2015-05-20
\| \| \|
\| * \|	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-05-20
\| \| \|
\| * \|	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-05-19
\| \| \|
\| \| *	added interpretation of floating point constants to the parser	Dietrich	2015-05-18
\| \| \|
\| * \|	Make it not return cached verification results for timed-out implementations ↵	Valentin Wüstholz	2015-05-18
\| \| \| \| \| \| \| \| \| \| \| \|	when timeout diagnostics are enabled.
\| * \|	Add some experimental support for diagnosing timeouts.	Valentin Wüstholz	2015-05-18
\| \| \|
\| * \|	Minor refactoring	Valentin Wüstholz	2015-05-17
\| \| \|
\| * \|	Make caching of verification results more fine-grained for changes that ↵	Valentin Wüstholz	2015-05-17
\| \| \| \| \| \| \| \| \| \| \| \|	affect preconditions.
\| * \|	Fix for printFixedPoint when dealing with functions	Akash Lal	2015-05-13
\| \| \|
\| \| *	Made significant changes to internal representation of BigFloat. Remains a ↵	Dietrich	2015-05-07
\| \| \| \| \| \| \| \| \| \| \| \|	work in progress
\| * \|	SecureVC: example	Akash Lal	2015-05-07
\| \| \|
\| * \|	Fix for secureVCGen	Akash Lal	2015-05-07
\| \| \|
\| * \|	Make it preserve the fact that the value of an assumption variable never ↵	Valentin Wüstholz	2015-05-06
\| \| \| \| \| \| \| \| \| \| \| \|	becomes logically weaker after a havoc.
\| \| *	added decimal reading functionality to the float type	Dietrich	2015-05-05
\| \| \|
\| \| *	added general floating point mantissa and exponent management	Dietrich	2015-05-04
\| \| \|