debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Enable snapshot test. This test is unusual in that it doesn't	Dan Liew	2014-05-07
\| \| \| \| \| \|	use .bpl files in the directory directy on the command line. So instead will tell lit to look for *.snapshot files and provide one that runs the commands we want in the right directory.
*	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.
*	Teach the ExecutionEngine to respect the -useBaseNameForFileName commandline	Dan Liew	2014-04-09
\| \| \| \|	option when reporting the number of errors.
*	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.
*	Added /useBaseNameForFile command line argument. The Scanner	Dan Liew	2014-04-06
\| \| \| \| \| \| \| \| \| \| \| \| \|	and Parser constructors have been modified to take an optional argument specifying this and the ExecutionEngine passes for that value CommandLineOptions.Clo.UseBaseNameForFileName This option when true causes the basename of file to be used inside created Tokens instead of what the user passed on the command line which might be a relative or absolute path. The motivation for adding this option is that it is needed for the lit driven tests so that the output of Boogie can be reliably checked.
*	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
\|
*	a bug fix	qadeer	2014-05-07
\|
*	added {:aux} attribute to local variables	qadeer	2014-05-07
\|
*	minor fix	qadeer	2014-05-05
\|
*	third checkpoint (refactored more code)	qadeer	2014-05-05
\|
*	example for variable introduction added	qadeer	2014-05-04
\|
*	second checkpoint	qadeer	2014-05-04
\|
*	checkpoint	qadeer	2014-05-03
\|
*	bug fix in the last update	qadeer	2014-04-25
\|
*	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
*	fixed some bugs in the previous check ins	qadeer	2014-04-16
\|
*	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