debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: print inductive datatypes	Rustan Leino	2012-05-01
\|
*	Dafny: added support for co-recursive calls	Rustan Leino	2012-05-01
\|
*	eliminated class ErrorModel	qadeer	2012-04-28
\|
*	removed proccopybounding code	qadeer	2012-04-28
\| \| \| \|	stratified inliinig is now run always with /doNotUseLabels
*	eliminated LazyInliningInfo	qadeer	2012-04-28
\|
*	removed lazy inlining	qadeer	2012-04-28
\|
*	Merge	qadeer	2012-04-27
\|\
* \|	unsat core for houdini	qadeer	2012-04-27
\| \|
\| *	Dafny: fixed unsoundness having to do with a function depending on the ↵	Unknown	2012-04-27
\| \| \| \| \| \| \| \|	allocation state
\| *	Merge	Unknown	2012-04-26
\| \|\ \| \|/ \|/\|
\| *	Dafny: fixed bug that had omitted the computation of .DefaultCtor for some ↵	Unknown	2012-04-26
\| \| \| \| \| \| \| \|	inductive datatypes
\| *	Dafny: compile co-inductive datatypes	Unknown	2012-04-26
\| \| \| \| \| \| \| \|	Dafny: for inductive datatypes, cache any default value computed and also produce slightly tidier target code
\| *	Dafny: rudimentary translation into Boogie of co-inductive datatypes	Unknown	2012-04-25
\| \|
\| *	Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵	Unknown	2012-04-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now)
* \|	Merge	Unknown	2012-04-24
\|\\|
* \|	Started refactoring invariant generation rules.	Unknown	2012-04-24
\| \|
* \|	Removed set encoding.	Unknown	2012-04-24
\| \|
* \|	Significantly changed the way race checking is performed. Made eager race ↵	Unknown	2012-04-24
\| \| \| \| \| \| \| \|	checking and symmetry reduction default, and removed the option to turn these off - makes the code a lot cleaner.
\| *	Added test to stratified inlining.	Unknown	2012-04-24
\| \| \| \| \| \| \| \|	Don't use UNSAT core for the refinement step.
\| *	Merge	Unknown	2012-04-20
\| \|\ \| \|/ \|/\|
\| *	Dafny: fixed bug (missing Boogie cast) in translation of induction over ↵	Unknown	2012-04-20
\| \| \| \| \| \| \| \|	generic datatypes instantiated with datatypes
* \|	removed BoogieDriver from solution	qadeer	2012-04-18
\| \|
* \|	various changes for using unsat cores in Houdini	qadeer	2012-04-17
\| \|
* \|	Merge	Unknown	2012-04-13
\|\ \
* \| \|	Made loop predicate invariant optionally generated.	Unknown	2012-04-13
\| \|/ \|/\|
\| *	Added functionality to "skip" procedures. Some cleanup.	akashlal	2012-04-12
\|/
*	Added invariant to predicated loops.	Unknown	2012-04-10
\|
*	Minor fix to array control flow analysis.	Unknown	2012-04-10
\|
*	Inference in GPUVerify now merges candidates for threads 1 and 2 into a ↵	Unknown	2012-04-10
\| \| \| \|	single conjunctive candidate.
*	Don't insert final barrier when eager race checking is enabled.	paulthomson	2012-04-09
\|
*	Tweak to inference.	Unknown	2012-04-09
\|
*	More accessed offset inference	Unknown	2012-04-09
\|
*	Refined assertion.	Unknown	2012-04-06
\|
*	Tuned candidate generation.	Unknown	2012-04-06
\|
*	Extended GPUVerify's candidate invariant generation to use thread id inference.	Unknown	2012-04-05
\|
*	Inference of thread ids complete.	Unknown	2012-04-05
\|
*	Thread id inference now generalised to infer other thread configuration ↵	Unknown	2012-04-05
\| \| \| \|	parameters.
*	Thread id inference now generalised to three dimensions.	Unknown	2012-04-05
\|
*	Started generalising thread id inference	Unknown	2012-04-05
\|
*	Merge	Unknown	2012-04-05
\|\
* \|	GPUverify now automatically decides then to use adversarial abstraction.	Unknown	2012-04-05
\| \|
\| *	Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).	Unknown	2012-04-04
\| \|
\| *	small fix	qadeer	2012-04-04
\| \| \| \| \| \| \| \|	added regressions
\| *	Merge	qadeer	2012-04-03
\| \|\ \| \|/ \|/\|
\| *	added nonUniformUnfolding option	qadeer	2012-04-03
\| \|
* \|	Fixed bug with handling of return in GPUVerify.	Unknown	2012-04-03
\| \|
* \|	Merge	Unknown	2012-04-03
\|\ \
* \| \|	Added support for break and return.	Unknown	2012-04-03
\| \| \|
\| \| *	deleted the option UseUnsatCoreForInlining	qadeer	2012-04-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Split ApiChecker.CheckAssumptions into two different methods, one which computes the unsatCore and one which does not Further edits to the MaxSat code
\| \| *	Merge	qadeer	2012-04-01
\| \| \|\ \| \| \|/ \| \|/\|