debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	qadeer	2013-10-15
\|\
* \|	bug fix in yield inference in modset analysis	qadeer	2013-10-15
\| \|
\| *	Fix for the Duplicator.	akashlal	2013-10-15
\| \|
\| *	Merge	Ally Donaldson	2013-10-11
\| \|\
\| * \|	Small fix in uniformity analysis	Ally Donaldson	2013-10-10
\| \| \|
\| \| *	Merge	Pantazis Deligiannis	2013-10-10
\| \| \|\ \| \| \|/ \| \|/\|
\| \| *	small cleanup	Pantazis Deligiannis	2013-10-10
\| \| \|
\| * \|	Merge	Pantazis Deligiannis	2013-10-09
\| \|\ \ \| \|/ / \|/\| / \| \|/
\| *	fixed bug with the exchange refuted invariants process	Pantazis Deligiannis	2013-10-06
\| \|
\| *	small refactoring	Pantazis Deligiannis	2013-10-02
\| \|
\| *	removal of comment	Pantazis Deligiannis	2013-10-02
\| \|
\| *	support for disabling loop entry invariant assertion checking	Pantazis Deligiannis	2013-10-01
\| \|
\| *	fixed bug	Pantazis Deligiannis	2013-10-01
\| \|
\| *	changes to support a configured errorLimit	Pantazis Deligiannis	2013-09-30
\| \|
\| *	more changes towards parallelisation of Houdini	Pantazis Deligiannis	2013-09-29
\| \|
\| *	refactoring + new class ConcurrentHoudini	Pantazis Deligiannis	2013-09-27
\| \|
\| *	refuted candidates are exchanged in memory using a concurrent dictionary ↵	Pantazis Deligiannis	2013-09-26
\| \| \| \| \| \| \| \|	instead of using an IO csv file as before
* \|	minor fix so that variable copies in procedures and codeexprs are different.	qadeer	2013-09-10
\| \|
* \|	refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of ↵	qadeer	2013-09-09
\| \| \| \| \| \| \| \|	GenerateVC
* \|	fixed bug	qadeer	2013-09-09
\| \|
* \|	No need for OG with Stratified Inlining.	akashlal	2013-09-08
\| \|
* \|	fixed bug introduced by the last checkin in letvciterative	qadeer	2013-09-08
\| \| \| \| \| \| \| \|	added /vc:i to all tests in stratifiedinline
* \|	fixed the problem with codexprs	qadeer	2013-09-07
\| \| \| \| \| \| \| \|	now positive/negative context is detected and appropriate translation is done
* \|	When a codeexpr is used at the top-level in an assume statement, we use the ↵	qadeer	2013-09-04
\| \| \| \| \| \| \| \|	alternative existential semantics.
* \|	Factored out the closure for codeexpr conversion so that it can be reused.	qadeer	2013-09-04
\| \| \| \| \| \| \| \|	Enabled it in stratified inlining.
* \|	fixed the linear type checking related to globals	qadeer	2013-09-04
\| \| \| \| \| \| \| \| \| \|	fixed the modset analysis so that it infers the stable predicate also added more information to type error messages
* \|	Applied Chris Hawblitzel's changes to deal with {:expand}	qadeer	2013-08-23
\| \| \| \| \| \| \| \|	Erased {:yields} in the resulting sequential program in OwickiGriesTransform
* \|	some minor fixes	qadeer	2013-08-21
\| \|
\| *	Merge	Pantazis Deligiannis	2013-08-20
\| \|\ \| \|/ \|/\|
\| *	improvements to the refuted annotations exchange process	Pantazis Deligiannis	2013-08-20
\| \|
\| *	new option for reversing the topological order - this could potentially help ↵	Pantazis Deligiannis	2013-08-19
\| \| \| \| \| \| \| \|	to speedup houdini refutation of candidates
* \|	inlining is now done in rhs of assignments for codeexprs	qadeer	2013-08-15
\| \| \| \| \| \| \| \|	added more regressions
* \|	Extended codeexpr inlining to deal with nested codeexpr	qadeer	2013-08-15
\| \| \| \| \| \| \| \|	Added a regression
\| *	new option to disable checking for loop maintained invariants - this leads ↵	Pantazis Deligiannis	2013-08-15
\| \| \| \| \| \| \| \|	to an underapproximation that helps to speedup houdini refutation of candidates
* \|	extended inlining to deal with codeexprs	qadeer	2013-08-14
\| \|
* \|	Fixed a contract.	wuestholz	2013-08-09
\| \|
* \|	process procedure only if an implementation is present.	qadeer	2013-08-07
\| \|
* \|	cleaned up the OG code	qadeer	2013-08-07
\| \| \| \| \| \| \| \|	enabled it to be always on
* \|	Changed BVD to display shortened names if they are unique.	wuestholz	2013-08-05
\| \|
* \|	Merge	Ally Donaldson	2013-08-05
\|\ \
* \| \|	Minor changes to uniformity analysis and inter-procedural reachability analysis.	Ally Donaldson	2013-08-05
\| \| \|
\| * \|	Fixed several build errors in the 'Checked' configuration.	wuestholz	2013-08-05
\| \| \|
\| * \|	Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 ↵	Rustan Leino	2013-08-02
\| \| \| \| \| \| \| \| \| \| \| \|	unexpectedly to output model information
\| * \|	Turned on options in Z3 to try producing models for timeouts.	wuestholz	2013-08-02
\| \| \|
\| * \|	Make it possible to set the font in BVD externally.	wuestholz	2013-07-31
\|/ /
* \|	Make it possible to look up variables in the Dafny error models.	wuestholz	2013-07-30
\| \|
* \|	Added test cases for symdiff (z3multipleErrors flag)	Unknown	2013-07-30
\| \|
\| *	changes in the parallel houdini script	Pantazis Deligiannis	2013-07-30
\| \|
* \|	Make the dependency analysis for snapshot verification take 'where' clauses ↵	wuestholz	2013-07-30
\| \| \| \| \| \| \| \|	into account.
\| *	added script for running the portfolio solver (parallel houdini)	Pantazis Deligiannis	2013-07-30
\| \|