From 8fc44564d35fb6ba10d54fab2ba8b5cbfed2f2e3 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 27 Aug 2020 16:53:30 +0200
Subject: [PATCH] [rte] refined condition for generating pointer value alarms
presence of an offset does not mean that we could write a spurious value through
a union.
---
src/plugins/rte/rte.ml | 7 ++++++-
tests/rte/invalid_fptr.i | 15 +++++++++++++++
tests/rte/oracle/invalid_fptr.res.oracle | 20 ++++++++++++++++++++
3 files changed, 41 insertions(+), 1 deletion(-)
create mode 100644 tests/rte/invalid_fptr.i
create mode 100644 tests/rte/oracle/invalid_fptr.res.oracle
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 16845eed8d5..bc526753f36 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -451,13 +451,18 @@ let finite_float_assertion ~remove_trivial:_ ~on_alarm (fkind, exp) =
let pointer_call ~remove_trivial:_ ~on_alarm (e, args) =
on_alarm ~invalid:false (Alarms.Function_pointer (e, Some args))
+let rec is_safe_offset = function
+ | NoOffset -> true
+ | Field(fi,o) -> fi.fcomp.cstruct && not fi.faddrof && is_safe_offset o
+ | Index(_,o) -> is_safe_offset o
+
let is_safe_pointer_value = function
| Lval (Var vi, offset) ->
(* Reading a pointer variable must emit an alarm if an invalid pointer value
could have been written without previous alarm, through:
- an union type, in which case [offset] is not NoOffset;
- an untyped write, in which case the address of [vi] is taken. *)
- not vi.vaddrof && offset = NoOffset
+ not vi.vaddrof && is_safe_offset offset
| AddrOf (_, NoOffset) | StartOf (_, NoOffset) -> true
| CastE (_typ, e) ->
(* 0 can always be converted into a NULL pointer. *)
diff --git a/tests/rte/invalid_fptr.i b/tests/rte/invalid_fptr.i
new file mode 100644
index 00000000000..45f779e17a2
--- /dev/null
+++ b/tests/rte/invalid_fptr.i
@@ -0,0 +1,15 @@
+/* run.config
+OPT: -rte -warn-invalid-pointer -print
+*/
+
+struct S { void (*f)(void); } s;
+
+void (*p)(void);
+
+void f(void) {
+ if (p) return; // should not warn
+ if (p+2) return; // should warn
+ if (s.f) return; //should not warn
+ if (s.f+2) return; // should warn
+ return;
+}
diff --git a/tests/rte/oracle/invalid_fptr.res.oracle b/tests/rte/oracle/invalid_fptr.res.oracle
new file mode 100644
index 00000000000..d8e8029a754
--- /dev/null
+++ b/tests/rte/oracle/invalid_fptr.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/rte/invalid_fptr.i (no preprocessing)
+[rte] annotating function f
+/* Generated by Frama-C */
+struct S {
+ void (*f)(void) ;
+};
+struct S s;
+void (*p)(void);
+void f(void)
+{
+ if (p) goto return_label;
+ /*@ assert rte: pointer_value: \valid_function(p + 2); */
+ if (p + 2) goto return_label;
+ if (s.f) goto return_label;
+ /*@ assert rte: pointer_value: \valid_function(s.f + 2); */
+ if (s.f + 2) goto return_label;
+ return_label: return;
+}
+
+
--
GitLab