diff options
author | 2011-07-01 11:40:18 +0200 | |
---|---|---|
committer | 2011-07-01 11:40:18 +0200 | |
commit | 29997a5dd73bfe92292caf1c26fea6b04082a7c9 (patch) | |
tree | 075d85b62fe670d744384aabfc83b01199d36ca0 /Chalice/make.py | |
parent | 9dfd07f5afe943abf40eaa7a9351ea92748b59ab (diff) |
Chalice: New permission model that provides more abstraction and more flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/).
This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced:
- Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed
- Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases
- Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.)
Currently not working - but planned to be updated as well - are the following features:
- Stepwise refinements
- autoFold
- read locks
There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice.
A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs)
- workitem 10200: Issue with the axiom of framing functions
- workitem 10197: The translation of old(waitlevel) resultet in Boogie error
- workitem 10196: Quantification over empty sequences
- workitem 10195: Contradiction when descending sequences are used
- workitem 10192: Invalid translation of old-construct in certain cases
- workitem 10190: Stack overflow when parsing large comment blocks
- workitem 10147: Duplicated method parameters and return values are not detected
Diffstat (limited to 'Chalice/make.py')
-rw-r--r-- | Chalice/make.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Chalice/make.py b/Chalice/make.py index e3ba1ab9..c7fb52d9 100644 --- a/Chalice/make.py +++ b/Chalice/make.py @@ -14,6 +14,9 @@ lastbuild = None if os.path.exists(buildstamp):
lastbuild = os.path.getmtime(buildstamp)
+if not os.path.exists(bindir):
+ os.makedirs(bindir)
+
changedfiles = [file for file in srcfiles if not lastbuild or lastbuild <= os.path.getmtime(file)]
if not changedfiles:
|