debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Jennisys: changed the Combiner method to produce more	Aleksandar Milicevic	2011-08-22
\| \| \| \|	combinations, so now List.Find works
*	Merge	Aleksandar Milicevic	2011-08-22
\|\
* \|	Jennisys:	Aleksandar Milicevic	2011-08-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- worked on some additional list examples - added expression simplification function - added "decreases Repr" for recursive methods - added desugaring when printing out method calls to Dafny
\| *	Use SMT2 syntax for sign_extend	Michal Moskal	2011-08-22
\| \|
\| *	Merge	t-espave	2011-08-22
\| \|\ \| \|/ \|/\|
\| *	(phone bct) boolean binding of control enabledness ignored (for now)	t-espave	2011-08-22
\| \| \| \| \| \| \| \|	tracking Page virtual overrides
* \|	Merge	Aleksandar Milicevic	2011-08-21
\|\ \
* \| \|	jennisys: got the List.Get example to work. List.Tail also works. Others ↵	Aleksandar Milicevic	2011-08-21
\| \| \| \| \| \| \| \| \| \| \| \|	should follow soon
\| * \|	reverting irreducible handling temporarily	qadeer	2011-08-21
\| \|\ \
\| * \ \	Merge	qadeer	2011-08-20
\| \|\ \ \ \| \|/ / / \|/\| \| \|
\| * \| \|	added code to handle irreducible graphs	qadeer	2011-08-20
\| \| \| \|
* \| \| \|	Merge	Aleksandar Milicevic	2011-08-20
\|\ \ \ \
* \| \| \| \|	Jennisys: added some more infrastructure for synthesizing read only methods	Aleksandar Milicevic	2011-08-20
\| \| \| \| \|
\| \| \| \| *	(phone bct) minor bugfixes found playing around with apps	t-espave	2011-08-19
\| \| \| \| \|
\| \| \| \| *	Merge	t-espave	2011-08-19
\| \| \| \| \|\ \| \| \|_\|_\|/ \| \|/\| \| \|
\| \| \| \| *	continuned phone bct docs	t-espave	2011-08-19
\| \| \| \| \|
\| * \| \| \|	Chalice build succeeded	CodeplexBot	2011-08-19
\| \| \| \| \|
\| * \| \| \|	Tagging EMIC CC.NET build 2.1.30819.0	VccBuildServer	2011-08-19
\| \| \|_\|/ \| \|/\| \|
\| * \| \|	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
\|\ \ \ \