debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Recursive walking of Exprs doesn't play nice when the depth of the AST is high.	akashlal	2014-01-07
\| \| \| \| \|	Reduce depth of AST whenever possible (e.g., use a binary tree instead of a linear list of terms)
*	points on "home strecth of yield type checker" added	kuruis	2014-01-04
\|
*	Updated year in main copyright message	Rustan Leino	2014-01-03
\|
*	and another	qadeer	2014-01-03
\|
*	another small fix	qadeer	2014-01-03
\|
*	some fixes	qadeer	2014-01-03
\|
*	First rough draft of refinement checking.	stasiran	2014-01-03
\|
*	First rough draft of refinement checking.	stasiran	2014-01-03
\|
*	minor bug in traversing program fixed	kuruis	2014-01-03
\|
*	some bugs related with phases fixed	kuruis	2014-01-03
\|
*	debug pragma closed	kuruis	2014-01-02
\|
*	some fixes on devicedriver example	kuruis	2014-01-02
\|
*	Error reporting with line numbers and commands of trace is provided	kuruis	2014-01-02
\|
*	some proper yield check reporting provided	kuruis	2014-01-02
\|
*	some bugs fixed on yiledtypechecker	kuruis	2013-12-31
\|
*	made some fixes to type checking of atomic actions	qadeer	2013-12-31
\|
*	Some bugs in yieldtypesafe fixed	kuruis	2013-12-29
\|
*	yieldtypesafe and yieldreachability automatons are separated.	kuruis	2013-12-29
\| \| \| \| \|	integration of parallel call cmds done points (1 and 3) on Shaz's email are done
*	fixed vc generation so that even when builtin array functions are used,	qadeer	2013-12-28
\| \| \| \|	the program can be verified without the use of /useArrayTheory
*	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.
*	fixed a bug in mover checking; wasn't generating enough commutativity checks	qadeer	2013-12-25
\|
*	Merge	qadeer	2013-12-24
\|\
* \|	more bug fixes	qadeer	2013-12-24
\| \| \| \| \| \| \| \|	updates to DeviceCache.bpl to make it verify
\| *	Regex fixed after discussion with Shaz	kuruis	2013-12-24
\|/
*	Automata debugging done on YieldTypeChecker.	kuruis	2013-12-23
\| \| \| \|	Regex must be revisited
*	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
*	strengthened type checking w.r.t. qed vs non-qed global variables	qadeer	2013-12-21
\|
*	more refactoring of the concurrency stuff	qadeer	2013-12-20
\|
*	comparison of phase_num checks updated	kuruis	2013-12-20
\|
*	Minor Changes in YieldTypeChecker	kuruis	2013-12-19
\|
*	Merge	qadeer	2013-12-19
\|\
* \|	various updates and tighter integration of QED stuff into mainline	qadeer	2013-12-19
\| \|
\| *	Epsilon reduction per phase automaton added	kuruis	2013-12-18
\| \|
\| *	Updates on YieldTypeChecker done	kuruis	2013-12-17
\| \|
\| *	Fixed another :never_pattern bug related to nested quantifiers	Rustan Leino	2013-12-16
\| \|
\| *	Merge	Rustan Leino	2013-12-16
\| \|\ \| \|/ \|/\|
\| *	Fixed bug in never_pattern functionality. In the new design, never_pattern ↵	Rustan Leino	2013-12-16
\| \| \| \| \| \| \| \|	does not assemble any nopats from nested quantifiers/lambdas.
* \|	regenerated after updating Parser.frame	qadeer	2013-12-16
\| \|
* \|	added syntax for par call and ParCallCmd	qadeer	2013-12-16
\| \|
* \|	Merge	qadeer	2013-12-14
\|\ \
* \| \|	fixed type checking errors in QED stuff	qadeer	2013-12-14
\| \|/ \|/\|
\| *	Resolve a concurrency issue (reported by Alex Summers).	wuestholz	2013-12-12
\|/
*	fixes to type checking code	qadeer	2013-12-11
\|
*	Updates on YieldTypeCheck	kuruis	2013-12-11
\|
*	Remove some (redundant) preconditions to avoid 'ccrewrite' errors.	wuestholz	2013-12-11
\|
*	some refactoring of QED stuff	qadeer	2013-12-10
\|
*	various updates	qadeer	2013-12-09
\|
*	Merge	Ally Donaldson	2013-12-09
\|\
* \|	Small change related to CVC4 support. Patch by Pantazis Deligiannis	Ally Donaldson	2013-12-09
\| \|