diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml index 16845eed8d574889527464bbff6a589dcd4c9b0b..bc526753f3612bf6fefef2d0bc0c6c752a1437eb 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 0000000000000000000000000000000000000000..45f779e17a2647a051a1572887ba4352dadba1c5 --- /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 0000000000000000000000000000000000000000..d8e8029a75405d138282c47ac34ad0d709c6ce25 --- /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; +} + +