From a326aa6b34747dcdf9edaa2372153af009e19149 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 22 Mar 2016 13:31:10 +0100
Subject: [PATCH] [typing] fix typing of \offset
---
src/plugins/e-acsl/interval.ml | 4 ++--
src/plugins/e-acsl/typing.ml | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index eedb1df7865..2617a9ad41b 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/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 (_,_)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 7d4c9ab576d..bd19b068fdc 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/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);
--
GitLab