From 953dc568865b5ffed4df4b9f4a9173b6fb9fcbee Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 9 Jun 2016 10:35:36 +0200
Subject: [PATCH] [doc] improve doc of MinusPP typing
---
src/plugins/e-acsl/interval.ml | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 6037ecd4764..d8aa1f987ab 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -211,7 +211,10 @@ let rec infer t =
| TBinOp (MinusPP, t, _) ->
(match Cil.unrollType (get_cty t) with
| TArray(_, _, { scache = Computed n (* size in bits *) }, _) ->
- make Integer.zero (Integer.div (Integer.of_int n) Integer.eight)
+ (* the second argument must be in the same block than [t]. Consequently
+ the result of the difference belongs to [0; \block_length(t)] *)
+ let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+ make Integer.zero (Integer.of_int nb_bytes)
| TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tblock_length (_, t)
--
GitLab