diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 27de33b58005ec5c5bea7e292c7aff70546d17be..d995b8b7ffe1d28df7d9b454b8fc6df7ee0b8e44 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -80,10 +80,7 @@ let unpack_mp flags mp admit =
let pred = if flags.simpl then
Meta_simplify.simplify pred
else pred
- in
- if flags.eacsl_transform then
- Meta_simplify.eacsl_transform pred
- else pred
+ in pred
in
let ump_assert = match mp.mp_translation with
| MtNone -> assert false
diff --git a/meta_options.ml b/meta_options.ml
index d0e8c762fbdaec6a3fb3e9084638df85a586e284..3059719bcfddb3bc19e993acfdc739c3b00764fd 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -42,11 +42,6 @@ module Check_External = Self.True (struct
modifying/accessing the state inside the caller's body"
end)
-module Eacsl_transform = Self.False (struct
- let option_name = "-meta-eacsl"
- let help = "Removes \\let and simple \\separated to accomodate E-ACSL"
- end)
-
module Targets = Self.String_set (struct
let option_name = "-meta-set"
let arg_name = "targets"
@@ -107,7 +102,6 @@ module Default_to_assert = Self.True (struct
type meta_flags = {
check_external : bool;
simpl : bool;
- eacsl_transform : bool;
static_bindings : int option;
target_set : StringSet.t option;
number_assertions : bool;
diff --git a/meta_run.ml b/meta_run.ml
index ab057a24cd52e697b9e1a1c35520c40c77ceef3e..2b184b9d0183ea3ac1bd6fdd2e1607980d77bc3f 100644
--- a/meta_run.ml
+++ b/meta_run.ml
@@ -70,7 +70,6 @@ let register () =
let flags = {
check_external = Check_External.get ();
simpl = Simpl.get ();
- eacsl_transform = Eacsl_transform.get ();
number_assertions = Number_assertions.get ();
prefix_meta = Prefix_meta.get ();
static_bindings = (let r = Static_bindings.get () in
@@ -93,8 +92,7 @@ let translate ?(check_external=true) ?(simpl=true) ?target_set
let flags = {
number_assertions; default_to_assert = true;
static_bindings; prefix_meta; list_targets = false;
- check_external; simpl; target_set; eacsl_transform = false;
- keep_proof_files = false;
+ check_external; simpl; target_set; keep_proof_files = false;
} in generate flags
let () =
diff --git a/meta_simplify.ml b/meta_simplify.ml
index 76f52db87401d77830090dc082df887f08777edc..da1e8a6dc0c2b9960231d7b34be1282e2b5f9500 100644
--- a/meta_simplify.ml
+++ b/meta_simplify.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Meta_options
(* Check if a logic variable corresponds to a C variable in the source code
* (to easily discard a separation between it and something else if there is no
@@ -171,116 +170,10 @@ class simplifier_visitor = object(_)
| _ -> Cil.DoChildren
end
-class unfold_one_let lid t' = object (_)
- inherit Visitor.frama_c_inplace
- method! vterm _ =
- Cil.DoChildrenPost (fun t ->
- match t.term_node with
- | TLval (TVar {lv_kind = LVLocal; lv_id; _}, _) when lv_id = lid -> t'
- | _ -> t
- )
-end
-(*
- * Unfolds \let and replace restricted cases of \separated with
- * \base_addr, \offset, etc.-based formulas
- *
- * -----|--##>-----------
- * ------|##---->--------
- * begin(o) = \base_address(o) + \offset(o)
- * end(o) = begin(o) + \sizeof(o)
- * \separated(o1, o2) <==> begin(o1) > end(o2) || begin(o2) > end(o1)
- *)
-class eacsl_transform_vis = object(_)
- inherit Visitor.frama_c_inplace
-
- method! vpredicate _ =
- Cil.DoChildrenPost (fun p ->
- match p.pred_content with
- | Plet ({l_var_info = lvi; l_body = LBterm t}, pred) ->
- let vis = new unfold_one_let lvi.lv_id t in
- Visitor.visitFramacPredicate vis pred
- | Plet _ -> Self.feedback "Unsupported let %a" Printer.pp_predicate p;
- p
- | Pseparated [t1; t2] ->
- let ptrt = Ctype (Cil.charPtrType) in
- let rec ba o = begin match o.term_node with
- | TAddrOf (TVar tab, TIndex ({term_node = Trange (Some _, Some _)}, TNoOffset)) ->
- ba (Logic_const.term (TStartOf (TVar tab, TNoOffset)) ptrt)
- | TBinOp(PlusPI, ptr, {term_node = Trange (Some _, Some _)}) ->
- ptr
- | TBinOp(IndexPI, ptr, {term_node = Trange (Some _, Some _)}) ->
- ptr
- | _ -> Logic_const.term (Tbase_addr(BuiltinLabel Here, o)) ptrt
- end in
- let off o = begin match o.term_node with
- | TAddrOf (TVar tab, TIndex ( {term_node = Trange ( Some begt, Some _)}, TNoOffset)) ->
- let artype = begin match tab.lv_type with
- | Ctype at -> Cil.typeOf_array_elem at
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, begt)) Linteger
- | TBinOp(PlusPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some _)})
- | TBinOp(IndexPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some _)}) ->
- let artype = begin match ptrType with
- | Ctype tt -> Cil.typeOf_pointed tt
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, begt)) Linteger
- | _ -> Logic_const.term (Toffset(BuiltinLabel Here, o)) Linteger
- end in
- let bl o = begin match o.term_node with
- | TAddrOf (TVar tab, TIndex (
- {term_node = Trange (Some begt, Some endt)}, TNoOffset)) ->
- let diff = Logic_const.term (TBinOp (MinusA, endt, begt)) Linteger in
- let artype = begin match tab.lv_type with
- | Ctype at -> Cil.typeOf_array_elem at
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, diff)) Linteger
- | TBinOp(PlusPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some endt)})
- | TBinOp(IndexPI,
- {term_type = ptrType},
- {term_node = Trange (Some begt, Some endt)}) ->
- let diff = Logic_const.term (TBinOp (MinusA, endt, begt)) Linteger in
- let artype = begin match ptrType with
- | Ctype tt -> Cil.typeOf_pointed tt
- | _ -> assert false
- end in
- let so = Logic_const.term (TSizeOf artype) Linteger in
- Logic_const.term (TBinOp (Mult, so, diff)) Linteger
- | _ ->
- let tp = begin match o.term_type with
- | Ctype tt -> Cil.typeOf_pointed tt
- | _ -> assert false
- end in
- Logic_const.term (TSizeOf tp) Linteger
- end in
- let fbeg o = Logic_const.term (TBinOp (PlusA, ba o, off o)) Linteger in
- let fend o = Logic_const.term (TBinOp (PlusA, fbeg o, bl o)) Linteger in
- let c1 = Logic_const.prel (Rge, fbeg t1, fend t2) in
- let c2 = Logic_const.prel (Rge, fbeg t2, fend t1) in
- Logic_const.por (c1, c2)
- | _ -> p
- )
-end
-
let simplify pred =
let vis = new simplifier_visitor in
Visitor.visitFramacPredicate vis pred
-let eacsl_transform pred =
- let vis = new eacsl_transform_vis in
- Visitor.visitFramacPredicate vis pred
-
(*
* Given a predicate and the statement (and kf) it will be attached to,
* return another predicate where every quantified, local or formal logic
diff --git a/meta_simplify.mli b/meta_simplify.mli
index bd33ed1a5ce7ecde0c1d302d1213d134504caf7d..b970d3f3822c61af345f45ef2e9a2c3f7f6b01bc 100644
--- a/meta_simplify.mli
+++ b/meta_simplify.mli
@@ -23,7 +23,6 @@
open Cil_types
val simplify : predicate -> predicate
-val eacsl_transform : predicate -> predicate
val remove_alpha_conflicts : predicate -> kernel_function -> stmt -> predicate
val neq_lval : term_lval -> term_lval -> bool
val is_not_orig_variable : logic_var -> bool