debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
* \| \|	UseLabels=false when stratified inline is on	qadeer	2012-04-29
\| \| \|
* \| \|	Merge	qadeer	2012-04-29
\|\\| \|
* \| \|	clean up in stratified inlining	qadeer	2012-04-29
\| \| \|
\| * \|	Boogie build succeeded, 1 test(s) failed	CodeplexBot	2012-04-29
\|/ /
* \|	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 the lazy inline test directory	qadeer	2012-04-28
\| \|
* \|	Merge	qadeer	2012-04-28
\|\ \
* \| \|	removed lazy inlining	qadeer	2012-04-28
\| \| \|
\| * \|	Boogie build succeeded	CodeplexBot	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
\| * \|	Dafny: added resolution tests cases for inductive datatypes	Unknown	2012-04-27
\| \| \|
\| * \|	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
\| \| \|
* \| \|	Boogie build succeeded	CodeplexBot	2012-04-18
\| \| \|
* \| \|	Merge	qadeer	2012-04-17
\|\ \ \
* \| \| \|	various changes for using unsat cores in Houdini	qadeer	2012-04-17
\| \| \| \|
\| * \| \|	Add options to control the emission of free ensures for	Unknown	2012-04-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	heap monotonicity (and allocatedness of references returned from a method) as well as the assert/assume checks that are generated for every object dereference.
\| * \| \|	Merge	Unknown	2012-04-15
\| \|\ \ \ \| \|/ / / \|/\| \| \|
\| * \| \|	Removed expression simplifier (actually just commented	Unknown	2012-04-15
\| \|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	it out for now) and used a simpler scheme for always assigning compound bound expressions to a local. Added the ability to assert/assume that an object is non-null before dereferencing it.
* \| \|	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
\| \|/ /
\| * \|	Temp file added as one to ignore.	Unknown	2012-04-10
\| \| \|
\| * \|	Merge	Unknown	2012-04-10
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Added "free ensures" to procedures encoding the allocatedness	Unknown	2012-04-10
\| \| \| \| \| \| \| \| \| \| \| \|	of references.
* \| \|	Added invariant to predicated loops.	Unknown	2012-04-10
\| \| \|
* \| \|	Minor fix to array control flow analysis.	Unknown	2012-04-10
\| \| \|
* \| \|	Merge	Unknown	2012-04-10
\|\\| \|
* \| \|	Inference in GPUVerify now merges candidates for threads 1 and 2 into a ↵	Unknown	2012-04-10
\| \| \| \| \| \| \| \| \| \| \| \|	single conjunctive candidate.
\| * \|	Merge	Unknown	2012-04-09
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Fix a lot of the translation of "op=" expressions	Unknown	2012-04-09
\| \| \| \| \| \| \| \| \| \| \| \|	(like += or *=).
* \| \|	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
\| \|