summaryrefslogtreecommitdiff
path: root/Chalice/src
Commit message (Collapse)AuthorAge
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵Gravatar Rustan Leino2013-03-05
| | | | Codeplex repositories.
* Chalice: Disallow unfolding expressions in postconditions.Gravatar stefanheule2012-10-01
|
* Chalice: Fix bug in detecting permissions in postconditions.Gravatar stefanheule2012-10-01
|
* Chalice: Let the trigger for the function postcondition axiom be more ↵Gravatar stefanheule2012-10-01
| | | | permissive.
* Chalice: Use new 'mod' and 'div' operators of Boogie for division and modulo.Gravatar stefanheule2012-09-30
|
* Chalice: Remove superfluous comment.Gravatar stefanheule2012-09-30
|
* Chalice: Clean up /percentageSupport command line option to adapt to the ↵Gravatar stefanheule2012-09-30
| | | | usage of reals for permissions.
* Chalice: Fix some problems related to the use of reals in Boogie.Gravatar stefanheule2012-09-30
|
* Chalice: Further changes to make permissions use the Boogie type real.Gravatar stefanheule2012-09-29
|
* Chalice: Make permissions use the Boogie type real.Gravatar stefanheule2012-09-29
|
* Chalice: Extend the Boogie AST with real literals.Gravatar stefanheule2012-09-29
|
* Chalice (Adapt to real support in Boogie): Axiomatization of division is no ↵Gravatar stefanheule2012-09-29
| | | | longer needed (and in fact, results in a Boogie parse error).
* Chalice: changed quantifier triggering to use #limited#trigger versions of ↵Gravatar Unknown2012-09-27
| | | | functions, instead of their "heap fragment" versions from the framing axiom. It's not totally clear why this works better, but it seems to avoid the excessive triggering Yannis' examples showed.
* Chalice: Fix type-checker incompleteness.Gravatar stefanheule2012-09-24
|
* Chalice: Improve code to generate triggers for framing axiom.Gravatar stefanheule2012-09-24
|
* Chalice: Fix triggers for framing axiom of known-folded locations.Gravatar stefanheule2012-09-24
|
* Chalice: Fix soundness issue about when it is sound to keep knowledge about ↵Gravatar stefanheule2012-09-21
| | | | predicate permission masks.
* Chalice: Alternative approach to frame known-folded locations; use ↵Gravatar stefanheule2012-09-21
| | | | quantification instead of explicit enumeration of locations.
* Chalice: Fix bug of computing the function height.Gravatar stefanheule2012-09-19
|
* Chalice: Use the framing function instead of the limited function in ↵Gravatar stefanheule2012-09-19
| | | | triggers to make them more permissive (and for instance fix a recent test failure).
* Chalice: Updated trigger generation to duplicate the entire quantifier in ↵Gravatar Unknown2012-09-18
| | | | cases where different numbers of extra boolean variables are needed to generate different trigger sets. In this case, the resulting quantified assertions are conjoined together in the result.
* Chalice: modified trigger generation for quantifiers to include the use of ↵Gravatar Unknown2012-09-18
| | | | additional boolean variables to replace any sub-expressions that would be problematic in a candidate trigger (logical operators and comparison operators are forbidden). These extra variables are used in the triggers but not in the bnody of the quantifier. However, they need to be quantified over as well, and this creates a problem if different trigger sets employ different sets of extra variables. For the moment, the implementation groups all of the trigger sets by the sets of extra variables they use, and only outputs the first (in practice, often the only) such group. Hopefully this will be improved on soon.
* Automatic MergeGravatar Unknown2012-09-17
|\
* | Chalice: modified Tr() to only generate a real list of statements when it's ↵Gravatar Unknown2012-09-17
| | | | | | | | going to be used (otherwise Nil is passed).
| * Chalice: Make the triggers for functions so it depends on all dependend ↵Gravatar stefanheule2012-09-14
| | | | | | | | predicate triggers (avoiding matching loops).
| * Chalice: Allow the postcondition axiom to be used when checking function ↵Gravatar stefanheule2012-09-13
| | | | | | | | specifications in certain well-defined cases.
| * Chalice: Merge the two definitional axioms (was previously necessary to work ↵Gravatar stefanheule2012-09-13
| | | | | | | | around a z3 bug that has been fixed).
| * Chalice: Remove CanAssumeFunctionDefs from framing axiom, as it is not ↵Gravatar stefanheule2012-09-13
| | | | | | | | needed for soundness.
| * Chalice: Use the height of functions to increase the expressiveness of the ↵Gravatar stefanheule2012-09-13
| | | | | | | | postcondition axiom.
| * Chalice: Remove debug output.Gravatar stefanheule2012-09-13
| |
| * Chalice: Compute the 'height' for functions (based on the condensation of ↵Gravatar stefanheule2012-09-13
|/ | | | the call graph).
* Chalice: Disallow accessibility predicates in function postconditions.Gravatar stefanheule2012-09-12
|
* Chalice: Also add time information for reg_test, reg_test_all and runalltests.Gravatar stefanheule2012-09-11
|
* Chalice: New command line parameter /time:<n> that allows to output timing ↵Gravatar stefanheule2012-09-11
| | | | information (with varying verbosity). By default, the overall verification time is output.
* Chalice: implemented automatic trigger-finding for quantifiers in ↵Gravatar Unknown2012-09-11
| | | | user-supplied specifications (searching for sets of matching function terms, and taking their "limited" forms).
* Chalice: added findFunctionAppsContaining(..) to Expression, which finds all ↵Gravatar Unknown2012-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. ↵Gravatar Unknown2012-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.
* Chalice: implemented "inside" information for all cases which translate to ↵Gravatar Unknown2012-09-06
| | | | statements. So far this does not include exhaling an unfolding expression, or translation of an unfolding expression in e.g., program code (which looks more challenging). Note that secondary permissions do not appear to be generated in these cases either, which may be problematic for certain pathological examples.
* Chalice: added "inside" knowledge of predicate instance nesting to unfold ↵Gravatar Unknown2012-09-06
| | | | statements (previously only fold was implemented), and to the translation of unfolding expressions in some cases.
* Chalice: first part of implementation of tracking which predicate instances ↵Gravatar Unknown2012-09-06
| | | | occur inside which (for extra non-aliasing information)
* Chalice: support for static functions. Functions declared "static" are ↵Gravatar Unknown2012-09-05
| | | | axiomatised without a receiver. However, calls of such functions still syntactically require a receiver for now (which is ignored).
* Chalice: adopted triggering/axioms used for "recursive" functions for all ↵Gravatar Unknown2012-09-04
| | | | functions (so that the various tricks get applied uniformly, even when Chalice thinks a function is not recursive).
* Chalice: reapplied changes from changesetGravatar Unknown2012-09-03
| | | | 2648 (ff8bdaa099cd) Chalice: Allow unfolding expressions in predicates (this fixes workitem 10223).
* reapplied changes from changeset:Gravatar Unknown2012-09-03
| | | | 2891 (c73229bf100d) Experimental version with weaker triggering for function definition axiom (should trigger whenever both the function application has occurred somewhere in the code, and a corresponding predicate has been either folded or unfolded).
* Chalice: reremoved implementation of (unuses) UpdateSecMask, as was ↵Gravatar Unknown2012-09-03
| | | | previously done in changeset 2678 (ca2a67918aa7)
* Chalice: reapplied changes from changesetGravatar Unknown2012-09-03
| | | | 2669 (bc94e6c85481) Chalice: Remove IsGoodState as it is not needed and causes problems in certain cases.
* Reapplied changes from previous updateGravatar Unknown2012-09-03
| | | | 2568 (f1a12d812207) : Chalice: refactor ExhaleHelper to use a local lambda expression for easier parameter management.
* Reverted Prelude.scala and Translator.scala to those from version 96adb1c351bdGravatar Unknown2012-09-03
|
* New attempt, back to predicate masks that start off empty and gradually get ↵Gravatar Unknown2012-08-09
| | | | populated. The hope is that, with the improved triggers for function framing, this will be sufficient, even for examples where we "learn later" that a location is inside a predicate instance.
* Intermediate version of implementation with two masks per predicate. #m_calc ↵Gravatar Unknown2012-08-09
| | | | | | mask starts out as ZeroPMask and is added to during translation. #m mask starts out havoced, and is assumed to be equal to #m_calc as late as possible. This idea doesn't seem to work out, since the assumes generated come too late in the code for some of the asserts (which depend on framing information) to work. However, given the changes I made to funciton framing recently, I'm wondering if the havoced masks are even necessary any more. Next: try removing them and just using #m_calc for everything..
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-31 10:02:51 +0000