| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Chalice: working out mask transfers between concrete and abstract heaps -- ↵ |  kyessenov | 2010-08-24 |
| | | | | | next goal is to make this verify! | ||
| * | Chalice: | kyessenov | 2010-08-24 |
| | | | | | | * fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals * example of finding duplicate elements in a sequence using a bitset | ||
| * | Chalice: exhale spec statement post condition in refinement block ↵ | kyessenov | 2010-08-23 |
| | | | | | translation; tag global coupling assertions (bug fix) | ||
| * | Chalice: copy concrete values for every permission in coupling invariants of ↵ | kyessenov | 2010-08-23 |
| | | | | | "this" | ||
| * | Chalice: | kyessenov | 2010-08-23 |
| | | | | | | | * added celebrity example (theory of sequences is still weak to prove basic things...) * bug in Chalice: old in while loops is ignored, needs to be fixed if ever want to complete DSW example * evil input from Z3 makes subsequent refinement proofs unsound; need to debug before building upon DSW.chalice; the error is triggered when adding parent field to Node | ||
| * | Chalice: spec stmt was unimplementable; changed it and refined; Z3 produces ↵ | kyessenov | 2010-08-22 |
| | | | | | evil input again... | ||
| * | Chalice: start of a DSW refinement | kyessenov | 2010-08-22 |
| | | |||
| * | Chalice: refining lists doesn't quite work yet... | kyessenov | 2010-08-22 |
| | | |||
| * | Chalice: limited functions are still problematic (see Calculator.chalice) | kyessenov | 2010-08-22 |
| | | |||
| * | Chalice: | kyessenov | 2010-08-22 |
| | | | | | * coupling invariants work (with certain restrictions as described in TODO comments) | ||
| * | Chalice: | kyessenov | 2010-08-21 |
| | | | | | | * fix a compilation problem (scalac relied on old binaries) * combinator parser and state don't work well together -- added higher-order parser for method transform | ||
| * | server-side rename | kyessenov | 2010-08-21 |
| | | |||
| * | Chalice: added syntax, printer and resolver for coupling invariants | kyessenov | 2010-08-20 |
| | | |||
| * | VS 2010 mode for Chalice: some errors didn't show up in the window because ↵ | kyessenov | 2010-08-20 |
| | | | | | positions were negative | ||
| * | Chalice: more regression tests; cosmetic changes to code | kyessenov | 2010-08-19 |
| | | |||
| * | Chalice: added finite differencing refinement | kyessenov | 2010-08-19 |
| | | |||
| * | Chalice: | kyessenov | 2010-08-19 |
| | | | | | | * support multi-step refinement (convert refinement blocks into normal sequences of statements) * added tests | ||
| * | Chalice: | kyessenov | 2010-08-19 |
| | | | | | | | * added loop transform pattern * implemented translation of refined loops to Boogie (only assert new loop invariants) * refactored loop target computation code (async call was not handled as maybe some other statement) | ||
| * | Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ↵ | kyessenov | 2010-08-19 |
| | | | | | to disable) | ||
| * | Chalice: | kyessenov | 2010-08-18 |
| | | | | | | | * transforms are now callable * resolve transform specs * implement translation for refinement blocks (correct for manipulating locals, not globals) | ||
| * | Chalice: | kyessenov | 2010-08-18 |
| | | | | | | | | * print type checked program (use -print -noTypecheck if you want old behavior) * refactored program context in Resolver ('errors' is kept as a ListBuffer and shared) * added resolver for refinement blocks (no loops yet) * pretty printer should work now for transforms | ||
| * | Chalice: added surface syntax for transform, AST matching algorithm | kyessenov | 2010-08-17 |
| | | |||
| * | Chalice: refactored AST code for class hierarchy (no need for caches since ↵ | kyessenov | 2010-08-17 |
| | | | | | Scala uses structural equality for case classes); landed first piece of refinement code | ||
| * | Chalice: bug fixes -- "check termination" flag was not properly preserved ↵ | kyessenov | 2010-08-16 |
| | | | | | (i.e. if function app was inside old, the flag was ignored); != was not properly translated for sequences | ||
| * | Chalice: add pre-conditions to specification statements; semantically spec ↵ | kyessenov | 2010-08-13 |
| | | | | | statement is just like a call statement now | ||
| * | 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 ↵ | kyessenov | 2010-08-12 |
| | | | | | specified | ||
| * | Chalice: example proving a simple identity (for refinement demonstration), ↵ | kyessenov | 2010-08-12 |
| | | | | | revise code comments | ||
| * | Chalice: put classes and objects into package "chalice" | kyessenov | 2010-08-11 |
| | | |||
| * | Chalice: fix "assume false" in the example (intended a spec statement) | kyessenov | 2010-08-11 |
| | | |||
| * | Chalice: finite differences with recursion instead of loops | kyessenov | 2010-08-10 |
| | | |||
| * | Chalice: added uninterpreted functions; attempting to re-verify Celebrity in ↵ | kyessenov | 2010-08-10 |
| | | | | | Chalice | ||
| * | Chalice: forcefully kill Boogie with taskkill /T /F on termination | kyessenov | 2010-08-10 |
| | | |||
| * | Chalice: refinement of a list with nodes (instead of lists pointing to sublists) | kyessenov | 2010-08-06 |
| | | |||
| * | Chalice: terminate Boogie subprocess manually on interrupt; Z3 still stays ↵ | kyessenov | 2010-08-06 |
| | | | | | alive though??? | ||
| * | Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); ↵ | kyessenov | 2010-08-06 |
| | | | | | added classic sqrt refinement; assertions on acc(s[*].f) have now positions attached | ||
| * | Chalice: try using output coupling assertion as loop invariant | kyessenov | 2010-08-05 |
| | | |||
| * | Chalice: testing refinement of a linked list | kyessenov | 2010-08-04 |
| | | |||
| * | Chalice: testing refinement of Counter | kyessenov | 2010-08-04 |
| | | |||
| * | Chalice: abstract Shorr-Waite algorithm verified | kyessenov | 2010-08-03 |
| | | |||
| * | Chalice: deriving SchorrWaite algorithm with Chalice | kyessenov | 2010-08-03 |
| | | |||
| * | Chalice: added Tarjan's SCC algorithm for computing function call graph and ↵ | kyessenov | 2010-08-03 |
| | | | | | recursion bits | ||
| * | Chalice: | kyessenov | 2010-08-02 |
| | | | | | | | | * change syntax for range: [a..b] instead of [a:b] * add multi-triggers to Boogie bindings * fix unsoundness in frame axiom for functions -- whenever acc(s[*].f,...) is detected in pre-condition, a different encoding to Boogie is applied * add limited functions to translator (disabled since Resolver is not ready yet) | ||
| * | Chalice: | kyessenov | 2010-08-02 |
| | | | | | | | * added quantifiers over any type (forall i: int :: i + 1 == i + 1) * cleaned up AST transformation code; organized one transform operation that should preserve source positions -- it was very annoying to see assertions with lost source positions * added a desugar method that simplifies Chalice AST by unrolling a few constructs -- maybe useful in the future to quickly add a syntactic sugar | ||
| * | Chalice: | kyessenov | 2010-07-30 |
| | | | | | | | | * add sequence axiom updates from Dafny * fix a bug in pretty printer for functions and predicates * add a command line option for not checking termination; refactor options code to update syntax help string * relax resolver to allow ghost state in assume statements (we don't know how to compile them in general anyways; assume false is still a special case and is compiled into assert false) | ||
| * | Chalice: pretty printer now prints element type for sequences; fixed a bug ↵ | kyessenov | 2010-07-27 |
| | | | | | in copying resolved member in sequence accesses; added graph closure (DSW) verification example | ||
| * | Chalice: bug -- permissions were implicity converted to Booge expressions ↵ | kyessenov | 2010-07-22 |
| | | | | | (due to "implicit def") | ||
| * | Chalice: bug -- expression substitution should preserve typing | kyessenov | 2010-07-22 |
| | | |||
| * | Chalice: sequence access wildcards a[*].* and a[*].f have been implemented ↵ | kyessenov | 2010-07-22 |
| | | | | | (sans checking for epsilon going beyond infinity and rd(...,*) permissions) | ||
| * | Chalice: introduced proper AST nodes for permission expressions and ↵ | kyessenov | 2010-07-21 |
| | | | | | permissions. This gets of redundancy in treating acc and rd in many places and should hopefully make permissions code more comprehensible | ||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |