debian-boogie - Debian packaging for Boogie

	Commit message (Expand)	Author	Age
*	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
*	Chalice: only one if conditional, as we want if-elseif-elseif behaviour, and ...	stefanheule	2012-02-25
*	Chalice: do not use a exhaleheap when recursing	stefanheule	2012-02-25
*	Chalice: add code to update secondary mask based on the folded predicates	stefanheule	2012-02-25
*	Chalice: introduce BoogieExpr to allow boogie expressions in the Chalice AST	stefanheule	2012-02-25
*	Chalice: begging of a method UpdateSecMask that decrements (recursively) the ...	stefanheule	2012-02-25
*	Chalice: start using FoldedPredicatesInfo and change exhale to transfer permi...	stefanheule	2012-02-25
*	Chalice: index error	stefanheule	2012-02-25
*	Chalice: start to integrate FoldedPredicatesInfo into etran	stefanheule	2012-02-25
*	Chalice: helper method resetState and more refactorings.	stefanheule	2012-02-25
*	Chalice: more abstraction with a case class Globals.	stefanheule	2012-02-25
*	Chalice: first part of the refactoring for better handling of globals	stefanheule	2012-02-25
*	Chalice: add classes to track predicate information	stefanheule	2012-02-25
*	Chalice: correct axiom for limited functions (use 2nd mask)	stefanheule	2012-02-25
*	Chalice: do not use inhalefrom anymore for predicates (and thus remove inhale...	stefanheule	2012-02-25
*	Chalice: unneeded type parameter to quantifier	stefanheule	2012-02-25
*	Chalice: missing updates to SecMask	stefanheule	2012-02-25
*	Chalice: preserve some information about versions to predicates for which we ...	stefanheule	2012-02-25
*	Chalice: translate the precondition of functions (with permissions) correctly	stefanheule	2012-02-25
*	Chalice: do not use exhalehelper externally	stefanheule	2012-02-25
*	Chalice: rename exhale to exhalehelper and place one comment at a better place.	stefanheule	2012-02-25
*	Chalice: update the predicates version only when we lose complete access to t...	stefanheule	2012-02-25
*	Chalice: add SecMask to "wf" and as a parameter to the (Boogie) function for ...	stefanheule	2012-02-25
*	Chalice: (comment about translatePrecondition)	stefanheule	2012-02-25
*	Chalice: update definition of CanRead to account for the secondary permission...	stefanheule	2012-02-25
*	Chalice: assume IsGoodMask also for SecMask	stefanheule	2012-02-25
*	Chalice: introducing the secondary map (not using it yet)	stefanheule	2012-02-25
*	Chalice: guard the defining axiom for functions by their precondition	stefanheule	2012-02-25
*	Chalice: update framing axiom for preconditions with AccessSeq (only renaming...	stefanheule	2012-02-25
*	Chalice: change definition of combine and replace nostate by heapFragment and...	stefanheule	2012-02-25