debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge extra recuresion bound changes for FixedPointVC	Ken McMillan	2014-04-21
\|\
* \	Merge changes for /printFixedPoint option	Ken McMillan	2014-04-14
\|\ \
\| * \|	Added /printFixedPoint option	Ken McMillan	2014-04-14
\| \| \|
* \| \|	resolved expressions created during generation of procedures for mover checks	qadeer	2014-04-14
\| \| \|
* \| \|	Fixed abstract interpretation for reals	Rustan Leino	2014-04-13
\|/ /
* \|	Fixed bug in abstract interpretation over reals	Rustan Leino	2014-04-08
\| \|
* \|	Added option to avoid unrolling irreducible loops	akashlal	2014-04-06
\| \|
* \|	Fixed class cast issue with type synonyms	Ally Donaldson	2014-04-01
\| \|
* \|	Fixes to predication. Patch by Jeroen Ketema.	Ally Donaldson	2014-03-18
\| \|
\| *	Added extra recursion bound and preconditions to FixedpointVC.	Ken McMillan	2014-03-17
\| \|
* \|	Change class 'LambdaVisitor' to attach checksum to expanded lambda functions.	wuestholz	2014-03-17
\| \|
* \|	More exhaustive generation of assertions during predication. Patch by ↵	Ally Donaldson	2014-03-14
\| \| \| \| \| \| \| \|	Jeroen Ketema
* \|	Fix duplicator so that BVConcatExpr and BVExtractExpr are handled. Patch by ↵	Ally Donaldson	2014-03-12
\| \| \| \| \| \| \| \|	Daniel Liew.
* \|	Fix to predication	Ally Donaldson	2014-03-05
\| \|
* \|	Merge	Rustan Leino	2014-02-28
\|\ \
* \| \|	Changed all lambda-expression rewriting to be done as a pre-processing step ↵	Rustan Leino	2014-02-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	before real verification. Fixed treatment of lambda-expression attributes.
\| * \|	Added a fix to inlining so that it becomes cognizant of procedures that the ↵	qadeer	2014-02-28
\| \| \| \| \| \| \| \| \| \| \| \|	user wants to check
\| * \|	Added /trustNonInterference option	qadeer	2014-02-28
\| \| \|
* \| \|	Changed return type of VisitLambdaExpr to just Expr	Rustan Leino	2014-02-27
\| \| \|
\| * \|	added /doNotUseParallelism option	qadeer	2014-02-27
\| \| \|
\| * \|	added some missing attributes to desugared assertions	qadeer	2014-02-27
\|/ /
* \|	added tokens to calls and requires/ensures	qadeer	2014-02-26
\| \|
* \|	Merge	qadeer	2014-02-25
\|\ \
* \| \|	fixed couple of bugs reported by Serdar	qadeer	2014-02-25
\| \| \|
\| * \|	Fixed tokens to improve error message produce for type errors in non-inlined ↵	Rustan Leino	2014-02-25
\|/ / \| \| \| \| \| \|	function bodies
* \|	(Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵	Rustan Leino	2014-02-24
\| \| \| \| \| \| \| \| \| \| \| \|	of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
* \|	added ReadOnlyStandardVisitor	qadeer	2014-02-24
\| \| \| \| \| \| \| \|	made the default phase of assertions be 0
* \|	Added /trustPhasesDownto option	qadeer	2014-02-24
\| \|
* \|	Added /trustPhasesUpto option	qadeer	2014-02-23
\| \|
* \|	Added /trustAtomicityTypes option	qadeer	2014-02-22
\|/
*	Merge ModelParser fix	Ken McMillan	2014-02-21
\|\
\| *	Fixed crash in ModelParser when Z3 returns an operator that is a list.	Ken McMillan	2014-02-21
\| \|
* \|	fixed a bug in desugaring of linear variables	qadeer	2014-02-20
\|/
*	Merge fixedpoint VC fix	Ken McMillan	2014-02-19
\|\
\| *	Fixedpoint VC fix.	Ken McMillan	2014-02-19
\| \|
* \|	fixed a bug in the automaton construction labeling	qadeer	2014-02-18
\| \|
* \|	fixed code contracts violations	qadeer	2014-02-11
\| \|
* \|	Fixed bug in printing real literals	Rustan Leino	2014-02-10
\| \|
* \|	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
\| \|