diff --git a/tests/rte/invalid_fptr.i b/tests/rte/invalid_fptr.i index 45f779e17a2647a051a1572887ba4352dadba1c5..c28d93b0ed1dfc232e053144dd4998f834f8b5f0 100644 --- a/tests/rte/invalid_fptr.i +++ b/tests/rte/invalid_fptr.i @@ -1,9 +1,11 @@ /* run.config -OPT: -rte -warn-invalid-pointer -print +OPT: -c11 -rte -warn-invalid-pointer -print */ struct S { void (*f)(void); } s; +struct S1 { void(*f)(void); } s1; + void (*p)(void); void f(void) { @@ -13,3 +15,23 @@ void f(void) { if (s.f+2) return; // should warn return; } + +struct { union { void(*g)(void); unsigned int x; }; } s2; + +struct { void (*tab[12])(void); } s3; + +void write_something(void *x); + +void h() { + write_something(&s1.f); + write_something(&s3.tab[4]); +} + +//all the pointers below can have their value set to an invalid pointer without +// generating a warning at write site, hence a warning should be generated +// at read access. +void g(void) { + if (s2.g) return; + if (s1.f) return; + if (s3.tab[4]) return; +} diff --git a/tests/rte/oracle/invalid_fptr.res.oracle b/tests/rte/oracle/invalid_fptr.res.oracle index d8e8029a75405d138282c47ac34ad0d709c6ce25..c1d6edf050a78c04f869915aba22205ed6fe211c 100644 --- a/tests/rte/oracle/invalid_fptr.res.oracle +++ b/tests/rte/oracle/invalid_fptr.res.oracle @@ -1,10 +1,26 @@ [kernel] Parsing tests/rte/invalid_fptr.i (no preprocessing) [rte] annotating function f +[rte] annotating function g +[rte] annotating function h /* Generated by Frama-C */ struct S { void (*f)(void) ; }; +struct S1 { + void (*f)(void) ; +}; +union __anonunion_2 { + void (*g)(void) ; + unsigned int x ; +}; +struct __anonstruct_s2_1 { + union __anonunion_2 __anonCompField1 ; +}; +struct __anonstruct_s3_3 { + void (*tab[12])(void) ; +}; struct S s; +struct S1 s1; void (*p)(void); void f(void) { @@ -17,4 +33,28 @@ void f(void) return_label: return; } +struct __anonstruct_s2_1 s2; +struct __anonstruct_s3_3 s3; +void write_something(void *x); + +void h(void) +{ + /*@ assert rte: pointer_value: \object_pointer(&s1.f); */ + write_something((void *)(& s1.f)); + /*@ assert rte: pointer_value: \object_pointer(&s3.tab[4]); */ + write_something((void *)(& s3.tab[4])); + return; +} + +void g(void) +{ + /*@ assert rte: pointer_value: \valid_function(s2.__anonCompField1.g); */ + if (s2.__anonCompField1.g) goto return_label; + /*@ assert rte: pointer_value: \valid_function(s1.f); */ + if (s1.f) goto return_label; + /*@ assert rte: pointer_value: \valid_function(s3.tab[4]); */ + if (s3.tab[4]) goto return_label; + return_label: return; +} +