debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Enabled "HAVOC-generated bpl files" lit tests.	Dan Liew	2014-05-07
\|
*	Enabled "Extract loops benchmarks" lit tests.	Dan Liew	2014-05-07
\|
*	Enabled the "Stratified inlining benchmarks" lit tests.	Dan Liew	2014-05-07
\| \| \| \| \| \| \| \| \| \|	The following tests will probably fail for newer versions of Z3 (e.g. 4.3) stratifiedinline/bar10.bpl stratifiedinline/bar7.bpl stratifiedinline/bar8.bpl stratifiedinline/bar9.bpl
*	Added "STORM benchmarks for testing correctness of live variable analysis" ↵	Dan Liew	2014-05-07
\| \| \| \|	lit tests.
*	Enabled generalizedarray lit test.	Dan Liew	2014-05-07
\|
*	Enabled datatypes lit tests.	Dan Liew	2014-05-07
\|
*	Enabled prover lit tests.	Dan Liew	2014-05-07
\|
*	Enable codeexpr lit tests.	Dan Liew	2014-05-07
\|
*	Enabled lit loop unrolling test	Dan Liew	2014-05-07
\|
*	Enabled smoke lit test.	Dan Liew	2014-05-07
\|
*	Enabled bitvector lit tests.	Dan Liew	2014-05-07
\|
*	Enabled "Benchmarks for error messages" lit tests.	Dan Liew	2014-05-07
\| \| \| \| \| \|	The test15/CaptureState.bpl test fails on Linux using (Z3 4.2) due to additional (but not meaningful) parentheses in the outputted model.
*	Enabled the inline lit tests. In order to support expansion2.bpl	Dan Liew	2014-05-07
\| \| \| \| \| \|	we now require the OutputCheck tool. The lit.site.cfg file has been taught to require that this tool is in the user's PATH before testing starts.
*	Enable "error messages for failing asserts vs. loop invariants" lit tests.	Dan Liew	2014-05-07
\|
*	Enable "SLAM example" lit tests.	Dan Liew	2014-05-07
\|
*	Enable "abstract domain of intervals" lit tests.	Dan Liew	2014-05-07
\|
*	Enable Linear inequality lit tests.	Dan Liew	2014-05-07
\|
*	For lit test infrastructure, disable running tests in	Dan Liew	2014-05-07
\| \| \| \| \| \| \| \|	AbsHoudini/ test17/ z3api/ because the alltests.txt claims they are "Postponed"
*	Enable the Constant propagation tests as lit tests.	Dan Liew	2014-05-07
\|
*	Enabled "Verify Boogie 2" lit tests. Note the following tests fail	Dan Liew	2014-05-07
\| \| \| \| \| \| \| \|	because they were never properly tested in the the old testing infrastructure. test21/Maps2.bpl test21/test3_AddMethod_conv.bpl
*	Enabled tests for types introduced in Boogie2 as lit tests.	Dan Liew	2014-05-07
\|
*	Enable the VCVariety.BlockNested tests as lit tests.	Dan Liew	2014-05-07
\|
*	Enabled VC Generation lit tests.	Dan Liew	2014-05-07
\|
*	For lit tests running on Windows pass /W flag to the fc tool	Dan Liew	2014-05-06
\| \| \| \| \| \| \|	so that all whitespace (including mismatching line endings due to DOS vs UNIX) are ignored. This fixes the test1/Arrays.bpl test under Windows. It's quite suprising this issue didn't come up earlier.
*	Enabled lit tests for test1/ directory	Dan Liew	2014-05-06
\| \| \| \|	Bizarely Array.bpl does not pass on Windows. This will be fixed soon.
*	Enabled most of the name resolution lit tests. They don't all pass	Dan Liew	2014-05-05
\| \| \| \|	yet due to a bug in -useBaseNameForFileName.
*	Converted textbook tests to lit tests.	Dan Liew	2014-04-08
\|
*	Add lit.local.cfg that instructs not to run any tests in this	Dan Liew	2014-05-05
\| \| \| \| \| \| \|	directory or its subdirectories. The test in this directory is pointless because we will run it later on anyway! When we migrate to lit this test directory should be removed
*	Pass -useBaseNameForFileName option to Boogie when running tests.	Dan Liew	2014-04-06
\| \| \| \| \| \| \| \| \|	This is needed because the expected test output contains just the basename of the .bpl files in error messages but lit passes an absolute path to Boogie so without this option error messages would contain absolute paths which would cause the tests to fail. Now all the houdini tests pass when driven by lit.
*	Enable houdini lit tests. Note some still fail due to Boogie	Dan Liew	2014-05-05
\| \| \| \|	outputing absolute paths to .bpl files in error messages
*	Added basic lit configuration file for running tests.	Dan Liew	2014-04-06
\|
*	minor fix	qadeer	2014-05-05
\|
*	example for variable introduction added	qadeer	2014-05-04
\|
*	second checkpoint	qadeer	2014-05-04
\|
*	checkpoint	qadeer	2014-05-03
\|
*	updated the mover checks	qadeer	2014-04-25
\|
*	Add support for assumption variables.	wuestholz	2014-04-21
\|
*	added another sample	qadeer	2014-04-20
\|
*	added simulation relation computation to yield type checking	qadeer	2014-04-20
\| \| \| \|	updated the type check to incorporate {:terminates} annotation
*	added the framing for the refinement check	qadeer	2014-04-16
\|
*	Merge	qadeer	2014-04-16
\|\
* \|	added variable hiding	qadeer	2014-04-16
\| \| \| \| \| \| \| \|	added annotation on an atomic action about the phases in which it exists
\| *	disabled quantifier merging, except when no triggers are provided (as ↵	Unknown	2014-03-03
\|/ \| \| \|	discussed with Rustan)
*	Fixed abstract interpretation for reals	Rustan Leino	2014-04-13
\|
*	Fixed bug in abstract interpretation over reals	Rustan Leino	2014-04-08
\|
*	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 ReadOnlyStandardVisitor	qadeer	2014-02-24
\| \| \| \|	made the default phase of assertions be 0
*	fixed a bug in desugaring of linear variables	qadeer	2014-02-20
\|
*	forgot to update the Answer file earlier	qadeer	2014-02-12
\|
*	fixed the civl-paper example	qadeer	2014-02-12
\|