debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	added assume about gate after calls and parallel calls	qadeer	2015-05-31
\|
*	patched ghost checking	qadeer	2015-04-18
\|
*	changed aux attribute to ghost	qadeer	2015-04-18
\|
*	fixed the treatment of extern	qadeer	2015-04-17
\|
*	patched the type checker to deal with modularity	qadeer	2015-04-16
\|
*	removed "layer" attribute from the desugared program	qadeer	2015-01-16
\|
*	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
*	some refactoring to separate the concept of shared variables under ↵	qadeer	2014-12-17
\| \| \| \|	refinement checking with all global variables
*	patched last check in	qadeer	2014-12-15
\|
*	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
*	systematic renaming of phase to layer	qadeer	2014-12-15
\|
*	fixed bug due to incomplete erasure of :linear attribute	qadeer	2014-12-05
\|
*	renamed :phase to :layer	qadeer	2014-11-14
\|
*	a fix to type checking	qadeer	2014-11-09
\|
*	Merge	qadeer	2014-10-14
\|\
* \|	reversed the order of generated procedures; commutativity checks are ↵	qadeer	2014-10-14
\| \| \| \| \| \| \| \|	generated first
\| *	Fix bug in Duplicator where GotoCmd's LabelTargets and LabelNames	Dan Liew	2014-10-05
\|/ \| \| \| \| \| \| \| \| \| \|	where not updated during duplication to point to duplicated BasicBlocks. Because the lists weren't being duplicated and resolved to the new basic blocks a duplicated Implementation pointed into Blocks in the old implementation via GotoCmds. This is bad and is not the expected behaviour. Now if VisitImplementation() is called during duplication GotoCmds will be resolved to point to duplicated Blocks.
*	Did more refactoring and addressed several todos.	wuestholz	2014-09-23
\|
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	Did some refactoring.	wuestholz	2014-09-23
\|
*	deleted the free assume about gates after parallel calls	qadeer	2014-07-26
\|
*	enabled merging of yield calls	qadeer	2014-07-20
\|
*	added support for facoring out calls to yield checkers; this will help avoid ↵	qadeer	2014-07-20
\| \| \| \|	quadratic space complexity
*	updated the linear type system based on Chris' design with linear, ↵	qadeer	2014-07-15
\| \| \| \|	linear_in, linear_out
*	fixed a regression failure	qadeer	2014-07-15
\|
*	simplified yield type chcking and added treiber stack (not fully done)	qadeer	2014-07-15
\|
*	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
*	various fixes	qadeer	2014-06-02
\|
*	a small fix	qadeer	2014-05-21
\|
*	a bug fix	qadeer	2014-05-07
\|
*	added {:aux} attribute to local variables	qadeer	2014-05-07
\|
*	third checkpoint (refactored more code)	qadeer	2014-05-05
\|
*	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
\|
*	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
\|
*	added variable hiding	qadeer	2014-04-16
\| \| \| \|	added annotation on an atomic action about the phases in which it exists
*	added more types to constructed expressions	qadeer	2014-04-15
\|
*	resolved expressions created during generation of procedures for mover checks	qadeer	2014-04-14
\|
*	Added /trustNonInterference option	qadeer	2014-02-28
\|
*	added some missing attributes to desugared assertions	qadeer	2014-02-27
\|
*	added tokens to calls and requires/ensures	qadeer	2014-02-26
\|
*	fixed couple of bugs reported by Serdar	qadeer	2014-02-25
\|
*	(Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵	Rustan Leino	2014-02-24
\| \| \| \| \| \|	of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
*	added ReadOnlyStandardVisitor	qadeer	2014-02-24
\| \| \| \|	made the default phase of assertions be 0
*	Added /trustPhasesDownto option	qadeer	2014-02-24
\|