Correction of pattern matching, add TCastE(_,_) to avoid warning

src/plugins/e-acsl/interval.ml

@@ -135,7 +135,6 @@ let rec infer t =
     let i1 = infer t1 in
     let i2 = infer t2 in
     Ival.bitwise_or i1 i2
-  | TCastE (ty, t)
   | Tif (_, t2, t3) ->
     let i2 = infer t2 in
     let i3 = infer t3 in
@@ -197,7 +196,8 @@ let rec infer t =
   | TUpdate (_,_,_)
   | Ttypeof _
   | Ttype _
-  | Tempty_set  -> raise Not_an_integer
+  | Tempty_set
+  | TCastE (_,_) -> raise Not_an_integer
 
 and infer_term_lval (host, offset as tlv) =
   match offset with

src/plugins/e-acsl/typing.ml

@@ -414,20 +414,6 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
     | TLogic_coerce (_, t) ->
       dup (type_term ~use_gmp_opt ~arith_operand ?ctx t).ty
 
-    | TCoerceE (t1, t2) ->
-      let ctx =
-        try
-          let i = Interval.infer t in
-          let i1 = Interval.infer t1 in
-          let i2 = Interval.infer t2 in
-          ty_of_interv ?ctx (Ival.join i (Ival.join i1 i2))
-        with Interval.Not_an_integer ->
-          Other
-      in
-      ignore (type_term ~use_gmp_opt:true ~ctx t1);
-      ignore (type_term ~use_gmp_opt:true ~ctx t2);
-      dup ctx
-
     | TAddrOf tlv
     | TStartOf tlv ->
       (* it is a pointer, but subterms must be typed. *)
@@ -480,7 +466,8 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
     | TConst (LStr _ | LWStr _ | LReal _)
     | Ttypeof _
     | Ttype _
-    | Tempty_set  -> dup Other
+    | Tempty_set
+    | TCastE (_,_) -> dup Other
   in
   Memo.memo
     (fun t ->