debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
* \|	Fixed errors in the use of Code Contracts	Rustan Leino	2014-02-10
\| \|
* \|	Merge	Rustan Leino	2014-02-10
\|\ \
* \| \|	Fixed bug in handling of break statements	Rustan Leino	2014-02-10
\| \| \|
\| * \|	fixed a problem with the nonblocking check	qadeer	2014-02-10
\| \| \|
\| * \|	added nonblocking checker for left movers	qadeer	2014-02-07
\| \| \|
\| * \|	added another example and fixed a bug regarding initialization of pc/ok	qadeer	2014-02-07
\| \| \| \| \| \| \| \| \| \| \| \|	snapshots per loop header
\| * \|	new design for linear types + VCgen	qadeer	2014-02-07
\|/ / \| \| \| \| \| \| \| \|	ported all the examples added the QED examples to runtest.bat
* \|	bug fix in error trace printing	qadeer	2014-02-05
\| \| \| \| \| \| \| \|	added a class for Token elimination (not done yet)
* \|	Option for reversing Houdini worklist (for top-down analysis)	akashlal	2014-01-28
\| \|
* \|	some small optimizations to mover checking	qadeer	2014-01-22
\| \| \| \| \| \| \| \|	added LookUp to multiset.bpl
* \|	various bug fixes	qadeer	2014-01-21
\| \| \| \| \| \| \| \|	added "cnst" feature
* \|	bug fix: if an absy is not reachable, make the set of available vars empty at it	qadeer	2014-01-21
\| \|
* \|	bug fix in handling of parallel call	qadeer	2014-01-20
\| \|
* \|	Added functionality to rename state captures when programs are unrolled.	Ally Donaldson	2014-01-17
\| \|
* \|	Merge	Ally Donaldson	2014-01-17
\|\ \
* \| \|	Integrated support for k-induction, implemented a while ago by Philipp ↵	Ally Donaldson	2014-01-17
\| \| \| \| \| \| \| \| \| \| \| \|	Ruemmer but never previously committed.
\| * \|	bug fix in error trace printing	qadeer	2014-01-16
\| \| \|
\| * \|	fix for a completeness bug (reported by Serdar) in refinement checker	qadeer	2014-01-16
\| \| \|
\| * \|	Clean up of yield type checker	qadeer	2014-01-16
\| \| \|
\| * \|	in the middle of cleaning up yield type checker	qadeer	2014-01-15
\| \| \|
\| * \|	fixed lots of bugs in mover checking code	qadeer	2014-01-14
\| \| \|
\| * \|	fixed bug in optimization of commutativity check	qadeer	2014-01-14
\| \| \|
\| * \|	Merge	qadeer	2014-01-14
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	added more information to assert messages	qadeer	2014-01-14
\| \| \|
* \| \|	Fix Boogie so it compiled with mono. Patch by Dan Liew.	Ally Donaldson	2014-01-14
\|/ /
* \|	Existential failure checker replaced with universal.	stasiran	2014-01-13
\| \|
* \|	a bug fix	qadeer	2014-01-13
\| \|
* \|	eliminated use of assertionPhaseNums	qadeer	2014-01-13
\| \|
* \|	Some proper naming done in YieldTypeChecker	kuruis	2014-01-12
\| \|
* \|	extended NormalSubstituter so that it can take in a forold substitution	qadeer	2014-01-10
\| \| \| \| \| \| \| \|	optimized the FailurePreservationChecker to eliminate some quantifiers
* \|	implemented a simple quantifier elimination for havoc commands in computing ↵	qadeer	2014-01-09
\| \| \| \| \| \| \| \| \| \| \| \|	transition relation changed the type checking of left movers; they are required to be non-blocking now
* \|	some optimizations to mover checks	qadeer	2014-01-09
\| \|
* \|	a fix regarding the checking of assertions in atomic specs at call sites	qadeer	2014-01-08
\| \|
* \|	Merge	qadeer	2014-01-07
\|\ \
* \| \|	first cut of refinement checking	qadeer	2014-01-07
\| \| \|
\| * \|	Recursive walking of Exprs doesn't play nice when the depth of the AST is high.	akashlal	2014-01-07
\|/ / \| \| \| \| \| \| \| \|	Reduce depth of AST whenever possible (e.g., use a binary tree instead of a linear list of terms)
* \|	points on "home strecth of yield type checker" added	kuruis	2014-01-04
\| \|
* \|	Updated year in main copyright message	Rustan Leino	2014-01-03
\| \|
* \|	and another	qadeer	2014-01-03
\| \|
* \|	another small fix	qadeer	2014-01-03
\| \|
* \|	some fixes	qadeer	2014-01-03
\| \|
* \|	First rough draft of refinement checking.	stasiran	2014-01-03
\| \|
* \|	First rough draft of refinement checking.	stasiran	2014-01-03
\| \|
* \|	minor bug in traversing program fixed	kuruis	2014-01-03
\| \|
* \|	some bugs related with phases fixed	kuruis	2014-01-03
\| \|
* \|	debug pragma closed	kuruis	2014-01-02
\| \|
* \|	some fixes on devicedriver example	kuruis	2014-01-02
\| \|
* \|	Error reporting with line numbers and commands of trace is provided	kuruis	2014-01-02
\| \|
* \|	some proper yield check reporting provided	kuruis	2014-01-02
\| \|
* \|	some bugs fixed on yiledtypechecker	kuruis	2013-12-31
\| \|