debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	Rustan Leino	2011-08-18
\|\
* \|	Dafny: fixed bug in looking at the arguments of the :induction attribute	Rustan Leino	2011-08-18
\| \|
\| *	Merge	mschwerhoff	2011-08-18
\| \|\
\| * \|	Chalice: Added a script gathering all files necessary and/or of interest for ↵	mschwerhoff	2011-08-18
\| \| \| \| \| \| \| \| \| \| \| \|	a Chalice release.
\| \| *	fix in event translation for whole program analysis	qadeer	2011-08-17
\| \| \|
\| \| *	Merge	qadeer	2011-08-17
\| \| \|\
\| \| * \|	added RealModulus	qadeer	2011-08-17
\| \| \| \|
\| \| \| *	Merge	t-espave	2011-08-17
\| \| \| \|\ \| \| \| \|/ \| \| \|/\|
\| \| \| *	(phone) documentation	t-espave	2011-08-17
\| \| \| \|
\| \| * \|	Merge	qadeer	2011-08-17
\| \| \|\ \
\| \| * \| \|	minor refactoring	qadeer	2011-08-17
\| \| \| \| \|
\| \| * \| \|	deleted lazyinlining option 2 and 3	qadeer	2011-08-17
\| \| \| \|/ \| \| \|/\| \| \| \| \| \| \| \| \|	fixed proc copy bounding
\| \| \| *	Merge	Aleksandar Milicevic	2011-08-16
\| \| \| \|\ \| \| \| \|/ \| \| \|/\|
\| \| \| *	Jennisys:	Aleksandar Milicevic	2011-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- changed the way candidate conditions are discovered; now it simply uses all sub-expressions found in the spec that evaluate to TrueLiteral - changed the implementation so that when trying to infer a precondition, try out several different possibilities (and see which one works) - added some very basic (and incomplete) type inference - fixed a bug in the Modularizer (it didn't fix the solution after trying out the spec infered from the solution) - fixed a bug in DafnyModelUtils so that now when reading from the boogie model file it keeps getting information from Seq# functions until reaching a fixpoint (that's needed because the order or reads is important)
\| \| * \|	(bct) skeleton of plugin infrastructure. for now the code is essentially the ↵	t-espave	2011-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	same I will open a plugin branch to make more deeper changes until everything is stable
\| \| * \|	Merge	t-espave	2011-08-16
\| \| \|\ \
\| \| * \| \|	(phone) fixed problem with unknown type anonymous controls	t-espave	2011-08-16
\| \| \| \| \|
\| \| \| * \|	Merge	Michal Moskal	2011-08-16
\| \| \| \|\ \ \| \| \| \|/ / \| \| \|/\| \|
\| \| * \| \|	Merge	t-espave	2011-08-16
\| \| \|\ \ \
\| \| * \| \| \|	saving navigation bad smells report	t-espave	2011-08-16
\| \| \| \| \| \|
\| \| \| * \| \|	Made the split fields heap agree with the naming convention used for fields that	Mike Barnett	2011-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the general heap uses. Updated regressions.
\| \| \| * \| \|	Chalice build succeeded, 58 test(s) failed	CodeplexBot	2011-08-16
\| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Merge	mschwerhoff	2011-08-16
\| \|\ \ \ \
\| \| \| \| \| *	Merge	Aleksandar Milicevic	2011-08-15
\| \| \| \| \| \|\ \| \| \| \|_\|_\|/ \| \| \|/\| \| \|
\| \| \| \| \| *	Jennisys:	Aleksandar Milicevic	2011-08-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- added concreteValues field to HeapInstance - brought back reading from Seq#Build when restoring Boogie models - changed the how the candidate conditions are inferred: now it only looks for unmodifiable concrete fields - method in parameter values are added to the list of potential candidate conditions
\| \| \| * \| \|	(BCT) starting translators-as-plugins impl	t-espave	2011-08-15
\| \| \|/ / /
\| \| * \| \|	Better message when an error happens.	Mike Barnett	2011-08-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	AssertionInjector: Check for invalid source locations (FeeFee) so they don't confuse the injection.
\| \| * \| \|	cleaning up & refactor	t-espave	2011-08-15
\| \| \| \|/ \| \| \|/\|
\| * / \|	Chalice: Changed tests/runalltests.bat such that additional parameters can ↵	mschwerhoff	2011-08-15
\| \|/ / \| \| \| \| \| \| \| \| \|	be passed to Chalice
\| * \|	Jennisys:	Aleksandar Milicevic	2011-08-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- changed the synthesis of the Valid() function to synthesize both unrolled and recursive definition of it, because both are needed in certain cases - to make the recursive definition of Valid() work, a "decreases" clause is needed. For now, decreases clause is always "decreases Repr", and that seems to be enough for now.
\| * \|	Jennisys: added some more infrastructure for synthesizing read only methods, so	Aleksandar Milicevic	2011-08-13
\| \| \| \| \| \| \| \| \| \| \| \|	that now a simple example like Node.Tail work.
\| * \|	Merge	Aleksandar Milicevic	2011-08-12
\| \|\ \
\| * \| \|	Jennisys:	Aleksandar Milicevic	2011-08-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- added "modifiable objects" to heap instance - when verifying synthesized program, only fields of the modifiable objects are considered
\| \| * \|	workaround corral bug (cannot handle parallel assignments)	qadeer	2011-08-12
\| \| \| \|
\| \| * \|	Merge	qadeer	2011-08-12
\| \| \|\ \
\| \| * \| \|	various fixes to deal with bug in generic delegates	qadeer	2011-08-12
\| \| \| \| \|
\| \| \| * \|	Chalice: Disallow credit expressions in the specification of functions.	stefanheule	2011-08-12
\| \| \| \| \|
\| \| * \| \|	Merge	qadeer	2011-08-11
\| \| \|\ \ \
\| \| * \| \| \|	fixes for bug with generic delegates	qadeer	2011-08-11
\| \| \| \| \| \|
\| \| \| \| * \|	Dafny: Fixed a bug in the printer that led to a stack overflow.	wuestholz	2011-08-11
\| \| \| \|/ /
\| \| \| * \|	Merge	t-espave	2011-08-11
\| \| \| \|\ \
\| \| \| * \| \|	(phone) cancel/navigation on back key is now deep through calls. More info ↵	t-espave	2011-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reported at end of analysis
\| \| \| \| * \|	Fixed problem where events in stubs were generating duplicate declarations.	Mike Barnett	2011-08-11
\| \| \| \| \| \|
\| \| \| \| * \|	Added references to the AssertionInjector project so it can build again.	Mike Barnett	2011-08-11
\| \| \| \|/ /
\| \| \| * \|	Merge	t-espave	2011-08-11
\| \| \| \|\ \
\| \| \| * \| \|	(BCT) BREAKING CHANGE	t-espave	2011-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox
\| \| \| \| * \|	Boogie build succeeded	CodeplexBot	2011-08-11
\| \| \|_\|/ / \| \|/\| \| \|
\| * \| \| \|	Merge	Aleksandar Milicevic	2011-08-10
\| \|\\| \| \|
\| * \| \| \|	Jennisys: started to work on synthesizing some methods. So far, only	Aleksandar Milicevic	2011-08-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	infrastructural things have been implemented, like handling return parameters, generating different "fresh" spec for methods than for constructors, adding "Valid()" to method preconditions.
\| \| \| * \|	(phone) fixed issues with anonymous xaml declarations.	t-espave	2011-08-10
\| \| \|/ /