debian-boogie - Debian packaging for Boogie

	Commit message (Expand)	Author	Age
...
\| *	Chalice: Test case for negative permission in the secondary mask.	stefanheule	2012-02-25
\| *	Chalice: Add testcase for mutually recursive predicates (failed before the la...	stefanheule	2012-02-25
\| *	Chalice: Fix the recursion bound for updating the secondary mask.	stefanheule	2012-02-25
\| *	Chalice: Fix the triggering mechanism once again.	stefanheule	2012-02-25
\| *	Chalice: Fix trigger problem (wrongly used limited function as trigger, inste...	stefanheule	2012-02-25
\| *	Chalice: Add function trigger for unfold and unfolding.	stefanheule	2012-02-25
\| *	Chalice: Code cleanup.	stefanheule	2012-02-25
\| *	Chalice: Change the Chalice function triggering mechanism to use a function p...	stefanheule	2012-02-25
\| *	Chalice: Do not remove permission from the secondary mask during the exhale t...	stefanheule	2012-02-25
\| *	Chalice: Change the Boogie encoding of Chalice functions to only depend on th...	stefanheule	2012-02-25
\| *	Chalice: Correct axioms with new trigger mechanism (with trigger f we have f ...	stefanheule	2012-02-25
\| *	Chalice: Change trigger function to only take a single argument.	stefanheule	2012-02-25
\| *	Chalice: Add trigger to 'limited axiom' instead of the definining axiom.	stefanheule	2012-02-25
\| *	Chalice: use canread instead of canreadforsure in function axiom	stefanheule	2012-02-25
\| *	Chalice: add axiom relating different triggers.	stefanheule	2012-02-25
\| *	Chalice: partly solve problem with triggers and quantified variables	stefanheule	2012-02-25
\| *	Chalice: first try at triggers for functions	stefanheule	2012-02-25
\| *	Chalice: update reference output of AssocitationList (to remove bogus fail)	stefanheule	2012-02-25
\| *	Chalice: update reference output to new error messages.	stefanheule	2012-02-25
\| *	Chalice: add missing well-formedness assumption.	stefanheule	2012-02-25
\| *	Chalice: Backed out changeset: a0fdb50e36b44bc939eb44e940b90975ffeaa781	stefanheule	2012-02-25
\| *	Chalice: the secondary mask was not saved using CallSecMask at a fork	stefanheule	2012-02-25
\| *	Chalice: use correct mask and secmask in translation during exhale	stefanheule	2012-02-25
\| *	Chalice: missing well-formedness assumption	stefanheule	2012-02-25
\| *	Chalice: another invalid use of etran instead of this	stefanheule	2012-02-25
\| *	Chalice: using this instead of etran inside of the ExpressionTranslator itsel...	stefanheule	2012-02-25
\| *	Chalice: no havoc during unfolding expressions	stefanheule	2012-02-25
\| *	Chalice: remove assertion that we have enought permission when updating the s...	stefanheule	2012-02-25
\| *	Chalice: Remove assumption IsGoodMask when updating the secondary mask.	stefanheule	2012-02-25
\| *	Chalice: do not assume IsGoodMask(sm)	stefanheule	2012-02-25
\| *	Chalice: ordering of picking a new version and checking against	stefanheule	2012-02-25
\| *	Chalice: Change position where we record the version and receiver of a predic...	stefanheule	2012-02-25
\| *	Chalice: reset auxilary information for while loops	stefanheule	2012-02-25
\| *	Chalice: add conditional variables to auxilary information	stefanheule	2012-02-25
\| *	Chalice: do not havoc during unfold's exhale	stefanheule	2012-02-25
\| *	Chalice: Backed out changeset: 5724b933941338bebb239272f6c90da6f3415f08	stefanheule	2012-02-25
\| *	Chalice: change order of unfold treatment; first inhale predicate body, then ...	stefanheule	2012-02-25
\| *	Chalice: reset state of predicate information after definedness check	stefanheule	2012-02-25
\| *	Chalice: more to handle unfolding	stefanheule	2012-02-25
\| *	Chalice: start to handle unfolding	stefanheule	2012-02-25
\| *	Chalice: reset currentConditions in fpi.reset	stefanheule	2012-02-25
\| *	Chalice: Backed out changeset: ae8ad67b7ed3 (invalid attempt to account for u...	stefanheule	2012-02-25
\| *	Chalice: remove stack dump	stefanheule	2012-02-25
\| *	Chalice: change location of stack trace dump.	stefanheule	2012-02-25
\| *	Chalice: first try for unfolding	stefanheule	2012-02-25
\| *	Chalice: add assumption that receivers of nested predicates are different	stefanheule	2012-02-25
\| *	Chalice: the folded predicate should only be recorded when the exhale for the...	stefanheule	2012-02-25
\| *	Chalice: correctly introduce a temporary secondary mask	stefanheule	2012-02-25
\| *	Chalice: include an exhale mask again for exhale	stefanheule	2012-02-25
\| *	Chalice: better bound on recursion for predicates	stefanheule	2012-02-25