diff options
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 |