debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	a bug fix in Houdini (also AbsHoudini)	qadeer	2014-09-19
\|
*	additional tests for houdini /inlineDepth	shuvendu	2014-09-18
\|
*	merge	qadeer	2014-08-08
\|\
* \|	fixed codexpr bug reported by Michael Emmi; removed special handling of ↵	qadeer	2014-08-08
\| \| \| \| \| \| \| \|	codexpr in InjectPostConditions
\| *	Merge	Dan Rosén	2014-08-01
\| \|\ \| \|/ \|/\|
\| *	Add alpha equivalence check for Expr, and use it when lambda lifting	Dan Rosén	2014-08-01
\| \|
* \|	deleted the free assume about gates after parallel calls	qadeer	2014-07-26
\|/
*	enabled merging of yield calls	qadeer	2014-07-20
\|
*	minor change	qadeer	2014-07-19
\|
*	treiber stack fixed	qadeer	2014-07-18
\|
*	some clean up	qadeer	2014-07-16
\|
*	updated the linear type system based on Chris' design with linear, ↵	qadeer	2014-07-15
\| \| \| \|	linear_in, linear_out
*	simplified yield type chcking and added treiber stack (not fully done)	qadeer	2014-07-15
\|
*	added tests	qadeer	2014-07-12
\|
*	fixed some tests in og	qadeer	2014-07-11
\| \| \| \| \|	added another test in linear (based on bug reported by Chris) removed the QED build configuration
*	Worked on the more advanced verification result caching.	wuestholz	2014-07-10
\|
*	Worked on the more advanced verification result caching.	wuestholz	2014-07-10
\|
*	Worked on the more advanced verification result caching.	wuestholz	2014-07-09
\|
*	Added more tests and worked on adding support for "canned errors".	wuestholz	2014-07-06
\|
*	Worked on adding support for "canned errors".	wuestholz	2014-07-06
\|
*	Did some refactoring, fixed minor issues, and made it apply the more ↵	wuestholz	2014-07-06
\| \| \| \|	advanced verification result caching even for implementations with errors.
*	Implemented an optimization for assignments to assumption variables that are ↵	wuestholz	2014-07-04
\| \| \| \|	injected by the verification result caching for calls within loops.
*	Fixed issue involving axioms in the dependency analysis used for ↵	wuestholz	2014-07-03
\| \| \| \|	verification result caching.
*	Optimized the way that assertions are marked as partially verified.	wuestholz	2014-06-26
\|
*	Fixed issue in verification result caching.	wuestholz	2014-06-26
\|
*	Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"	Dan Rosén	2014-06-24
\| \| \| \| \| \|	When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off.
*	Worked on an extension of the existing verification result caching.	wuestholz	2014-06-23
\|
*	Changed the 'verifySnapshots' command-line option to accept a numeric ↵	wuestholz	2014-06-20
\| \| \| \|	argument instead of a boolean one.
*	Fixed crash in resolver	Rustan Leino	2014-06-19
\|
*	updated golden outputs and removed irrelevant tests	qadeer	2014-06-02
\|
*	Added more tests (snapshots).	wuestholz	2014-05-30
\|
*	Documented the clean.py script	Dan Liew	2014-05-28
\|
*	Document lit's ``-s`` option.	Dan Liew	2014-05-28
\|
*	Remove a few other old test infrastructure files. They	Dan Liew	2014-05-28
\| \| \| \| \|	probably aren't very useful anymore now that the old test infrastructure is gone.
*	Removed old test infrastructure files except for	Dan Liew	2014-05-28
\| \| \| \| \| \| \| \| \|	./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
*	Merge	Dan Liew	2014-05-28
\|\
* \|	Report the python version being used when executing lit.	Dan Liew	2014-05-28
\| \|
* \|	Fix running pydiff.py under Python 2.7	Dan Liew	2014-05-28
\| \|
\| *	Updated an 'Answer' file (AbsHoudini).	wuestholz	2014-05-28
\|/
*	Merge	Dan Liew	2014-05-27
\|\
* \|	Fix lit test suite when running Boogie under a path that contains	Dan Liew	2014-05-27
\| \| \| \| \| \| \| \|	spaces.
\| *	Merge	Ally Donaldson	2014-05-27
\| \|\ \| \|/ \|/\|
* \|	Convert the AbsHoudini tests to lit tests. They weren't being run by the old	Dan Liew	2014-05-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	infrastructure so I have not bothered to update the Answer file. These tests are still disabled by the lit.local.cfg file in the AbsHoudini folder because the following tests fail or weren't even being run previously (these are left unresolved because I do not know how these tests are meant to be run) UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32) UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32) UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32) UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32) FAIL: Boogie :: AbsHoudini/quant3.bpl (22 of 32) FAIL: Boogie :: AbsHoudini/quant5.bpl (28 of 32)
* \|	Added simple python implementation of diff to replace using the	Dan Liew	2014-05-27
\|/ \| \| \| \|	``fc`` tool on windows because it is buggy when tests are run concurrently.
*	Implemented an additional type check for assumption variables.	wuestholz	2014-05-27
\|
*	Added more tests (snapshots).	wuestholz	2014-05-27
\|
*	Set the following tests to expected failure under lit. Having these	Dan Liew	2014-05-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reported is unnecessary noise right now. Someone needs to fix these tests but I'm not the author. Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl Boogie :: test21/Maps2.bpl Boogie :: test21/test3_AddMethod_conv.bpl
*	Remove solver executable check under windows at the request	Dan Liew	2014-05-12
\| \| \| \| \|	of Valentin Wüstholz because under Windows Boogie looks in other locations for Z3.
*	Converted test0/Arrays1.bpl test to OutputCheck style test.	Dan Liew	2014-05-12
\|
*	Convert houd12.bpl into a OutputCheck style test and also pass	Dan Liew	2014-05-12
\| \| \| \|	--dump-file-to-check flag to OutputCheck by default to ease debugging