diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 1e911b3d17b18982c22e05affe1c513cbe9c45bd..7224d5519e39957161ade8c2d5719d564b076592 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -59,7 +59,7 @@ type t =
env_stack: local_env list;
init_env: local_env;
var_mapping: Varinfo.t Logic_var.Map.t; (* bind logic var to C var *)
- loop_invariants: predicate named list list;
+ loop_invariants: predicate list list;
(* list of loop invariants for each currently visited loops *)
cpt: int; (* counter used when generating variables *) }
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index f1d5f2c452fb46cceac152df003a2cb60c545f20..51d40665385a737a24d99e6e8d560ecd6bbf46c4 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -66,7 +66,7 @@ module Logic_binding: sig
val remove: t -> logic_var -> t
end
-val add_assert: t -> stmt -> predicate named -> unit
+val add_assert: t -> stmt -> predicate -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
@@ -119,8 +119,8 @@ val set_annotation_kind: t -> Misc.annotation_kind -> t
(* ************************************************************************** *)
val push_loop: t -> t
-val add_loop_invariant: t -> predicate named -> t
-val pop_loop: t -> predicate named list * t
+val add_loop_invariant: t -> predicate -> t
+val pop_loop: t -> predicate list * t
(* ************************************************************************** *)
(** {2 RTEs} *)
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index b4fa6ede3c3d899359027f4a782727de87d15806..a3871f06a64cd2914f885513318126cbdc97f8e3 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -191,7 +191,7 @@ let predicate_to_exp =
~journalize:false
"predicate_to_exp"
(Datatype.func2
- Kernel_function.ty Cil_datatype.Predicate_named.ty Cil_datatype.Exp.ty)
+ Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
Translate.predicate_to_exp
let add_e_acsl_library _files =
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 1b32c106fcf84a3578fe2b482d2d52337dfd9808..1704470ba4b6d46a6d8329d5623fd311e74e8afd 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -145,10 +145,10 @@ let mk_gen_name name =
(* Build a C conditional doing a runtime assertion check. *)
let mk_e_acsl_guard ?(reverse=false) kind kf e p =
- let loc = p.loc in
+ let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
- (Format.asprintf "%a@?" Printer.pp_predicate_named) p
+ (Format.asprintf "%a@?" Printer.pp_predicate) p
in
let line = (fst loc).Lexing.pos_lnum in
let e =
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 261a76633610ea1570ec2befb97857b35d2095f7..dbc11e59db77a31e3d42e65d56d078a7605c1836 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -46,7 +46,7 @@ type annotation_kind =
| RTE
val mk_e_acsl_guard:
- ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate named
+ ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
-> stmt
val mk_block: Project.t -> stmt -> block -> stmt
diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml
index 760834c8209a42aab7dcd261db423ed328cff3ea..117b3cf5b33b179c66c26c0929b3ad01e015529f 100644
--- a/src/plugins/e-acsl/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/mmodel_analysis.ml
@@ -309,7 +309,7 @@ module rec Transfer
let register_object kf state_ref = object
inherit Visitor.frama_c_inplace
- method !vpredicate = function
+ method !vpredicate_node = function
| Pvalid(_, t) | Pvalid_read(_, t) | Pvalid_function t
| Pinitialized(_, t) | Pfreeable(_, t) ->
(* Options.feedback "REGISTER %a" Cil.d_term t;*)
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 71ab22990c6307f86fb67cb63675c3c736a7235b..f26cb8fa5f1069e757cab8767ebfc5a128e5970f 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -24,8 +24,8 @@ open Cil_types
open Cil
open Cil_datatype
-let named_predicate_to_exp_ref
- : (kernel_function -> Env.t -> predicate named -> exp * Env.t) ref
+let predicate_to_exp_ref
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
= Extlib.mk_fun "named_predicate_to_exp_ref"
let term_to_exp_ref
@@ -37,7 +37,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
let msg1 = Format.asprintf msg pp x in
let msg2 =
Format.asprintf "@[ in quantification@ %a@]"
- Printer.pp_predicate_named quantif
+ Printer.pp_predicate quantif
in
Error.untypable (msg1 ^ msg2)
in
@@ -58,8 +58,8 @@ let compute_quantif_guards quantif bounded_vars hyps =
else error "@[invalid binder %a@]" Printer.pp_term t
| _ -> error "@[invalid binder %a@]" Printer.pp_term t
in
- let rec parse acc vars p = match p.content with
- | Pand(p, { content = Prel((Rlt | Rle) as r, t1, t2) }) ->
+ let rec parse acc vars p = match p.pred_content with
+ | Pand(p, { pred_content = Prel((Rlt | Rle) as r, t1, t2) }) ->
(* && is left-associative in the AST *)
let acc, partial, vars = parse acc vars p in
(match partial with
@@ -82,7 +82,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
| Prel((Rlt | Rle) as r, t1, t2) ->
(* left-most predicate: the searched variable is [t2] *)
left_term acc vars (t1, r) t2
- | _ -> error "@[invalid guard %a@]" Printer.pp_predicate_named p
+ | _ -> error "@[invalid guard %a@]" Printer.pp_predicate p
in
let acc, partial, vars = parse [] bounded_vars hyps in
(match partial with
@@ -100,7 +100,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
List.iter
(fun v -> Format.fprintf fmt "@[%a @]" Printer.pp_logic_var v)
vars)
- Printer.pp_predicate_named quantif
+ Printer.pp_predicate quantif
in
Error.untypable msg);
List.rev acc
@@ -119,7 +119,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
if is_forall then o, z, (fun x -> x)
else z, o, (fun e -> new_exp ~loc:e.eloc (UnOp(LNot, e, intType)))
in
- let named_predicate_to_exp = !named_predicate_to_exp_ref in
+ let named_predicate_to_exp = !predicate_to_exp_ref in
let term_to_exp = !term_to_exp_ref in
(* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in
@@ -281,12 +281,12 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
res, env
let quantif_to_exp kf env p =
- let loc = p.loc in
- match p.content with
- | Pforall(bounded_vars, { content = Pimplies(hyps, goal) }) ->
+ let loc = p.pred_loc in
+ match p.pred_content with
+ | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) }) ->
convert kf env loc true p bounded_vars hyps goal
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
- | Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
+ | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
convert kf env loc false p bounded_vars hyps goal
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| _ -> assert false
diff --git a/src/plugins/e-acsl/quantif.mli b/src/plugins/e-acsl/quantif.mli
index e1cb26309d32ca157739e6d69d9f4251493d8715..873579909f499b4b8671d75d3c39b3ad529513c0 100644
--- a/src/plugins/e-acsl/quantif.mli
+++ b/src/plugins/e-acsl/quantif.mli
@@ -24,15 +24,15 @@
open Cil_types
-val quantif_to_exp: kernel_function -> Env.t -> predicate named -> exp * Env.t
+val quantif_to_exp: kernel_function -> Env.t -> predicate -> exp * Env.t
(** The given predicate must be a quantification. *)
(* ***********************************************************************)
(** {2 Forward references} *)
(* ***********************************************************************)
-val named_predicate_to_exp_ref:
- (kernel_function -> Env.t -> predicate named -> exp * Env.t) ref
+val predicate_to_exp_ref:
+ (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevator_test/CSRV14/main.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevator_test/CSRV14/main.o
deleted file mode 100755
index 41692ff84e80669df0633240871ef9484128465d..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevator_test/CSRV14/main.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/cabin.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/cabin.o
deleted file mode 100755
index 7ef4b421ba573c31d17f4838e2a1a4c496b7cd2e..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/cabin.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/door.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/door.o
deleted file mode 100755
index 07cc21e7226302faf0db09e9d52b851171012680..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/door.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/elevator.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/elevator.o
deleted file mode 100755
index 2e58d11072effaf2debbfa9048618b2a1d9f5023..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/elevator.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/ext_call.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/ext_call.o
deleted file mode 100755
index 08a427d2d19bf02c9a4cff84adc6099c209d908a..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/ext_call.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/rendering.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/rendering.o
deleted file mode 100755
index 3849778e6b1899979ba67ec3e5e2c7c2a30514c5..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/rendering.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/testing.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/testing.o
deleted file mode 100755
index b168888c608f174a022e681f1032eda7d84d06e2..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/testing.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/transitions.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/transitions.o
deleted file mode 100755
index 0a7018777f678ae53443b4232b18ba249eec8a91..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/transitions.o and /dev/null differ
diff --git a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/utils.o b/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/utils.o
deleted file mode 100755
index 8f3f5088e0dae947f0fbb96d5f69d5ad79a92a6a..0000000000000000000000000000000000000000
Binary files a/src/plugins/e-acsl/tests/csrv14/Team3/Bench1/elevatorlib/CSRV14/src/utils.o and /dev/null differ
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index bcb73b373ca6c5f3394fd6ff59971d44b0fcadf7..4cb1ce8ed9a2197274f1b1d2c422825b88f6e596 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -607,8 +607,8 @@ and at_to_exp env t_opt label e =
any) in the given environment. Also extend this environment which includes
the generating constructs. *)
and named_predicate_content_to_exp ?name kf env p =
- let loc = p.loc in
- match p.content with
+ let loc = p.pred_loc in
+ match p.pred_content with
| Pfalse -> Cil.zero ~loc, env
| Ptrue -> Cil.one ~loc, env
| Papp _ -> not_yet env "logic function application"
@@ -720,7 +720,7 @@ and named_predicate_to_exp ?name kf ?rte env p =
let env = if rte then translate_rte kf env e else env in
let cast = Typing.get_cast_of_predicate p in
add_cast
- ~loc:p.loc
+ ~loc:p.pred_loc
?name
env
cast
@@ -758,7 +758,7 @@ and translate_rte kf env e =
and translate_named_predicate kf env p =
Options.feedback ~dkey ~level:3 "translating predicate %a"
- Printer.pp_predicate_named p;
+ Printer.pp_predicate p;
let rte = Env.generate_rte env in
Typing.type_named_predicate ~must_clear:rte p;
let e, env = named_predicate_to_exp kf ~rte env p in
@@ -772,7 +772,7 @@ let named_predicate_to_exp ?name kf env p =
let () =
Quantif.term_to_exp_ref := term_to_exp;
- Quantif.named_predicate_to_exp_ref := named_predicate_to_exp
+ Quantif.predicate_to_exp_ref := named_predicate_to_exp
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
@@ -814,10 +814,10 @@ let term_to_exp typ t =
let assumes_predicate bhv =
List.fold_left
- (fun acc p ->
- Logic_const.pand
- ~loc:p.ip_loc
- (acc, Logic_const.unamed ~loc:p.ip_loc p.ip_content))
+ (fun acc p ->
+ let loc = p.ip_content.pred_loc in
+ Logic_const.pand ~loc (acc,
+ Logic_const.unamed ~loc p.ip_content.pred_content))
Logic_const.ptrue
bhv.b_assumes
@@ -842,13 +842,14 @@ let translate_preconditions kf kinstr env behaviors =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
- let do_it env =
- if must_translate (Property.ip_of_requires kf kinstr b p) then
- let loc = p.ip_loc in
- let p =
- Logic_const.pimplies
- ~loc
- (assumes_pred, Logic_const.unamed ~loc p.ip_content)
+ let do_it env =
+ if must_translate (Property.ip_of_requires kf kinstr b p) then
+ let loc = p.ip_content.pred_loc in
+ let p =
+ Logic_const.pimplies
+ ~loc
+ (assumes_pred,
+ Logic_const.unamed ~loc p.ip_content.pred_content)
in
translate_named_predicate kf env p
else
@@ -881,13 +882,13 @@ let translate_postconditions kf kinstr env behaviors =
let do_it env =
match t with
| Normal ->
- let loc = p.ip_loc in
+ let loc = p.ip_content.pred_loc in
let p = p.ip_content in
let p =
Logic_const.pimplies
~loc
(Logic_const.pold ~loc assumes_pred,
- Logic_const.unamed ~loc p)
+ Logic_const.unamed ~loc p.pred_content)
in
translate_named_predicate kf env p
| Exits | Breaks | Continues | Returns ->
diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli
index 3e858be410e6b9c483ac0a625d97828b36b11993..294b0cde138c37781f9f73f06cff206319fcc7ff 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/translate.mli
@@ -33,7 +33,7 @@ val translate_pre_code_annotation:
val translate_post_code_annotation:
kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
val translate_named_predicate:
- kernel_function -> Env.t -> predicate named -> Env.t
+ kernel_function -> Env.t -> predicate -> Env.t
val translate_rte_annots:
(Format.formatter -> 'a -> unit) ->
@@ -46,7 +46,7 @@ val translate_rte_annots:
exception No_simple_translation of term
val term_to_exp: typ option -> term -> exp
-val predicate_to_exp: kernel_function -> predicate named -> exp
+val predicate_to_exp: kernel_function -> predicate -> exp
val set_original_project: Project.t -> unit
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 7b7832024fc6384ec236fb7cffee767eb7e1227b..1475fe087f00b12769a368ff3265caa6b8d5e77a 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -28,7 +28,7 @@ open Cil_types
let dkey = Options.dkey_typing
let compute_quantif_guards_ref
- : (predicate named -> logic_var list -> predicate named ->
+ : (predicate -> logic_var list -> predicate ->
(term * relation * logic_var * relation * term) list) ref
= Extlib.mk_fun "compute_quantif_guards_ref"
@@ -443,10 +443,10 @@ and type_term_offset = function
ignore (type_term ~force:true ~ctx:(size_t ()) t);
type_term_offset toff
-let rec type_predicate_named p =
- Cil.CurrentLoc.set p.loc;
+let rec type_predicate p =
+ Cil.CurrentLoc.set p.pred_loc;
(* this pattern matching also follows the formal rules of the JFLA's paper *)
- let op = match p.content with
+ let op = match p.pred_content with
| Pfalse | Ptrue -> c_int
| Papp _ -> Error.not_yet "logic function application"
| Pseparated _ -> Error.not_yet "\\separated"
@@ -471,22 +471,22 @@ let rec type_predicate_named p =
| Pxor(p1, p2)
| Pimplies(p1, p2)
| Piff(p1, p2) ->
- ignore (type_predicate_named p1);
- ignore (type_predicate_named p2);
+ ignore (type_predicate p1);
+ ignore (type_predicate p2);
c_int
| Pnot p ->
- ignore (type_predicate_named p);
+ ignore (type_predicate p);
c_int
| Pif(t, p1, p2) ->
let ctx = mk_ctx ~force:true c_int in
ignore (type_term ~force:true ~ctx t);
- ignore (type_predicate_named p1);
- ignore (type_predicate_named p2);
+ ignore (type_predicate p1);
+ ignore (type_predicate p2);
c_int
| Plet _ -> Error.not_yet "let _ = _ in _"
- | Pforall(bounded_vars, { content = Pimplies(hyps, goal) })
- | Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
+ | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
+ | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
let guards = !compute_quantif_guards_ref p bounded_vars hyps in
List.iter
(fun (t1, r1, x, r2, t2) ->
@@ -525,7 +525,7 @@ let rec type_predicate_named p =
ignore (type_term ~force:true ~ctx t2);
Interval.Env.add x i)
guards;
- (type_predicate_named goal).ty
+ (type_predicate goal).ty
| Pinitialized(_, t)
| Pfreeable(_, t)
@@ -538,7 +538,7 @@ let rec type_predicate_named p =
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
- | Pat(p, _) -> (type_predicate_named p).ty
+ | Pat(p, _) -> (type_predicate p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
in
@@ -551,12 +551,12 @@ let type_term ~force ?ctx t =
let type_named_predicate ?(must_clear=true) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
- Printer.pp_predicate_named p;
+ Printer.pp_predicate p;
if must_clear then begin
Interval.Env.clear ();
Memo.clear ()
end;
- ignore (type_predicate_named p)
+ ignore (type_predicate p)
(******************************************************************************)
(** {2 Getters} *)
@@ -564,7 +564,7 @@ let type_named_predicate ?(must_clear=true) p =
let get_integer_ty t = (Memo.get t).ty
let get_integer_op t = (Memo.get t).op
-let get_integer_op_of_predicate p = (type_predicate_named p).op
+let get_integer_op_of_predicate p = (type_predicate p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
let extract_typ t ty =
@@ -593,7 +593,7 @@ let get_cast t =
with Not_an_integer -> None
let get_cast_of_predicate p =
- let info = type_predicate_named p in
+ let info = type_predicate p in
try Extlib.opt_map typ_of_integer_ty info.cast
with Not_an_integer -> assert false
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index de5d764a9f708a94b57342f4d5951abbe29fa214..177e4f99acd6983fde71a8ce88124f73b24d5f27 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -86,7 +86,7 @@ val type_term: force:bool -> ?ctx:integer_ty -> term -> unit
[force] is true, then the conversion to the given context is done even if
-e-acsl-gmp-only is set. *)
-val type_named_predicate: ?must_clear:bool -> predicate named -> unit
+val type_named_predicate: ?must_clear:bool -> predicate -> unit
(** Compute the type of each term of the given predicate.
Set {!must_clear} to false in order to not reset the environment. *)
@@ -107,7 +107,7 @@ val get_integer_op: term -> integer_ty
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
-val get_integer_op_of_predicate: predicate named -> integer_ty
+val get_integer_op_of_predicate: predicate -> integer_ty
(** @return the infered type for the top operation of the given predicate. *)
val get_typ: term -> typ
@@ -120,7 +120,7 @@ val get_op: term -> typ
val get_cast: term -> typ option
(** Get the type which the given term must be converted to (if any). *)
-val get_cast_of_predicate: predicate named -> typ option
+val get_cast_of_predicate: predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
(******************************************************************************)
@@ -128,7 +128,7 @@ val get_cast_of_predicate: predicate named -> typ option
(******************************************************************************)
val compute_quantif_guards_ref
- : (predicate named -> logic_var list -> predicate named ->
+ : (predicate -> logic_var list -> predicate ->
(term * relation * logic_var * relation * term) list) ref
(** Forward reference. *)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a8eb4c67809ef712e843c756b2c818103fdf294b..76f6840b162814830308c023a5df791aa9c8120a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -737,7 +737,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| _ -> ());
t)
- method !vpredicate _ =
+ method !vpredicate_node _ =
Cil.DoChildrenPost
(function
| Pat(_, StmtLabel s_ref) as p ->