summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp.ml13
-rw-r--r--abstract/abs_interp_dynpart.ml9
-rw-r--r--abstract/abs_interp_edd.ml61
-rw-r--r--abstract/apron_domain.ml6
-rw-r--r--abstract/domain.ml3
-rw-r--r--abstract/enum_domain.ml12
-rw-r--r--abstract/enum_domain_edd.ml4
-rw-r--r--abstract/formula.ml165
-rw-r--r--abstract/formula_printer.ml2
-rw-r--r--abstract/intervals_domain.ml7
-rw-r--r--abstract/nonrelational.ml11
-rw-r--r--abstract/num_domain.ml5
-rw-r--r--abstract/transform.ml32
-rw-r--r--abstract/value_domain.ml7
-rw-r--r--abstract/varenv.ml33
15 files changed, 242 insertions, 128 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
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 5beffda..23df612 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -19,6 +19,15 @@ end = struct
type abs_v = ED.t * ND.t
+ (*
+ Abstract analysis based on dynamic partitionning of the state space.
+ Idea : use somme conditions appearing in the text of the program as
+ disjunctions. We don't want to consider them all at once in the first
+ place because it would be way too costly ; instead we try to dynamically
+ partition tye system. But we haven't got a very good heuristic for that,
+ so it doesn't work very well.
+ *)
+
type location = {
id : int;
depth : int;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 31fe5aa..722dc1a 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -26,6 +26,27 @@ end = struct
(* **********************
EDD Domain
********************** *)
+
+ (*
+ This abstract domain is capable of representing values of a program using enumerated
+ variables and numerical variables. The representation is a decision graph on
+ enumerated variables, whose leaves are values for the numerical variables in a given
+ numerical domain (relationnal or non-relationnal). This domain necessarily does the
+ disjunction between all the cases that appear for the enumerated variables, and is
+ not able to do a disjunction with respect to a condition on numerical variables if
+ that condition is not bound to a boolean variable appearing in the program.
+
+ Possible extensions :
+ - use groups of variables, so that an EDD does not have to consider all the
+ numerical and enumerated variables at once
+ - add the possibility for numeric condition decision nodes (something like ghost
+ boolean variables that would be bound to a numeric condition)
+ - ...
+
+ This domain is currently the most promising lead in our research on abstract
+ interpretation of Scade programs.
+ *)
+
type edd =
| DBot
| DTop
@@ -479,10 +500,10 @@ end = struct
let ve = v.ve in
let leaves, get_leaf = get_leaf_fun () in
+ let dq = new_node_fun () in
- let nc = ref 0 in
let memo = Hashtbl.create 12 in
- let node_memo = Hashtbl.create 12 in
+
let rec f l =
let kl = List.sort Pervasives.compare (List.map key l) in
try Hashtbl.find memo kl
@@ -522,16 +543,7 @@ end = struct
let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
c, f (ch1@ch2@ch3))
cl in
- let _, x0 = List.hd cc in
- if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc
- then begin
- let k = (dv, List.map (fun (a, b) -> a, key b) cc) in
- let n =
- try Hashtbl.find node_memo k
- with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
- in
- DChoice(n, dv, cc)
- end else x0
+ dq dv cc
with | Top -> DTop
in Hashtbl.add memo kl r; r
in
@@ -616,7 +628,7 @@ end = struct
(*
- edd_join_widen : edd_v -> edd_v -> edd_v
+ edd_widen : edd_v -> edd_v -> edd_v
*)
let edd_widen (a:edd_v) (b:edd_v) =
let ve = a.ve in
@@ -658,7 +670,7 @@ end = struct
| _ -> assert false
in
- { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) }
+ { leaves; ve; root = time "widen" (fun () -> memo2 f a.root b.root) }
(*
edd_accumulate : edd_v -> edd_v -> edd_v
@@ -703,7 +715,7 @@ end = struct
| _ -> assert false
in
- { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) }
+ { leaves; ve; root = time "accumulate" (fun () -> memo2 f a.root b.root) }
(*
edd_star_new : edd_v -> edd_v -> edd_v
@@ -775,9 +787,11 @@ end = struct
let f = simplify_k (get_root_true f) f in
Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
- (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
- (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
- (* WHY THE **** AM I SHOUTING LIKE THAT ? *)
+ (*
+ Here we simplify the program formula so that uselessly redundant variables don't
+ appear anymore. If an enumerated equation x = y appears at the root of the
+ program, then we chose to remove either x or y.
+ *)
let facts = get_root_true f in
let f, rp, repls = List.fold_left
(fun (f, (rp : rooted_prog), repls) eq ->
@@ -814,6 +828,11 @@ end = struct
Format.printf "Complete formula after simpl:@.%a@.@."
Formula_printer.print_expr f;
+ (*
+ Here we specialize the program formula for the two following cases :
+ - L/must_reset = tt, this is the first instant of the program (global reset)
+ - L/must_reset = ff, this is for all the rest of the time
+ *)
let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in
let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in
@@ -839,10 +858,8 @@ end = struct
let ve = mk_varenv rp f cl in
-
{ rp; opt; ve; init_cl; cl; guarantees; }
-
let do_prog opt rp =
@@ -925,8 +942,10 @@ end = struct
let init_acc = edd_star_new (edd_bot e.ve)
(pass_cycle e.ve (edd_apply_cl (edd_top e.ve) e.init_cl)) in
- (* Dump final state *)
+ (* Iterate *)
let acc = ch_it 0 init_acc in
+
+ (* Dump final state *)
edd_dump_graphviz acc "/tmp/graph-final0.dot";
Format.printf "Finishing up...@.";
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 288f961..a929c0b 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -6,6 +6,11 @@ open Num_domain
open Apron
+(*
+ Link between our NUMERICAL_ENVIRONMENT_DOMAIN interface and Apron.
+ Mostly direct translation between the two.
+*)
+
module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
(* manager *)
@@ -18,7 +23,6 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
type t = man Abstract1.t
(* direct translation of numerical expressions into Apron tree expressions *)
- (* TODO : some variables have type real and not int... *)
let rec texpr_of_nexpr = function
| NIdent id -> Texpr1.Var (Var.of_string id)
| NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i))
diff --git a/abstract/domain.ml b/abstract/domain.ml
deleted file mode 100644
index 76635d1..0000000
--- a/abstract/domain.ml
+++ /dev/null
@@ -1,3 +0,0 @@
-open Ast
-open Formula
-
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 77d7e3f..68b04f5 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -4,6 +4,18 @@ open Util
exception Bot
+(*
+ Interface and implementation of an abstract domain meant to handle
+ constraints on enumerated variables.
+
+ Constraints are basically of two types :
+ - var OP value
+ - var OP var'
+ with OP either == or !=
+
+ (see formula.ml for a definition of the enum_cons type)
+*)
+
module type ENUM_ENVIRONMENT_DOMAIN = sig
type t
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index ae71b09..3e03d59 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -3,6 +3,10 @@ open Formula
open Util
open Enum_domain
+(*
+ Implementation of a more powerfull domain for enumerate constraints,
+ based on decision graphs (BDD).
+*)
module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
exception Top
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 650f8f4..4102891 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -4,6 +4,21 @@ open Ast_util
(* AST for logical formulas *)
+(*
+ Two representations are used for the formulas :
+ - Formula tree, representing the boolean formula directly
+ as would be expected
+ - "conslist", where all the numerical and enumerate constraints
+ considered in a tree of ANDs are regrouped in a big list.
+ The second form is used when applying a formula to an abstract value,
+ whereas the first form is the one generated by the program transformation
+ procedure and is the one we prefer to show the user because it is more
+ easily understandable.
+*)
+
+(* ------------------------------------ *)
+(* First representation *)
+(* ------------------------------------ *)
(* Numerical part *)
@@ -27,7 +42,6 @@ type num_cons = num_expr * num_cons_op (* always imply right member = 0 *)
(* Logical part *)
-
(* Enumerated types *)
type enum_expr =
| EIdent of id
@@ -52,6 +66,11 @@ type bool_expr =
(* (A and B) or ((not A) and C) *)
| BNot of bool_expr
+(*
+ Helper functions to construct formula trees and automatically
+ simplifying some tautologies/contradictions
+*)
+
let is_false = function
| BConst false | BNot(BConst true) -> true
| _ -> false
@@ -85,7 +104,10 @@ let f_e_op op a b = match a, b with
| EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
let f_e_eq = f_e_op E_EQ
-(* Write all formula without using the NOT operator *)
+(*
+ Transformation functions so that all the logical formula are written
+ without using the NOT operator
+*)
let rec eliminate_not = function
| BNot e -> eliminate_not_negate e
@@ -117,68 +139,19 @@ and eliminate_not_negate = function
BOr(eliminate_not_negate a, eliminate_not_negate b)
| BOr(a, b) ->
BAnd(eliminate_not_negate a, eliminate_not_negate b)
+
+(* ------------------------------------ *)
+(* Simplification functions on the *)
+(* first representation *)
+(* ------------------------------------ *)
(*
- In big ANDs, try to separate levels of /\ and levels of \/
- We also use this step to simplify trues and falses that may be present.
-*)
-
-type conslist = enum_cons list * num_cons list * conslist_bool_expr
-and conslist_bool_expr =
- | CLTrue
- | CLFalse
- | CLAnd of conslist_bool_expr * conslist_bool_expr
- | CLOr of conslist * conslist
-
-let rec conslist_of_f = function
- | BNot e -> conslist_of_f (eliminate_not_negate e)
- | BRel (op, a, b, is_real) ->
- let x, y, op = match op with
- | AST_EQ -> a, b, CONS_EQ
- | AST_NE -> a, b, CONS_NE
- | AST_GT -> a, b, CONS_GT
- | AST_GE -> a, b, CONS_GE
- | AST_LT -> b, a, CONS_GT
- | AST_LE -> b, a, CONS_GE
- in
- let cons = if y = NIntConst 0 || y = NRealConst 0.
- then (x, op)
- else (NBinary(AST_MINUS, x, y, is_real), op)
- in [], [cons], CLTrue
- | BConst x ->
- [], [], if x then CLTrue else CLFalse
- | BEnumCons e ->
- [e], [], CLTrue
- | BOr(a, b) ->
- let eca, ca, ra = conslist_of_f a in
- let ecb, cb, rb = conslist_of_f b in
- begin match eca, ca, ra, ecb, cb, rb with
- | _, _, CLFalse, _, _, _ -> ecb, cb, rb
- | _, _, _, _, _, CLFalse -> eca, ca, ra
- | [], [], CLTrue, _, _, _ -> [], [], CLTrue
- | _, _, _, [], [], CLTrue -> [], [], CLTrue
- | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
- end
- | BAnd(a, b) ->
- let eca, ca, ra = conslist_of_f a in
- let ecb, cb, rb = conslist_of_f b in
- let cons = ca @ cb in
- let econs = eca @ ecb in
- begin match ra, rb with
- | CLFalse, _ | _, CLFalse -> [], [], CLFalse
- | CLTrue, _ -> econs, cons, rb
- | _, CLTrue -> econs, cons, ra
- | _, _ -> econs, cons, CLAnd(ra, rb)
- end
- | BTernary(c, a, b) ->
- conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
-
-
-
-(*
- Simplify formula considering something is true
+ Extract enumerated and numeric constants that
+ are always true in the formula (ie do not appear
+ under an OR or a ternary).
+ (not mathematically exact : only a subset is returned)
*)
let rec get_root_true = function
@@ -188,6 +161,13 @@ let rec get_root_true = function
| BRel (a, b, c, d) -> [BRel (a, b, c, d)]
| _ -> []
+(*
+ Simplify formula considering something is true
+ (only does some clearly visible simplifications ;
+ later simplifications are implicitly done when
+ abstract-interpreting the formula)
+*)
+
let rec simplify true_eqs e =
if List.exists
(fun f ->
@@ -228,7 +208,6 @@ let rec simplify_k true_eqs e =
List.fold_left f_and (simplify true_eqs e) true_eqs
-
(*
Simplify a formula replacing a variable with another
*)
@@ -266,7 +245,7 @@ let rec formula_replace_evars repls e =
(*
- extract names of variables referenced in formula
+ Extract names of enumerated variables referenced in formula
*)
let rec refd_evars_of_f = function
@@ -276,3 +255,65 @@ let rec refd_evars_of_f = function
| BEnumCons(_, e, EItem _) -> [e]
| BEnumCons(_, e, EIdent f) -> [e; f]
| _ -> []
+
+
+
+(* ------------------------------------ *)
+(* Second representation *)
+(* ------------------------------------ *)
+
+(*
+ In big ANDs, try to separate levels of /\ and levels of \/
+ We also use this step to simplify trues and falses that may be present.
+*)
+
+type conslist = enum_cons list * num_cons list * conslist_bool_expr
+and conslist_bool_expr =
+ | CLTrue
+ | CLFalse
+ | CLAnd of conslist_bool_expr * conslist_bool_expr
+ | CLOr of conslist * conslist
+
+let rec conslist_of_f = function
+ | BNot e -> conslist_of_f (eliminate_not_negate e)
+ | BRel (op, a, b, is_real) ->
+ let x, y, op = match op with
+ | AST_EQ -> a, b, CONS_EQ
+ | AST_NE -> a, b, CONS_NE
+ | AST_GT -> a, b, CONS_GT
+ | AST_GE -> a, b, CONS_GE
+ | AST_LT -> b, a, CONS_GT
+ | AST_LE -> b, a, CONS_GE
+ in
+ let cons = if y = NIntConst 0 || y = NRealConst 0.
+ then (x, op)
+ else (NBinary(AST_MINUS, x, y, is_real), op)
+ in [], [cons], CLTrue
+ | BConst x ->
+ [], [], if x then CLTrue else CLFalse
+ | BEnumCons e ->
+ [e], [], CLTrue
+ | BOr(a, b) ->
+ let eca, ca, ra = conslist_of_f a in
+ let ecb, cb, rb = conslist_of_f b in
+ begin match eca, ca, ra, ecb, cb, rb with
+ | _, _, CLFalse, _, _, _ -> ecb, cb, rb
+ | _, _, _, _, _, CLFalse -> eca, ca, ra
+ | [], [], CLTrue, _, _, _ -> [], [], CLTrue
+ | _, _, _, [], [], CLTrue -> [], [], CLTrue
+ | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
+ end
+ | BAnd(a, b) ->
+ let eca, ca, ra = conslist_of_f a in
+ let ecb, cb, rb = conslist_of_f b in
+ let cons = ca @ cb in
+ let econs = eca @ ecb in
+ begin match ra, rb with
+ | CLFalse, _ | _, CLFalse -> [], [], CLFalse
+ | CLTrue, _ -> econs, cons, rb
+ | _, CLTrue -> econs, cons, ra
+ | _, _ -> econs, cons, CLAnd(ra, rb)
+ end
+ | BTernary(c, a, b) ->
+ conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
+
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index a5359a8..dd902ad 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -3,6 +3,8 @@ open Ast
open Formula
open Ast_printer
+(* Just a pretty-printer, nothing to see here *)
+
let string_of_binary_rel = function
| AST_EQ -> "="
| AST_NE -> "≠"
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 084e397..22ea60b 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -1,5 +1,12 @@
open Value_domain
+(*
+ Value domain for representing one interval, doing operations on
+ such representations, etc.
+
+ Restricted implementation, only support integers.
+*)
+
module VD : VALUE_DOMAIN = struct
type t = itv
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index efa30dd..ed029da 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -5,9 +5,11 @@ open Ast
open Value_domain
open Num_domain
-let debug = false
+(*
+ Implementation of a nonrelationnal domain for numerical values.
-(* Restricted domain, only support integers *)
+ Restricted implementation, only support integers.
+*)
module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
type env = V.t VarMap.t
@@ -160,11 +162,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
| AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u
| AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v
in
- if debug then Format.printf
- "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i
- (Formula_printer.string_of_binary_rel op)
- Formula_printer.print_num_expr expr
- (V.to_string v1) (V.to_string v2) (V.to_string v1');
Env (VarMap.add i v1' env))
env
in
diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml
index 285b3c4..a91c69f 100644
--- a/abstract/num_domain.ml
+++ b/abstract/num_domain.ml
@@ -1,6 +1,11 @@
open Ast
open Formula
+(*
+ Interface specification for a numerical environment domain
+ (relationnal with Apron or nonrelationnal with intervals)
+*)
+
module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
type t
type itv
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 20512aa..eedec3e 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -7,7 +7,8 @@ open Typing
open Interpret (* used for constant evaluation ! *)
-(* Transform SCADE program to logical formula.
+(* Transform SCADE program to logical formula.
+ See formula.ml for a description of the formula's AST.
Convention : to access the last value of a variable,
access the variable with the same name prefixed by "L".
@@ -527,8 +528,6 @@ let f_of_prog_incl_init rp assume_guarantees =
assume_guarantees in
f_and clock_eq (f_and no_next_init_cond scope_f)
-
-
(*
Get expressions for guarantee violation
@@ -583,30 +582,3 @@ and guarantees_of_prog rp =
-(*
- Extract variables accessed by a LAST
-*)
-
-let rec extract_last_vars = function
- | BRel(_, a, b, _) ->
- elv_ne a @ elv_ne b
- | BEnumCons c ->
- elv_ec c
- | BAnd(a, b) | BOr (a, b) ->
- extract_last_vars a @ extract_last_vars b
- | BNot(e) -> extract_last_vars e
- | BTernary(c, a, b) -> extract_last_vars c @
- extract_last_vars a @ extract_last_vars b
- | _ -> []
-
-and elv_ne = function
- | NIdent i when i.[0] = 'L' -> [i]
- | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
- | NUnary (_, a, _) -> elv_ne a
- | _ -> []
-
-and elv_ec (_, v, q) =
- (if v.[0] = 'L' then [v] else []) @
- (match q with
- | EIdent i when i.[0] = 'L' -> [i]
- | _ -> [])
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index 0a421f7..48d87f9 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -1,4 +1,11 @@
+(*
+ Interface definition for any single-value abstract domain.
+ Only implementation of interface is intervals.
+*)
+
+
+
type bound = Int of int | PInf | MInf
type itv = Itv of bound * bound | Bot
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 4d6caca..cf29edf 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -25,6 +25,37 @@ type varenv = {
+
+(*
+ Extract variables accessed by a LAST
+*)
+
+let rec extract_last_vars = function
+ | BRel(_, a, b, _) ->
+ elv_ne a @ elv_ne b
+ | BEnumCons c ->
+ elv_ec c
+ | BAnd(a, b) | BOr (a, b) ->
+ extract_last_vars a @ extract_last_vars b
+ | BNot(e) -> extract_last_vars e
+ | BTernary(c, a, b) -> extract_last_vars c @
+ extract_last_vars a @ extract_last_vars b
+ | _ -> []
+
+and elv_ne = function
+ | NIdent i when i.[0] = 'L' -> [i]
+ | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
+ | NUnary (_, a, _) -> elv_ne a
+ | _ -> []
+
+and elv_ec (_, v, q) =
+ (if v.[0] = 'L' then [v] else []) @
+ (match q with
+ | EIdent i when i.[0] = 'L' -> [i]
+ | _ -> [])
+
+
+
(*
extract_linked_evars : conslist -> (id * id) list
@@ -200,7 +231,7 @@ let force_ordering vars groups =
let mk_varenv (rp : rooted_prog) f cl =
(* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 17:17:13 +0000