[Kernel] Ensures that infer_annotations assigns \result for ghost functions

src/kernel_internals/typing/infer_annotations.ml

@@ -142,9 +142,10 @@ let assigns_from_prototype kf =
       (fun (g, t) acc -> if g then acc else t :: acc) inputs []
   in
   let inputs = List.map (fun (_g, t) -> t) inputs in
+  let inputs g = if g then inputs else inputs_no_ghost in
   let arguments =
     List.map
-      (fun (g, content) -> content, From (if g then inputs else inputs_no_ghost))
+      (fun (g, content) -> content, From (inputs g))
       to_assign
   in
   match rtyp with
@@ -155,7 +156,7 @@ let assigns_from_prototype kf =
     (* assigns result from basic args and content of pointer args *)
     let loc = vi.vdecl in
     let result = Logic_const.(new_identified_term (tresult ~loc rtyp)) in
-    (result, From inputs_no_ghost):: arguments
+    (result, From (inputs vi.vghost)):: arguments
 
 let is_frama_c_builtin name =
   Ast_info.is_frama_c_builtin name

tests/spec/assigns_from_kf.i

@@ -12,8 +12,17 @@ void something_ghost(void) /*@ ghost (int* p) */;
 int something_non_ghost_r(int *p);
 int something_ghost_r(void) /*@ ghost (int* p) */;
 
-void both(int* p, int x) /*@ ghost (int* gp, int gx) */;
-int both_r(int* p, int x) /*@ ghost (int* gp, int gx) */;
+void both(int *p, int x) /*@ ghost (int* gp, int gx) */;
+int both_r(int *p, int x) /*@ ghost (int* gp, int gx) */;
+
+/*@ ghost
+  void g_nothing(void);
+  int g_nothing_r(void);
+  void g_something_non_ghost(int *p);
+  int g_something_non_ghost_r(int *p);
+  void g_both(int *p, int x, int *gp, int gx);
+  int g_both_r(int *p, int x, int *gp, int gx);
+*/
 
 void reference(void) {
   nothing();
@@ -24,4 +33,13 @@ void reference(void) {
   something_ghost_r() /*@ ghost (0) */;
   both(0, 1) /*@ ghost (0, 2) */;
   both_r(0, 1) /*@ ghost (0, 2) */;
+
+  /*@ ghost
+    g_nothing();
+    g_nothing_r();
+    g_something_non_ghost(0);
+    g_something_non_ghost_r(0);
+    g_both(0, 1, 0, 2);
+    g_both_r(0, 1, 0, 2);
+  */
 }
\ No newline at end of file

tests/spec/oracle/assigns_from_kf.res.oracle

 [kernel] Parsing tests/spec/assigns_from_kf.i (no preprocessing)
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function both, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function both_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+  Neither code nor specification for function g_both, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+  Neither code nor specification for function g_both_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+  Neither code nor specification for function g_nothing, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+  Neither code nor specification for function g_nothing_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+  Neither code nor specification for function g_something_non_ghost, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
+  Neither code nor specification for function g_something_non_ghost_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function nothing, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function nothing_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function something_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function something_ghost_r, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function something_non_ghost, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning: 
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:27: Warning: 
   Neither code nor specification for function something_non_ghost_r, generating default assigns from the prototype
 /* Generated by Frama-C */
 /*@ assigns \nothing; */
@@ -55,6 +67,40 @@ void both(int *p, int x) /*@ ghost (int *gp, int gx) */;
  */
 int both_r(int *p, int x) /*@ ghost (int *gp, int gx) */;
 
+/*@ ghost /@ assigns \nothing; @/
+void g_nothing(void); */
+
+/*@ ghost
+/@ assigns \result;
+   assigns \result \from \nothing; @/
+int g_nothing_r(void); */
+
+/*@ ghost
+/@ assigns *p;
+   assigns *p \from *p; @/
+void g_something_non_ghost(int *p); */
+
+/*@ ghost
+/@ assigns \result, *p;
+   assigns \result \from *p;
+   assigns *p \from *p; @/
+int g_something_non_ghost_r(int *p); */
+
+/*@ ghost
+/@ assigns *p, *gp;
+   assigns *p \from *p, *gp, x, gx;
+   assigns *gp \from *p, *gp, x, gx;
+ @/
+void g_both(int *p, int x, int *gp, int gx); */
+
+/*@ ghost
+/@ assigns \result, *p, *gp;
+   assigns \result \from *p, *gp, x, gx;
+   assigns *p \from *p, *gp, x, gx;
+   assigns *gp \from *p, *gp, x, gx;
+ @/
+int g_both_r(int *p, int x, int *gp, int gx); */
+
 void reference(void)
 {
   nothing();
@@ -65,6 +111,12 @@ void reference(void)
   something_ghost_r() /*@ ghost ((int *)0) */;
   both((int *)0,1) /*@ ghost ((int *)0,2) */;
   both_r((int *)0,1) /*@ ghost ((int *)0,2) */;
+  /*@ ghost g_nothing(); */
+  /*@ ghost g_nothing_r(); */
+  /*@ ghost g_something_non_ghost((int *)0); */
+  /*@ ghost g_something_non_ghost_r((int *)0); */
+  /*@ ghost g_both((int *)0,1,(int *)0,2); */
+  /*@ ghost g_both_r((int *)0,1,(int *)0,2); */
   return;
 }