diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-26 18:03:33 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-26 18:03:33 +0200 |
| commit | 11e7905ba16d4b13b5c2eda50a198391693e5d96 (patch) | |
| tree | e083b92f611047eb5ae353aca497021a9611a108 /abstract | |
| parent | f3d89408ebb44f77f257b2cb51a4bdd74b9268d0 (diff) | |
| download | scade-analyzer-11e7905ba16d4b13b5c2eda50a198391693e5d96.tar.gz scade-analyzer-11e7905ba16d4b13b5c2eda50a198391693e5d96.zip | |
Minor corrections.
- Use correect clock scope in typing
- De-activate multi-valuated domain for enumerate vars + var couples.
- Add comment explaining why it doesn't work
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/enum_domain.ml | 9 | ||||
| -rw-r--r-- | abstract/transform.ml | 1 |
2 files changed, 10 insertions, 0 deletions
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index 2353049..d216276 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -268,6 +268,15 @@ end Complicated domain : a set of values for each variables, plus some constraints on couples of variables (eg. (x, y) in [ tt, tt ; ff, ff ] + + WARNING : This domain is not proved to be safe. In particular, it may represent + a set of contraints that imply Bot (ie that are impossible) without raising the + Bot exception. (there is potentially exponential cost in the checking that all + the constraints are coherent, and I have no idea of an algorithm for doing that + check.) + + Therefore, do not use this domain unless you know what you are doing (which is + probably not the case anyway). *) module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct diff --git a/abstract/transform.ml b/abstract/transform.ml index 4a13e18..d9b20d8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -475,3 +475,4 @@ and guarantees_of_prog rp = } in g_of_scope td rp.root_scope "" (BConst true) + |