[rte] add more test cases for pointer value alarm generation

tests/rte/invalid_fptr.i

 /* 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;
+}

tests/rte/oracle/invalid_fptr.res.oracle

 [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;
+}
+