debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	phone nav building "doc"	t-espave	2011-08-09
\|
*	(phone) fully automated phone nav graph building	t-espave	2011-08-09
\|
*	Merge	t-espave	2011-08-08
\|\
* \|	(phone bct) filtering out nonpages for boogie queries, faster but maybe a ↵	t-espave	2011-08-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	less precise preparing boogie code for static unrolls filtering out some navigations
\| *	another bug fix in bct	qadeer	2011-08-08
\| \|
\| *	added a new file and fixed a bug in bct	qadeer	2011-08-08
\|/
*	Added option "getMeHere" so that calls to GetMeHere.Assert(e) become "assert e"	Mike Barnett	2011-08-06
\| \| \| \| \| \| \|	(which really could be done just by defining it that way in an assembly either via a contract or else by inlining it). But more importantly the option causes all assertions to be translated as assumptions. Still to do: postconditions should be translated as "free ensures".
*	fixed a bug in delegate dispatcher name for generic invoke methods	qadeer	2011-08-05
\|
*	(phone bct) nav graph building (mostly) automated	t-espave	2011-08-05
\|
*	(phone bct) nav graph building (mostly) automated	t-espave	2011-08-05
\|
*	Merge	Mike Barnett	2011-08-04
\|\
* \|	Added new option /captureState (/c) for generating a capture state assumption	Mike Barnett	2011-08-04
\| \| \| \| \| \| \| \|	after each statement.
\| *	Merge	t-espave	2011-08-04
\| \|\ \| \|/ \|/\|
\| *	(phone bct) anonymous control support	t-espave	2011-08-04
\| \| \| \| \| \| \| \| \| \|	boogie nav graph modular analysis code default uris to lowercase to make life easier
* \|	Changed name mangling (again) to avoid name clashes.	Mike Barnett	2011-08-04
\| \| \| \| \| \| \| \|	If a method's parameters don't have names, give them names!
\| *	(phone bct) monitoring pivot controls	t-espave	2011-08-04
\| \|
\| *	(phone bct) moved some code to urihelper	t-espave	2011-08-03
\| \|
\| *	Merge	t-espave	2011-08-03
\| \|\ \| \|/ \|/\|
* \|	Increase the name mangling to avoid name clashes in the Boogie program. In IL,	Mike Barnett	2011-08-03
\| \| \| \| \| \| \| \|	members of a type can have the same name.
\| *	(phone bct) user feedback, showing possibly anomalous nav targets	t-espave	2011-08-03
\|/ \| \| \|	(bct) '+' invalid in string literals
*	typo	t-espave	2011-08-03
\|
*	(phone bct) tracking targets of back key navs.	t-espave	2011-08-02
\|
*	Merge	t-espave	2011-08-02
\|\
* \|	(phone bct) default URI checks inlined	t-espave	2011-08-02
\| \| \| \| \| \| \| \|	inlining statistics
\| *	Unicode surrogate characters cannot be handled by Boogie. For now (forever?)	Mike Barnett	2011-08-02
\| \| \| \| \| \| \| \|	just delete them from the identifier that represents each literal string.
* \|	(phone bct) methods inlined for modular analysis (fix)	t-espave	2011-08-02
\|/
*	further fixes in the translation of compiletime constants	qadeer	2011-08-01
\|
*	Merge	t-espave	2011-08-01
\|\
* \|	(phone bct) compute fixpoint for necessary inlined methods (for modular ↵	t-espave	2011-08-01
\| \| \| \| \| \| \| \|	analysis)
* \|	control parsing creates batch file with several calls to corral for graph ↵	t-espave	2011-08-01
\| \| \| \| \| \| \| \|	building. lacks some automation still
\| *	Fix in the assertion injector for putting the output on top of the input	Mike Barnett	2011-08-01
\| \| \| \| \| \| \| \| \| \| \| \|	assembly. Fix in the Sink so that the consolidated index of a type parameter is computed correctly.
* \|	generating individual corral queries for page navigation	t-espave	2011-08-01
\|/
*	fix for exception when phoneControls are not set	t-espave	2011-08-01
\|
*	more phone controls tracked for feedback	t-espave	2011-07-29
\|
*	anonymous phone controls fix	t-espave	2011-07-29
\|
*	more input/output control handling for phones	t-espave	2011-07-28
\|
*	refactored phonehelper	t-espave	2011-07-28
\|
*	trivial contract for phone event handlers	t-espave	2011-07-28
\|
*	bugfix,nothing was done if no white/blacklist specified	t-espave	2011-07-28
\|
*	option bugfix	t-espave	2011-07-28
\|
*	Merge	Mike Barnett	2011-07-27
\|\
* \|	New project to support "Get Me Here": an assertion injector that puts into a	Mike Barnett	2011-07-27
\| \| \| \| \| \| \| \|	binary a call to "Contract.Assert(false)".
* \|	Implemented a whitelist/blacklist so translator can ignore certain parts of an	Mike Barnett	2011-07-27
\| \| \| \| \| \| \| \|	assembly.
\| *	fixed right/left shift functions decl	t-espave	2011-07-27
\| \|
\| *	solved uri naming issues	t-espave	2011-07-27
\| \|
\| *	not handling property bindings for controls (for now)	t-espave	2011-07-27
\| \|
\| *	Merge	t-espave	2011-07-27
\| \|\ \| \|/ \|/\|
\| *	- handler methods with simulated calls	t-espave	2011-07-27
\| \| \| \| \| \| \| \|	- easy checks on backstack navigation that may make graph innecessary
* \|	Updated regressions.	Mike Barnett	2011-07-27
\| \|
* \|	fixed bug in constant translation	qadeer	2011-07-27
\|/