debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	cleaned up some names	Shaz Qadeer	2015-09-28
\|
*	added introduced and ghost local variables	Shaz Qadeer	2015-09-25
\|
*	modified desugaring so that in commutatitivity checks copies of original	qadeer	2015-06-17
\| \| \| \|	codeexpr is made.
*	added assume about gate after calls and parallel calls	qadeer	2015-05-31
\|
*	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
*	some refactoring to separate the concept of shared variables under ↵	qadeer	2014-12-17
\| \| \| \|	refinement checking with all global variables
*	systematic renaming of phase to layer	qadeer	2014-12-15
\|
*	renamed :phase to :layer	qadeer	2014-11-14
\|
*	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 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
*	simplified yield type chcking and added treiber stack (not fully done)	qadeer	2014-07-15
\|
*	various fixes	qadeer	2014-06-02
\|
*	a bug fix	qadeer	2014-05-07
\|
*	third checkpoint (refactored more code)	qadeer	2014-05-05
\|
*	second checkpoint	qadeer	2014-05-04
\|
*	checkpoint	qadeer	2014-05-03
\|
*	updated the mover checks	qadeer	2014-04-25
\|
*	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
\|
*	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
\|
*	added ReadOnlyStandardVisitor	qadeer	2014-02-24
\| \| \| \|	made the default phase of assertions be 0
*	Added /trustPhasesDownto option	qadeer	2014-02-24
\|
*	Added /trustPhasesUpto option	qadeer	2014-02-23
\|
*	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
*	various bug fixes	qadeer	2014-01-21
\| \| \| \|	added "cnst" feature
*	bug fix in handling of parallel call	qadeer	2014-01-20
\|
*	fix for a completeness bug (reported by Serdar) in refinement checker	qadeer	2014-01-16
\|
*	added more information to assert messages	qadeer	2014-01-14
\|
*	a bug fix	qadeer	2014-01-13
\|
*	a fix regarding the checking of assertions in atomic specs at call sites	qadeer	2014-01-08
\|
*	first cut of refinement checking	qadeer	2014-01-07
\|
*	Fixed a bug regarding the treatment of old() in stable procedures. The ↵	qadeer	2013-12-26
\| \| \| \| \| \| \|	implementation of the stable procedure interprets old() as the state at the beginning of the procedure's execution but the caller of the procedure interprets old() as the state just before the call. The fix bridges the mismatch between these two interpretations.
*	more bug fixes	qadeer	2013-12-24
\| \| \| \|	updates to DeviceCache.bpl to make it verify
*	more bug fixes	qadeer	2013-12-22
\|
*	bug fixes in Duplicate.cs and parsing of invariant attributes	qadeer	2013-12-22
\| \| \| \|	other bug fixes in QED stuff
*	more refactoring of the concurrency stuff	qadeer	2013-12-20
\|
*	various updates and tighter integration of QED stuff into mainline	qadeer	2013-12-19
\|
*	added syntax for par call and ParCallCmd	qadeer	2013-12-16
\|
*	some refactoring of QED stuff	qadeer	2013-12-10
\|
*	various updates	qadeer	2013-12-09
\|