From c2be7fad142bff70f670263d34c9d2f326697b5b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 26 Mar 2020 12:01:35 +0100
Subject: [PATCH] [Kernel] Alarms: new overflow_kind for pointer downcasts.
---
src/kernel_services/ast_data/alarms.ml | 8 +++++++-
src/kernel_services/ast_data/alarms.mli | 7 ++++---
src/plugins/value/alarmset.ml | 1 +
3 files changed, 12 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ae9503e76ad..445efc3204d 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -23,7 +23,8 @@
open Cil_types
open Cil_datatype
-type overflow_kind = Signed | Unsigned | Signed_downcast | Unsigned_downcast
+type overflow_kind =
+ Signed | Unsigned | Signed_downcast | Unsigned_downcast | Pointer_downcast
type access_kind = For_reading | For_writing
type bound_kind = Lower_bound | Upper_bound
@@ -32,6 +33,7 @@ let string_of_overflow_kind = function
| Unsigned -> "unsigned_overflow"
| Signed_downcast -> "signed_downcast"
| Unsigned_downcast -> "unsigned_downcast"
+ | Pointer_downcast -> "pointer_downcast"
type alarm =
| Division_by_zero of exp
@@ -549,6 +551,10 @@ let create_predicate ?(loc=Location.unknown) alarm =
(* n <= e or e <= n according to bound *)
let loc = best_loc ~loc e.eloc in
let t = match kind with
+ | Pointer_downcast ->
+ let t = Logic_utils.expr_to_term ~cast:true e in
+ let typ = Cil.theMachine.upointType in
+ Logic_const.tlogic_coerce ~loc t (Ctype typ)
| Signed_downcast | Unsigned_downcast ->
Logic_utils.expr_to_term ~cast:true e
| _ ->
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index c301b2e797c..a369dc60f2b 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -25,9 +25,10 @@
open Cil_types
-(** Only signed overflows int are really RTEs. The other kinds may be
- meaningful nevertheless. *)
-type overflow_kind = Signed | Unsigned | Signed_downcast | Unsigned_downcast
+(** Only signed overflows and pointer downcasts are really RTEs.
+ The other kinds may be meaningful nevertheless. *)
+type overflow_kind =
+ Signed | Unsigned | Signed_downcast | Unsigned_downcast | Pointer_downcast
type access_kind = For_reading | For_writing
type bound_kind = Lower_bound | Upper_bound
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index fa27012f076..1738ac4a35a 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -309,6 +309,7 @@ let emit_alarm kinstr alarm (status:status) =
| Alarms.Unsigned -> "unsigned overflow"
| Alarms.Signed_downcast -> "signed downcast"
| Alarms.Unsigned_downcast -> "unsigned downcast"
+ | Alarms.Pointer_downcast -> "pointer downcast"
in
register_alarm str
--
GitLab