debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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!
* \|	Merge	qadeer	2011-08-04
\|\ \
* \| \|	full port of houdini project	qadeer	2011-08-04
\| \| \|
\| \| *	Merge	t-espave	2011-08-04
\| \| \|\ \| \| \|/ \| \|/\|
\| \| *	(phone bct) monitoring pivot controls	t-espave	2011-08-04
\| \| \|
\| * \|	Chalice: Add comment to a broken test-case.	stefanheule	2011-08-04
\| \| \|
\| * \|	Chalie: Fix Visual Studio integration and add note about JVM stack size ↵	stefanheule	2011-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	problems.
* \| \|	Merge	qadeer	2011-08-03
\|\\| \|
* \| \|	ported Houdini to C#, added Houdini project to the Boogie solution	qadeer	2011-08-03
\| \| \|
\| * \|	Merge	Aleksandar Milicevic	2011-08-03
\| \|\ \
\| * \| \|	Jennisys:	Aleksandar Milicevic	2011-08-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- moved modularization and method unification stuff to their own modules - improved the modular synthesis so that whole branches can be delegated to existing methods.
\| \| \| *	(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
\| \| *	Merge	t-espave	2011-08-03
\| \| \|\
\| \| * \|	typo	t-espave	2011-08-03
\| \| \| \|
\| \| \| *	Chalice: Add regression tests for all fixed bugs and separate the tests in ↵	stefanheule	2011-08-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	'examples' into "read" examples and general tests.
\| \| \| *	Chalice: only show warning about misleading smoke warnings if there are ↵	stefanheule	2011-08-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	actually smoke warnings.
\| \| \| *	Chalice: Improve command line interface. Unknown options are no longer ↵	stefanheule	2011-08-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	silently passed to Boogie (but passing them to Boogie is still possible with /boogieOpt), and Chalice shows a message when it expects input from stdin.
\| \| \| *	Chalice VS integration: recognize string literals	Rustan Leino	2011-08-03
\| \| \|/ \| \|/\|
\| * \|	Merge	Aleksandar Milicevic	2011-08-02
\| \|\\|
\| * \|	Jennisys: implemented a unification algorithm that tries to find an existing	Aleksandar Milicevic	2011-08-02
\| \| \| \| \| \| \| \| \| \| \| \|	method that matches (specification-wise) a synthesized one
\| \| *	(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
\| \|/ \|/\|
* \|	Chalice: Add sbt to the repository.	stefanheule	2011-08-02
\| \|
* \|	Chalice: Chalice is now built using sbt (simple built tool).	stefanheule	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
\|/ /
* \|	Merge	t-espave	2011-08-01
\|\\|
* \|	fix for exception when phoneControls are not set	t-espave	2011-08-01
\| \|
\| *	Merge	Aleksandar Milicevic	2011-07-29
\| \|\ \| \|/ \|/\|
\| *	Jennisys: (1) fixed a bug in "TryInferConditionals"; (2) added synthesized ↵	Aleksandar Milicevic	2011-07-29
\| \| \| \| \| \| \| \|	modular code
\| *	Jennisys:	Aleksandar Milicevic	2011-07-29
\| \| \| \| \| \| \| \| \| \| \| \|	- finished the initial version of the modular code for constructors (excluding the unification part where it tries to find an existing function that meets the required spec)
* \|	more phone controls tracked for feedback	t-espave	2011-07-29
\| \|
* \|	anonymous phone controls fix	t-espave	2011-07-29
\| \|
* \|	Merge	t-espave	2011-07-28
\|\ \
* \| \|	more input/output control handling for phones	t-espave	2011-07-28
\| \| \|
\| * \|	release build should not have z3api being built	Unknown	2011-07-28
\| \| \|