debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	updated the example to include atomic specifications (sent by Suha)	qadeer	2015-03-29
\|
*	fixed crash reported by Dan.	qadeer	2015-03-02
\| \| \| \|	DoModSetAnalysis needs to run before the linear and mover type checking.
*	fix from Serdar and Suha	qadeer	2015-02-24
\|
*	moved some things around	qadeer	2015-02-11
\|
*	minor fix to the golden file	qadeer	2015-01-28
\|
*	added lit stuff at the top of the file and the golden output	qadeer	2015-01-28
\|
*	Work stealing queue (PLDI '12 Vechev et al.)	Unknown	2015-01-28
\|
*	removed unused functions and axioms to make the verification faster	qadeer	2015-01-27
\|
*	strengthened type checking	qadeer	2014-12-26
\| \| \| \| \|	cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
*	changed type checking of yield procedures so that they can only call other ↵	qadeer	2014-12-18
\| \| \| \|	yielding procedures
*	1. made variable introduction layer explicit in the test cases	qadeer	2014-12-15
\| \| \| \|	2. if a single layer is specified for a global variable, that layer is the introduction layer
*	patched an expected output	qadeer	2014-12-15
\|
*	renamed :phase to :layer	qadeer	2014-11-14
\|
*	removed a useless procedure	qadeer	2014-10-21
\|
*	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
*	updated golden outputs and removed irrelevant tests	qadeer	2014-06-02
\|
*	Removed old test infrastructure files except for	Dan Liew	2014-05-28
\| \| \| \| \| \| \| \| \|	./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
*	Fix lit test suite when running Boogie under a path that contains	Dan Liew	2014-05-27
\| \| \| \|	spaces.
*	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
*	Enable as many "og" lit tests. Several fail because they weren't	Dan Liew	2014-05-11
\| \| \| \| \| \| \| \| \| \| \| \|	being executed previously! 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
*	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
\|
*	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
\|
*	added variable hiding	qadeer	2014-04-16
\| \| \| \|	added annotation on an atomic action about the phases in which it exists
*	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
\|
*	using break statement in the inner loop instead of goto	qadeer	2014-02-11
\|
*	added another example and fixed a bug regarding initialization of pc/ok	qadeer	2014-02-07
\| \| \| \|	snapshots per loop header
*	new design for linear types + VCgen	qadeer	2014-02-07
\| \| \| \| \|	ported all the examples added the QED examples to runtest.bat
*	more cleanup	qadeer	2014-01-23
\|
*	some cleanup	qadeer	2014-01-23
\|
*	some small optimizations to mover checking	qadeer	2014-01-22
\| \| \| \|	added LookUp to multiset.bpl
*	some fixes	qadeer	2014-01-21
\|
*	various bug fixes	qadeer	2014-01-21
\| \| \| \|	added "cnst" feature
*	fixed a bug revealed subsequent to the latest fix in parallel call handling	qadeer	2014-01-20
\|
*	bug fix in handling of parallel call	qadeer	2014-01-20
\|