[typing] fix typing of \offset

src/plugins/e-acsl/interval.ml

@@ -209,7 +209,8 @@ let rec infer env t =
       make Integer.zero (Integer.div (Integer.of_int n) Integer.eight)
     | TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
     | _ -> assert false)
-  | Tblock_length (_, t) ->
+  | Tblock_length (_, t)
+  | Toffset(_, t) ->
     (match Cil.unrollType (get_cty t) with
     | TArray(_, _, { scache = Computed n }, _) ->
       let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
@@ -236,7 +237,6 @@ let rec infer env t =
   | TBinOp (MinusPI,_,_)
   | TAddrOf _
   | TStartOf _
-  | Toffset _
   | Tlambda (_,_)
   | TDataCons (_,_)
   | Tbase_addr (_,_)

src/plugins/e-acsl/typing.ml

@@ -191,6 +191,7 @@ let rec type_term env ~ctx t =
        with Interval.Not_an_integer ->
          Other)
 
+    | Toffset(_, t')
     | Tblock_length(_, t')
     | TSizeOfE t'
     | TAlignOfE t' ->
@@ -306,7 +307,6 @@ let rec type_term env ~ctx t =
       type_term_lval env tlv;
       Other
 
-    | Toffset(_, t)
     | Tbase_addr (_, t) ->
       (* it is a pointer, as well as [t], but [t] must be typed. *)
       ignore (type_term env ~ctx:Other t);