Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | | Merge | Nadia Polikarpova | 2012-09-17 | |
| |\ \ \ \ | |/ / / / |/| | | | | ||||
| * | | | | Allow custom operators on a line | Nadia Polikarpova | 2012-09-17 | |
| | | | | | ||||
* | | | | | During dualisation, | Unknown | 2012-09-17 | |
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | x := y; now becomes x$1 := y$1; x$2 := y$2; instead of x$1, x$2 := y$1, y$2; This is to make way for further changes. | |||
| * | | | Allow several calculation operators (for the whole calculation) | Nadia Polikarpova | 2012-09-16 | |
| | | | | ||||
| * | | | Allowing calc as hint (without braces) | Nadia Polikarpova | 2012-09-16 | |
| | | | | ||||
| * | | | Renamed terms into lines (according to the proposal), fixed some contracts | Nadia Polikarpova | 2012-09-16 | |
| | | | | ||||
| * | | | Added the new keyword (calc) to Util | Nadia Polikarpova | 2012-09-16 | |
| | | | | ||||
* | | | | Added creation of source variable pre- and post- conditions. | Egor Kyshtymov | 2012-09-16 | |
| | | | | | | | | | | | | | | | | | | | | Changed style of error messages. Cleaned up error reporting code. | |||
| * | | | Error reporting for calculation steps | Nadia Polikarpova | 2012-09-14 | |
| | | | | ||||
| * | | | Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵ | Nadia Polikarpova | 2012-09-14 | |
| | | | | | | | | | | | | | | | | t<i> op t<i + 1>), generated during resolution; first version of the translation | |||
| | | * | Chalice: Make the triggers for functions so it depends on all dependend ↵ | stefanheule | 2012-09-14 | |
| | | | | | | | | | | | | | | | | predicate triggers (avoiding matching loops). | |||
| * | | | Merge | Nadia Polikarpova | 2012-09-14 | |
| |\ \ \ | |/ / / |/| | | | ||||
| * | | | Pretty-print calc statements | Nadia Polikarpova | 2012-09-14 | |
| | | | | ||||
| | | * | Chalice: Extend one test case with more complete specification. | stefanheule | 2012-09-13 | |
| | | | | ||||
| | | * | Chalice: Allow the postcondition axiom to be used when checking function ↵ | stefanheule | 2012-09-13 | |
| | | | | | | | | | | | | | | | | specifications in certain well-defined cases. | |||
| * | | | Resolve and clone calc statements; fixed a small grammar bug | Nadia Polikarpova | 2012-09-13 | |
| | | | | ||||
| * | | | Added calc statement to the AST and the grammar (first attempt) | Nadia Polikarpova | 2012-09-13 | |
| | | | | ||||
| | | * | Chalice: Merge the two definitional axioms (was previously necessary to work ↵ | stefanheule | 2012-09-13 | |
| | | | | | | | | | | | | | | | | around a z3 bug that has been fixed). | |||
| | | * | Chalice: Update reference file for a test (a recent improvement makes the ↵ | stefanheule | 2012-09-13 | |
| | | | | | | | | | | | | | | | | verifier more complete). Also remove an old comment from that test. | |||
| | | * | Chalice: Remove CanAssumeFunctionDefs from framing axiom, as it is not ↵ | stefanheule | 2012-09-13 | |
| | | | | | | | | | | | | | | | | needed for soundness. | |||
| | | * | Chalice: Use the height of functions to increase the expressiveness of the ↵ | stefanheule | 2012-09-13 | |
| | | | | | | | | | | | | | | | | postcondition axiom. | |||
| | | * | Chalice: Remove debug output. | stefanheule | 2012-09-13 | |
| | | | | ||||
| | | * | Chalice: Compute the 'height' for functions (based on the condensation of ↵ | stefanheule | 2012-09-13 | |
| | |/ | | | | | | | | | | the call graph). | |||
* | | | Merge | Unknown | 2012-09-12 | |
|\ \ \ | ||||
* | | | | Dafny: clone and merge attributes in refinements | Unknown | 2012-09-12 | |
| | | | | ||||
* | | | | Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ↵ | Unknown | 2012-09-12 | |
| |/ / |/| | | | | | | | | and axiomatize [][..0] == [] == [][0..] | |||
| | * | Chalice: Test case for permissions in function postconditions. | stefanheule | 2012-09-12 | |
| | | | ||||
| | * | Chalice: Disallow accessibility predicates in function postconditions. | stefanheule | 2012-09-12 | |
| | | | ||||
| * | | Updated test 'livevars' that would fail with Z3 4.1 (alternative error trace). | wuestholz | 2012-09-12 | |
| | | | ||||
| * | | Updated test 'test15' that would fail with Z3 4.1 (different ordering of ↵ | wuestholz | 2012-09-12 | |
|/ / | | | | | | | elements in the model output). | |||
| * | Chalice: Switch to latest Scala release (there seems to be a compiler bug ↵ | stefanheule | 2012-09-12 | |
| | | | | | | | | with 2.8.1 that prevents the current code from compiling). | |||
| * | Chalice: Also add time information for reg_test, reg_test_all and runalltests. | stefanheule | 2012-09-11 | |
| | | ||||
| * | Chalice: Update reference output for all test-cases due to recent change in ↵ | stefanheule | 2012-09-11 | |
| | | | | | | | | the output. | |||
| * | Chalice: Adapt test scripts to not output timing information. | stefanheule | 2012-09-11 | |
| | | ||||
| * | Chalice: New command line parameter /time:<n> that allows to output timing ↵ | stefanheule | 2012-09-11 | |
| | | | | | | | | information (with varying verbosity). By default, the overall verification time is output. | |||
* | | Dafny: did a little to extend the support of labeled statements in ↵ | Unknown | 2012-09-10 | |
| | | | | | | | | refinements (things like multiple labels are still not thought through very well) | |||
* | | Dafny: improved checking of inherited postconditions (in refinements) | Unknown | 2012-09-10 | |
| | | ||||
* | | Boogie: added /tracePOs option for printing out number of proof obligations ↵ | Unknown | 2012-09-10 | |
| | | | | | | | | without also printing out the verification times | |||
| * | Chalice: implemented automatic trigger-finding for quantifiers in ↵ | Unknown | 2012-09-11 | |
| | | | | | | | | user-supplied specifications (searching for sets of matching function terms, and taking their "limited" forms). | |||
* | | Merge | Rustan Leino | 2012-09-10 | |
|\ \ | ||||
* | | | ignore Chalice/bin | Rustan Leino | 2012-09-10 | |
| | | | ||||
* | | | Merge | Rustan Leino | 2012-09-10 | |
|\ \ \ | ||||
| * | | | Find implementations of interface methods for dynamic dispatch, not just | Unknown | 2012-09-09 | |
| | | | | | | | | | | | | | | | | overrides of virtual methods. | |||
* | | | | DafnyExtension: addressed a class initialization order problem | Rustan Leino | 2012-09-09 | |
| | | | | ||||
* | | | | Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵ | Rustan Leino | 2012-09-09 | |
| | | | | | | | | | | | | | | | | tail-recursive methods | |||
| * | | | Avoid creating a dynamic dispatch table for GetHashCode and ToString: it ends | Unknown | 2012-09-09 | |
| | | | | | | | | | | | | | | | | | | | | up creating code that the Boogie parser gets a stack overflow while trying to parse! | |||
| * | | | Moved the statement traverser's operand stack (used for explicit push/pop/dup | Unknown | 2012-09-09 | |
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | in the code model) into the sink so that the different statement traversers used for things like if-then-else statements share the same stack. Fixed a problem in the dispatch table for whole program virtual dispatch so it works for generic methods. Found input that either crashed the translator or caused it to produce bad Boogie: "fixed" it by having the translator thrown an exception so the method containing the bad code is skipped. | |||
| | * | Chalice: added findFunctionAppsContaining(..) to Expression, which finds all ↵ | Unknown | 2012-09-08 | |
| | | | | | | | | | | | | | | | | | | the function applications with at least one variable in common with a given list. This is a pre-cursor to writing a trigger-generating routine for quantifiers. Also corrected some copy-paste comments in Translator.scala | |||
| | * | Chalice: implemented the final cases of the "inside" feature for predicates. ↵ | Unknown | 2012-09-08 | |
| | | | | | | | | | | | | | | | | | | At the same time, exhaling an unfolding expression now generates corresponding secondary permission information (this can in principle be useful; with fractional permissions it need not be the case that just because we exhale (part of) a predicate, we don't have any left. Also added a test case to test the new non-aliasing knowledge the "inside" encoding provides in various situations. | |||
* | | | Merge | Unknown | 2012-09-07 | |
|\ \ \ |