debian-boogie - Debian packaging for Boogie

	Commit message (Expand)	Author	Age
*	Chalice:	kyessenov	2010-08-24
*	Chalice: exhale spec statement post condition in refinement block translation...	kyessenov	2010-08-23
*	Chalice: copy concrete values for every permission in coupling invariants of ...	kyessenov	2010-08-23
*	Chalice: refining lists doesn't quite work yet...	kyessenov	2010-08-22
*	Chalice:	kyessenov	2010-08-22
*	Chalice:	kyessenov	2010-08-21
*	VS 2010 mode for Chalice: some errors didn't show up in the window because po...	kyessenov	2010-08-20
*	Chalice:	kyessenov	2010-08-19
*	Chalice:	kyessenov	2010-08-19
*	Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ...	kyessenov	2010-08-19
*	Chalice:	kyessenov	2010-08-18
*	Chalice: refactored AST code for class hierarchy (no need for caches since Sc...	kyessenov	2010-08-17
*	Chalice: bug fixes -- "check termination" flag was not properly preserved (i....	kyessenov	2010-08-16
*	Chalice: add pre-conditions to specification statements; semantically spec st...	kyessenov	2010-08-13
*	Chalice: add specification statement ( ghost? (const\|var) (x (:T)?)+ [P(x)] )	kyessenov	2010-08-13
*	Chalice: accept many input files at once; read from stdin if no input file sp...	kyessenov	2010-08-12
*	Chalice: put classes and objects into package "chalice"	kyessenov	2010-08-11
*	Chalice: added uninterpreted functions; attempting to re-verify Celebrity in ...	kyessenov	2010-08-10
*	Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); ...	kyessenov	2010-08-06
*	Chalice:	kyessenov	2010-08-02
*	Chalice:	kyessenov	2010-08-02
*	Chalice:	kyessenov	2010-07-30
*	Chalice: pretty printer now prints element type for sequences; fixed a bug in...	kyessenov	2010-07-27
*	Chalice: bug -- permissions were implicity converted to Booge expressions (du...	kyessenov	2010-07-22
*	Chalice: bug -- expression substitution should preserve typing	kyessenov	2010-07-22
*	Chalice: sequence access wildcards a[]. and a[*].f have been implemented (s...	kyessenov	2010-07-22
*	Chalice: introduced proper AST nodes for permission expressions and permissio...	kyessenov	2010-07-21
*	Chalice: fixed typos in strings; trying out committing with TFS	kyessenov	2010-07-21
*	Chalice: added surface syntax for acc(s[].) and acc(s[*].f); extended AST, ...	kyessenov	2010-07-20
*	Chalice: fixed a bug with permission operations treating AccessAll not as a p...	kyessenov	2010-07-20
*	Chalice: added type information for sequences ("where" clauses in local varia...	kyessenov	2010-07-20
*	Chalice: adding support for sequence local variables; removed ClassType from ...	kyessenov	2010-07-20
*	Chalice: extended substitutor to handle "exists" quantifier and sequence cont...	kyessenov	2010-07-20
*	Chalice: added sequence containment surface syntax ("in" comparison operator)...	kyessenov	2010-07-19
*	Chalice: added "exists" quantifier; changed surface syntax for quantifier exp...	kyessenov	2010-07-19
*	Chalice: Re-designed lockchange on methods and loops. The lockchange clause i...	mueller	2010-07-18
*	Chalice: No longer use Mask for "held" field; instead, only use the value of...	rustanleino	2010-07-14
*	Chalice: Changed definition of waitlevel to take into account rdlock. Adapted...	mueller	2010-07-03
*	Chalice:	rustanleino	2010-06-25
*	Chalice: Applied patch #6192	mueller	2010-06-25
*	Chalice: fixed bug in the exhale of permissions (to handle negative epsilons)	mueller	2010-06-09
*	Implicitly declare as local variables undeclared variables occurring as LHS's...	rustanleino	2009-10-16
*	- where clauses are now properly type-checked	jansmans	2009-10-02
*	Implemented -noDeadlockChecks mode. With this mode, it is possible to give s...	rustanleino	2009-10-01
*	* Implemented channels	rustanleino	2009-08-16
*	Parse channels and condition variables.	rustanleino	2009-08-05
*	Initial set of files.	mikebarnett	2009-07-15