diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-15 11:35:12 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-15 11:35:12 +0200 |
| commit | 4e66de932b91e91e4cadd943ff8859d6f69f57e1 (patch) | |
| tree | ced73719216f2f1fd2eb9057001079a39dbad68e /abstract/abs_interp.ml | |
| parent | 7205927e18ea355a619e95b1036aac9b94a22667 (diff) | |
| download | scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.tar.gz scade-analyzer-4e66de932b91e91e4cadd943ff8859d6f69f57e1.zip | |
Clean up & comment a bit.
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index b5fc684..319f105 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -3,6 +3,7 @@ open Ast_util open Formula open Typing open Cmdline +open Varenv open Util open Num_domain @@ -12,8 +13,6 @@ open Enum_domain module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig - type st - val do_prog : cmdline_opt -> rooted_prog -> unit end = struct @@ -22,6 +21,14 @@ end = struct Disjunction domain ************************** *) + (* + This domain uses a fix set of enumerate-type variables to make disjunctions between + different cases that are analyzed. A case is a list of values for each of these + disjunction variables. The value for that case is the product of a value in a domain + specific for enumerated variables and a domain for numeric variables. See README for + more details. + *) + type case_v = ED.t * ND.t type case = ED.item list @@ -291,7 +298,7 @@ end = struct (* add variables from LASTs *) let last_vars = uniq_sorted - (List.sort compare (Transform.extract_last_vars f)) in + (List.sort compare (extract_last_vars f)) in let last_vars = List.map (fun id -> let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars |