From 63f85c069d23cb418185c398ddd74cc131d4feca Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 29 Apr 2020 15:13:09 +0200
Subject: [PATCH] [eacsl:analyses] Complete `Interval.infer` to support
remaining bitwise operations
---
src/plugins/e-acsl/src/analyses/interval.ml | 20 ++++++++++++++++----
1 file changed, 16 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 54d7f8e5af4..91043aca76a 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -253,7 +253,10 @@ let ikind_of_ival iv =
| None, None -> raise Cil.Not_representable (* GMP *)
(* TODO: do not raise an exception, but returns a value instead *)
| None, Some _ | Some _, None ->
- Kernel.fatal ~current:true "unexpected ival: %a" Ival.pretty iv
+ (* Semi-open interval that can happen when computing the interval of shift
+ operations if the computation overflows *)
+ (* TODO: do not raise an exception, but returns a value instead *)
+ raise Cil.Not_representable (* GMP *)
(* function call profiles (intervals for their formal parameters) *)
module Profile = struct
@@ -456,9 +459,18 @@ let rec infer t =
let i1 = infer t1 in
let i2 = infer t2 in
lift_binop ~safe_float:false Ival.c_rem i1 i2
- | TBinOp (Shiftlt , _, _) -> Error.not_yet "right shift"
- | TBinOp (Shiftrt , _, _) -> Error.not_yet "left shift"
- | TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
+ | TBinOp (Shiftlt, t1, t2) ->
+ let i1 = infer t1 in
+ let i2 = infer t2 in
+ lift_binop ~safe_float:false Ival.shift_left i1 i2
+ | TBinOp (Shiftrt, t1, t2) ->
+ let i1 = infer t1 in
+ let i2 = infer t2 in
+ lift_binop ~safe_float:false Ival.shift_right i1 i2
+ | TBinOp (BAnd, t1, t2) ->
+ let i1 = infer t1 in
+ let i2 = infer t2 in
+ lift_binop ~safe_float:false Ival.bitwise_and i1 i2
| TBinOp (BXor, t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
--
GitLab