From bf154b79747d55c65bf8172003dd07550d785d5d Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Thu, 18 Apr 2019 16:11:47 +0200
Subject: [PATCH] supression of TCoerce, TCoerceE, PLcoercion and PLCoercionE
---
src/kernel_internals/parsing/logic_parser.mly | 4 ---
src/kernel_services/analysis/logic_interp.ml | 6 ++--
src/kernel_services/ast_data/cil_types.mli | 2 --
.../ast_printing/cil_printer.ml | 8 -----
.../ast_printing/cil_types_debug.ml | 4 ---
.../ast_printing/logic_print.ml | 5 ---
src/kernel_services/ast_queries/cil.ml | 12 +------
.../ast_queries/cil_datatype.ml | 16 +---------
.../ast_queries/logic_typing.ml | 21 +++---------
.../ast_queries/logic_utils.ml | 32 +++----------------
src/kernel_services/parsetree/logic_ptree.mli | 4 ---
src/plugins/value/legacy/eval_terms.ml | 1 -
src/plugins/wp/LogicSemantics.ml | 4 ---
src/plugins/wp/RefUsage.ml | 4 ---
14 files changed, 14 insertions(+), 109 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index dd7a194c057..4a0a607b3e7 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -525,10 +525,6 @@ lexpr_inner:
| LPAR range RPAR { info $2.lexpr_node }
| LPAR cast_logic_type RPAR lexpr_inner %prec prec_cast
{ info (PLcast ($2, $4)) }
-| lexpr_inner COLONGT logic_type
- { info (PLcoercion ($1, $3)) }
-| lexpr_inner COLONGT lexpr_inner %prec prec_cast
- { info (PLcoercionE ($1, $3)) }
| TYPEOF LPAR lexpr RPAR { info (PLtypeof $3) }
| BSTYPE LPAR type_spec RPAR { info (PLtype $3) }
| BSTYPE LPAR type_spec stars RPAR { info (PLtype ($4 $3)) }
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index bb41ed0466e..bb821242ae4 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -322,7 +322,7 @@ and loc_to_exp ~result {term_node = lnode ; term_type = ltype; term_loc = loc} =
| Tbase_addr _
| Toffset _
| Tblock_length _
- | TCoerce _ | TCoerceE _ | TUpdate _ | Ttypeof _ | Ttype _
+ | TUpdate _ | Ttypeof _ | Ttype _
| TLogic_coerce _
-> error_lval ()
@@ -346,7 +346,7 @@ let rec loc_to_lval ~result t =
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
| TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Tat _ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull | Trange _
- | TCoerce _ | TCoerceE _ | TDataCons _ | TUpdate _ | Tlambda _
+ | TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tlet _ | TLogic_coerce _ ->
error_lval ()
@@ -369,7 +369,7 @@ let loc_to_offset ~result loc =
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
| TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull
- | TCoerce _ | TCoerceE _ | TDataCons _ | TUpdate _ | Tlambda _
+ | TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tcomprehension _ | Tinter _ | Tlet _
| TLogic_coerce _
-> error_lval ()
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 405a2f547d2..99c30feec37 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1403,8 +1403,6 @@ and term_node =
The logic type must not be a Ctype. In particular, used to denote
lifting to Linteger and Lreal.
*)
- | TCoerce of term * typ (** coercion to a given C type. *)
- | TCoerceE of term * term (** coercion to the type of a given term. *)
| TUpdate of term * term_offset * term
(** functional update of a field. *)
| Ttypeof of term (** type tag for a term. *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 0d6c7ecce00..8b7bd79e84d 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -276,8 +276,6 @@ module Precedence = struct
| TAddrOf(_) -> addrOfLevel
| TStartOf(_) -> 30
| TUnOp((Neg|BNot|LNot),_) -> 30
- (* Unary post *)
- | TCoerce _ | TCoerceE _ -> 25
(* Lvals *)
| TLval(TMem _ , _) -> derefStarLevel
| TLval(TVar _, (TField _|TIndex _|TModel _)) -> indexLevel
@@ -2323,12 +2321,6 @@ class cil_printer () = object (self)
fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\block_length"
self#labels [l] self#term t
| Tnull -> self#pp_acsl_keyword fmt "\\null"
- | TCoerce (e,ty) ->
- fprintf fmt "%a@ :>@ %a"
- (self#term_prec current_level) e (self#typ None) ty
- | TCoerceE (e,ce) ->
- fprintf fmt "%a :> %a"
- (self#term_prec current_level) e (self#term_prec current_level) ce
| TUpdate (t,toff,v) ->
fprintf fmt "{%a %a %a = %a}"
self#term t
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 147e26274ed..a257df94803 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -699,10 +699,6 @@ and pp_term_node fmt = function
| Tnull -> Format.fprintf fmt "Tnull"
| TLogic_coerce(logic_type,term) ->
Format.fprintf fmt "TLogic_coerce(%a,%a)" pp_logic_type logic_type pp_term term
- | TCoerce(term,typ) ->
- Format.fprintf fmt "TCoerce(%a,%a)" pp_term term pp_typ typ
- | TCoerceE(term1,term2) ->
- Format.fprintf fmt "TCoerceE(%a,%a)" pp_term term1 pp_term term2
| TUpdate(term1,term_offset,term2) ->
Format.fprintf fmt "TUpdate(%a,%a,%a)" pp_term term1 pp_term_offset term_offset pp_term term2
| Ttypeof(term) -> Format.fprintf fmt "Ttypeof(%a)" pp_term term
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index b59c4b76f70..4f859eb0d5a 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -124,7 +124,6 @@ let getParenthLevel e =
| PLbinop (_,(Badd|Bsub|Blshift|Brshift),_) -> 60
| PLbinop (_,(Bmul|Bdiv|Bmod),_) -> 40
| PLunop ((Uamp|Uminus|Ubw_not),_) | PLcast _ | PLnot _ -> 30
- | PLcoercion _ | PLcoercionE _ -> 25
| PLunop (Ustar,_) | PLdot _ | PLarrow _ | PLarrget _
| PLsizeof _ | PLsizeofE _ -> 20
| PLapp _ | PLold _ | PLat _
@@ -217,10 +216,6 @@ and print_lexpr_level n fmt e =
(pp_opt print_lexpr) e1 (pp_opt print_lexpr) e2
| PLsizeof t -> fprintf fmt "sizeof(@;@[%a@]@;)" (print_logic_type None) t
| PLsizeofE e -> fprintf fmt "sizeof(@;@[%a@]@;)" print_lexpr_plain e
- | PLcoercion(e,t) ->
- fprintf fmt "%a@ :>@ %a" print_lexpr e (print_logic_type None) t
- | PLcoercionE(e1,e2) ->
- fprintf fmt "%a@ :>@ %a" print_lexpr e1 print_lexpr e2
| PLupdate(e1,path,e2) ->
fprintf fmt "{@ @[%a@ \\with@ %a@]}"
print_lexpr_plain e1 print_path_val (path, e2)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a166a49b5ec..ac3f9c46927 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2485,14 +2485,6 @@ and childrenTermNode vis tn =
let t' = vTerm t in
if t' != t || s' != s then Tblock_length (s',t') else tn
| Tnull -> tn
- | TCoerce(te,ty) ->
- let ty' = vTyp ty in
- let te' = vTerm te in
- if ty' != ty || te' != te then TCoerce(te',ty') else tn
- | TCoerceE(te,tc) ->
- let tc' = vTerm tc in
- let te' = vTerm te in
- if tc' != tc || te' != te then TCoerceE(te',tc') else tn
| TUpdate (tc,toff,te) ->
let tc' = vTerm tc in
let te' = vTerm te in
@@ -7765,10 +7757,8 @@ let rec free_vars_term bound_vars t = match t.term_node with
| Toffset (_,t)
| Tbase_addr (_,t)
| Tblock_length (_,t)
- | TCoerce (t,_)
| Ttypeof t -> free_vars_term bound_vars t
- | TBinOp (_,t1,t2)
- | TCoerceE (t1,t2) ->
+ | TBinOp (_,t1,t2) ->
Logic_var.Set.union
(free_vars_term bound_vars t1)
(free_vars_term bound_vars t2)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 86342ad91af..9dd7af1b0dc 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -108,8 +108,6 @@ let rank_term = function
| Tbase_addr _ -> 17
| Tblock_length _ -> 18
| Tnull -> 19
- | TCoerce _ -> 20
- | TCoerceE _ -> 21
| TUpdate _ -> 22
| Ttypeof _ -> 23
| Ttype _ -> 24
@@ -1562,12 +1560,6 @@ let rec compare_term t1 t2 =
let cl = compare_logic_label l1 l2 in
if cl <> 0 then cl else compare_term t1 t2
| Tnull , Tnull -> 0
- | TCoerce(t1,ty1) , TCoerce(t2,ty2) ->
- let ct = Typ.compare ty1 ty2 in
- if ct <> 0 then ct else compare_term t1 t2
- | TCoerceE(t1,ty1) , TCoerceE(t2,ty2) ->
- let ct = compare_term ty1 ty2 in
- if ct <> 0 then ct else compare_term t1 t2
| TUpdate(x1,off1,y1) , TUpdate(x2,off2,y2) ->
let cx = compare_term x1 x2 in
if cx <> 0 then cx else
@@ -1598,7 +1590,7 @@ let rec compare_term t1 t2 =
| TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
| Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
| Tbase_addr _ | Tblock_length _ | Toffset _
- | Tnull | TCoerce _ | TCoerceE _ | TUpdate _ | Ttypeof _
+ | Tnull | TUpdate _ | Ttypeof _
| Ttype _ | Tempty_set | Tunion _ | Tinter _ | Tcomprehension _
| Trange _ | Tlet _
| TLogic_coerce _), _ -> assert false
@@ -1727,12 +1719,6 @@ let rec hash_term (acc,depth,tot) t =
let hash = acc + 351 + hash_label l in
hash_term (hash,depth-1,tot-2) t
| Tnull -> acc+361, tot - 1
- | TCoerce(t,ty) ->
- let hash = Typ.hash ty in
- hash_term (acc+380+hash,depth-1,tot-2) t
- | TCoerceE(t1,t2) ->
- let hash1,tot1 = hash_term (acc+399,depth-1,tot-1) t1 in
- hash_term (hash1,depth-1,tot1) t2
| TUpdate(t1,off,t2) ->
let hash1,tot1 = hash_term (acc+418,depth-1,tot-1) t1 in
let hash2,tot2 = hash_toffset (hash1,depth-1,tot1) off in
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 6cd4dcee6f3..80d58f94a72 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1015,8 +1015,6 @@ struct
| TStartOf (_,o) -> needs_at_offset o
| Tapp(_,_,l) | TDataCons(_,l) -> List.exists needs_at l
| Tlambda(_,t) -> needs_at t
- | TCoerce(t,_) -> needs_at t
- | TCoerceE(t,_) -> needs_at t
| TUpdate(t1,o,t2) -> needs_at t1 || needs_at_offset o || needs_at t2
| Tunion l | Tinter l -> List.exists needs_at l
| Tcomprehension(t,_,None) -> needs_at t
@@ -2047,7 +2045,7 @@ struct
| TSizeOfStr _ | TAlignOf _ | TAlignOfE _
| TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
| Tapp _ | TDataCons _ | Tbase_addr _ | Toffset _
- | Tblock_length _ | Tnull | TCoerce _ | TCoerceE _
+ | Tblock_length _ | Tnull
| TUpdate _ | Ttypeof _ | Ttype _ | Tempty_set
(* [VP] I suppose that an union of functions
is theoretically possible but I'm not sure that we want to
@@ -2332,8 +2330,8 @@ struct
| Trange _ | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
| TAlignOfE _ | TUnOp (_,_) | TBinOp (_,_,_) | TCastE (_,_)
| TStartOf _ | Tlambda (_,_) | TDataCons (_,_) | Tbase_addr (_,_)
- | Toffset (_,_) | Tblock_length (_,_) | Tnull | Tapp _ | TCoerce (_,_)
- | TCoerceE (_,_) | TUpdate (_,_,_) | Ttypeof _ | Ttype _ ->
+ | Toffset (_,_) | Tblock_length (_,_) | Tnull | Tapp _
+ | TUpdate (_,_,_) | Ttypeof _ | Ttype _ ->
false
in
aux t
@@ -2869,17 +2867,6 @@ struct
let ct = Logic_const.unroll_ltdef (logic_type ctxt loc env ty) in
let { term_node; term_type } = mk_cast ~explicit:true t ct in
(term_node, term_type)
- | PLcoercion (t,ty) ->
- let t = term env t in
- (match Logic_const.unroll_ltdef (logic_type ctxt loc env ty) with
- | Ctype ty as cty
- -> TCoerce (t, ty), cty
- | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _ ->
- ctxt.error loc "cannot cast to logic type")
- | PLcoercionE (t,tc) ->
- let t = term env t in
- let tc = term env tc in
- TCoerceE (t, tc), tc.term_type
| PLrel (t1, (Eq | Neq | Lt | Le | Gt | Ge as op), t2) ->
let f _ op t1 t2 =
(TBinOp(binop_of_rel op, t1, t2),
@@ -3423,7 +3410,7 @@ struct
| PLcast _ | PLblock_length _ | PLbase_addr _ | PLoffset _
| PLrepeat _ | PLlist _ | PLarrget _ | PLarrow _
| PLdot _ | PLbinop _ | PLunop _ | PLconstant _
- | PLnull | PLresult | PLcoercion _ | PLcoercionE _ | PLsizeof _
+ | PLnull | PLresult | PLsizeof _
| PLsizeofE _ | PLlambda _
| PLupdate _ | PLinitIndex _ | PLinitField _
| PLtypeof _ | PLtype _ -> boolean_to_predicate ctxt env p0
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 1eef0ebab99..d85fd2d8704 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -778,10 +778,6 @@ let rec is_same_term t1 t2 =
| Toffset (l1,t1), Toffset (l2,t2)
| Tat(t1,l1), Tat(t2,l2) -> is_same_logic_label l1 l2 && is_same_term t1 t2
| Tnull, Tnull -> true
- | TCoerce(t1,typ1), TCoerce(t2,typ2) ->
- is_same_term t1 t2 && Cil_datatype.TypByName.equal typ1 typ2
- | TCoerceE(t1,tt1), TCoerceE(t2,tt2) ->
- is_same_term t1 t2 && is_same_term tt1 tt2
| Tlambda (v1,t1), Tlambda(v2,t2) ->
is_same_list is_same_var v1 v2 && is_same_term t1 t2
| TUpdate(t1,i1,nt1), TUpdate(t2,i2,nt2) ->
@@ -810,7 +806,7 @@ let rec is_same_term t1 t2 =
| TAlignOf _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _
| TAddrOf _ | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _
| Tif _ | Tat _ | Tbase_addr _ | Tblock_length _ | Toffset _ | Tnull
- | TCoerce _ | TCoerceE _ | TUpdate _ | Ttypeof _ | Ttype _
+ | TUpdate _ | Ttypeof _ | Ttype _
| Tcomprehension _ | Tempty_set | Tunion _ | Tinter _ | Trange _
| Tlet _ | TLogic_coerce _
),_ -> false
@@ -1212,14 +1208,12 @@ and is_same_lexpr l1 l2 =
| PLresult, PLresult | PLnull, PLnull
| PLfalse, PLfalse | PLtrue, PLtrue | PLempty, PLempty ->
true
- | PLcast(t1,e1), PLcast(t2,e2) | PLcoercion(e1,t1), PLcoercion (e2,t2)->
+ | PLcast(t1,e1), PLcast(t2,e2) ->
is_same_pl_type t1 t2 && is_same_lexpr e1 e2
| PLrange(l1,h1), PLrange(l2,h2) ->
is_same_opt is_same_lexpr l1 l2 && is_same_opt is_same_lexpr h1 h2
| PLsizeof t1, PLsizeof t2 -> is_same_pl_type t1 t2
| PLsizeofE e1,PLsizeofE e2 | PLtypeof e1,PLtypeof e2-> is_same_lexpr e1 e2
- | PLcoercionE (b1,t1), PLcoercionE(b2,t2) ->
- is_same_lexpr b1 b2 && is_same_lexpr t1 t2
| PLupdate(b1,p1,r1), PLupdate(b2,p2,r2) ->
is_same_lexpr b1 b2
&& is_same_list is_same_path_elt p1 p2 && is_same_update_term r1 r2
@@ -1270,8 +1264,8 @@ and is_same_lexpr l1 l2 =
| PLold _ | PLat _
| PLbase_addr _ | PLblock_length _ | PLoffset _
| PLresult | PLnull | PLcast _
- | PLrange _ | PLsizeof _ | PLsizeofE _ | PLtypeof _ | PLcoercion _
- | PLcoercionE _ | PLupdate _ | PLinitIndex _ | PLtype _ | PLfalse
+ | PLrange _ | PLsizeof _ | PLsizeofE _ | PLtypeof _
+ | PLupdate _ | PLinitIndex _ | PLtype _ | PLfalse
| PLtrue | PLinitField _ | PLrel _ | PLand _ | PLor _ | PLxor _
| PLimplies _ | PLiff _ | PLnot _ | PLif _ | PLforall _
| PLexists _ | PLvalid _ | PLvalid_read _ | PLvalid_function _
@@ -1348,12 +1342,6 @@ let rec hash_term (acc,depth,tot) t =
let hash = acc + 351 + hash_label l in
hash_term (hash,depth-1,tot-2) t
| Tnull -> acc+361, tot - 1
- | TCoerce(t,ty) ->
- let hash = Cil_datatype.TypByName.hash ty in
- hash_term (acc+380+hash,depth-1,tot-2) t
- | TCoerceE(t1,t2) ->
- let hash1,tot1 = hash_term (acc+399,depth-1,tot-1) t1 in
- hash_term (hash1,depth-1,tot1) t2
| TUpdate(t1,off,t2) ->
let hash1,tot1 = hash_term (acc+418,depth-1,tot-1) t1 in
let hash2,tot2 = hash_term_offset (hash1,depth-1,tot1) off in
@@ -1594,16 +1582,6 @@ let rec compare_term t1 t2 =
| Tnull, Tnull -> 0
| Tnull, _ -> 1
| _, Tnull -> -1
- | TCoerce(t1,typ1), TCoerce(t2,typ2) ->
- let res = compare_term t1 t2 in
- if res = 0 then Cil_datatype.TypByName.compare typ1 typ2 else res
- | TCoerce _, _ -> 1
- | _, TCoerce _ -> -1
- | TCoerceE(t1,tt1), TCoerceE(t2,tt2) ->
- let res = compare_term t1 t2 in
- if res = 0 then compare_term tt1 tt2 else res
- | TCoerceE _, _ -> 1
- | _, TCoerceE _ -> -1
| Tlambda (v1,t1), Tlambda(v2,t2) ->
let res = Extlib.list_compare compare_var v1 v2 in
if res = 0 then compare_term t1 t2 else res
@@ -2290,7 +2268,7 @@ let rec constFoldTermToInt ?(machdep=true) (e: term) : Integer.t option =
constFoldMinMax ~machdep Integer.min args
| TLval _ | TAddrOf _ | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _
- | Tat _ | Tbase_addr _ | Tblock_length _ | TCoerce _ | TCoerceE _
+ | Tat _ | Tbase_addr _ | Tblock_length _
| TUpdate _ | Ttypeof _ | Ttype _ | Tempty_set | Tunion _ | Tinter _
| Tcomprehension _ | Trange _ | Tlet _ ->
None
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 35aec8c31fc..261788e5fe2 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -107,10 +107,6 @@ and lexpr_node =
| PLrange of lexpr option * lexpr option (** interval of integers. *)
| PLsizeof of logic_type (** sizeof a type. *)
| PLsizeofE of lexpr (** sizeof the type of an expression. *)
- | PLcoercion of lexpr * logic_type
- (** coercion of an expression in a given type. *)
- | PLcoercionE of lexpr * lexpr
- (** coercion of the first expression into the type of the second one. *)
| PLupdate of lexpr * (path_elt list) * update_term
(** functional update of the field of a structure. *)
| PLinitIndex of (lexpr * lexpr) list (** array constructor. *)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 863d1a5e8fc..14de9d26666 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1002,7 +1002,6 @@ let rec eval_term ~alarm_mode env t =
| Tlambda _ -> unsupported "logic functions or predicates"
| TUpdate _ -> unsupported "functional updates"
- | TCoerce _ | TCoerceE _ -> unsupported "logic coercions" (* jessie *)
| Ttype _ -> unsupported "\\type operator"
| Ttypeof _ -> unsupported "\\typeof operator"
| Tcomprehension _ -> unsupported "sets defined by comprehension"
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 886549d1abf..e8f8b966ba2 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -681,8 +681,6 @@ struct
| TUnOp(unop,t) -> term_unop unop (C.logic env t)
| TBinOp(binop,a,b) -> term_binop env binop a b
- | TCoerceE (t,e) -> term_cast_to_ltype env e.term_type t (** Jessie only, to be deprecated *)
- | TCoerce (t,ty) -> term_cast_to_ctype env ty t (** Jessie only, to be deprecated *)
| TCastE(ty,t) -> term_cast_to_ctype env ty t
| TLogic_coerce(typ,t) -> term_cast_to_ltype env typ t
@@ -961,8 +959,6 @@ struct
Warning.error "Complex let-binding not implemented yet (%a)"
Printer.pp_term t
- | TCoerce (t,_) (** Jessie only, to be deprecated *)
- | TCoerceE (t,_) (** Jessie only, to be deprecated *)
| TCastE (_,t)
| TLogic_coerce(_,t) -> C.region env ~unfold t
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 3b0cf1f9c90..47761ae4794 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -406,10 +406,6 @@ and term (env:ctx) (t:term) : model = match t.term_node with
| TCastE(ty_tgt,t) -> cast (cast_ltyp ty_tgt t.term_type) (term env t)
| TLogic_coerce (_lt,t) -> term env t
- (* Jessie *)
- | TCoerce _ -> Wp_parameters.fatal "Coercions: TCoerc _"
- | TCoerceE _ -> Wp_parameters.fatal "Coercions: TCoerceE _"
-
(* Term L-Values *)
| TLval tlv -> term_lval env tlv
--
GitLab