[Eva] use callsite for populate_funspec locations

src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle

@@ -158,7 +158,7 @@
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: Warning: 
+[kernel:annot:missing-spec] parallel_threads.c:121: Warning: 
   Neither code nor specification for function pthread_mutex_trylock,
    generating default assigns. See -generated-spec-* options for more info
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning: 

src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle

@@ -158,7 +158,7 @@
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: Warning: 
+[kernel:annot:missing-spec] parallel_threads.c:121: Warning: 
   Neither code nor specification for function pthread_mutex_trylock,
    generating default assigns. See -generated-spec-* options for more info
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning: 

src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: Warning: 
+[kernel:annot:missing-spec] hidden_malloc.c:11: Warning: 
   Neither code nor specification for function realpath,
    generating default assigns. See -generated-spec-* options for more info

src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle

@@ -27,7 +27,7 @@
 [eva:alarm] t_fun_lib.c:15: Warning: 
   function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                         \valid(data->values) got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: Warning: 
+[kernel:annot:missing-spec] t_fun_lib.c:19: Warning: 
   Neither code nor specification for function realpath,
    generating default assigns. See -generated-spec-* options for more info
 [eva:alarm] t_fun_lib.c:22: Warning: 

src/plugins/eva/engine/function_calls.ml

@@ -154,8 +154,13 @@ let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
 
 (* Returns the function specification of [kf], with generated assigns clauses
    if they are missing. *)
-let get_funspec kf =
-  Populate_spec.populate_funspec ~do_body:true kf [`Assigns];
+let get_funspec callsite kf =
+  let loc =
+    match callsite with
+    | Kglobal -> None
+    | Kstmt stmt -> Some (Cil_datatype.Stmt.loc stmt)
+  in
+  Populate_spec.populate_funspec ?loc ~do_body:true kf [`Assigns];
   Annotations.funspec kf
 
 let analysis_target ~recursion_depth callsite kf =
@@ -166,14 +171,14 @@ let analysis_target ~recursion_depth callsite kf =
     if recursion_depth >= Parameters.RecursiveUnroll.get ()
     then begin
       Recursion.check_spec callsite kf;
-      `Spec (get_funspec kf)
+      `Spec (get_funspec callsite kf)
     end
     else
       match kf.fundec with
-      | Declaration _ -> `Spec (get_funspec kf)
+      | Declaration _ -> `Spec (get_funspec callsite kf)
       | Definition (def, _) ->
         if Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
-        then `Spec (get_funspec kf)
+        then `Spec (get_funspec callsite kf)
         else `Body (def, save_results def)
 
 let define_analysis_target ?(recursion_depth = -1) callsite kf  =

src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle

@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[kernel:annot:missing-spec] n5.i:9: Warning: 
+[kernel:annot:missing-spec] n5.i:21: Warning: 
   Neither code nor explicit assigns for function may_not_terminate,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function may_not_terminate <- main.
@@ -13,7 +13,7 @@
 [eva] Done for function may_not_terminate
 [eva] computing for function f <- main.
   Called from n5.i:22.
-[kernel:annot:missing-spec] n5.i:5: Warning: 
+[kernel:annot:missing-spec] n5.i:12: Warning: 
   Neither code nor explicit assigns for function never_terminates,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function never_terminates <- f <- main.

src/plugins/report/tests/report/oracle/csv.res.oracle

@@ -10,7 +10,7 @@
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
   Called from csv.c:55.
-[kernel:annot:missing-spec] csv.c:18: Warning: 
+[kernel:annot:missing-spec] csv.c:21: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f <- main2 <- main.

src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle

@@ -2,7 +2,7 @@
 [variadic] empty-vpar-with-ghost.i:8: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] empty-vpar-with-ghost.i:5: Warning: 
+[kernel:annot:missing-spec] empty-vpar-with-ghost.i:8: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle

 [variadic] empty-vpar.i:1: Declaration of variadic function f.
 [variadic] empty-vpar.i:8: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] empty-vpar.i:5: Warning: 
+[kernel:annot:missing-spec] empty-vpar.i:8: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle

@@ -2,7 +2,7 @@
 [variadic] function-ptr-with-ghost.i:2: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] function-ptr-with-ghost.i:4: Warning: 
+[kernel:annot:missing-spec] function-ptr-with-ghost.i:2: Warning: 
   Neither code nor specification for function va_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function va_f

src/plugins/variadic/tests/declared/oracle/label.res.oracle

 [variadic] label.i:4: Declaration of variadic function f.
 [variadic] label.i:8: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] label.i:4: Warning: 
+[kernel:annot:missing-spec] label.i:8: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/multi.res.oracle

@@ -3,11 +3,11 @@
 [variadic] multi.i:9: Generic translation of call to variadic function.
 [variadic] multi.i:18: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] multi.i:15: Warning: 
+[kernel:annot:missing-spec] multi.i:18: Warning: 
   Neither code nor explicit assigns for function g,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function g
-[kernel:annot:missing-spec] multi.i:6: Warning: 
+[kernel:annot:missing-spec] multi.i:9: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle

 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] no-va-with-ghost.i:1: Warning: 
+[kernel:annot:missing-spec] no-va-with-ghost.i:4: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/no-va.res.oracle

 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] no-va.i:1: Warning: 
+[kernel:annot:missing-spec] no-va.i:4: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle

@@ -2,7 +2,7 @@
 [variadic] rvalues-with-ghost.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] rvalues-with-ghost.i:1: Warning: 
+[kernel:annot:missing-spec] rvalues-with-ghost.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle

 [variadic] rvalues.i:1: Declaration of variadic function f.
 [variadic] rvalues.i:5: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] rvalues.i:1: Warning: 
+[kernel:annot:missing-spec] rvalues.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle

@@ -2,7 +2,7 @@
 [variadic] simple-with-ghost.i:9: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] simple-with-ghost.i:6: Warning: 
+[kernel:annot:missing-spec] simple-with-ghost.i:9: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/simple.res.oracle

 [variadic] simple.i:1: Declaration of variadic function f.
 [variadic] simple.i:9: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] simple.i:6: Warning: 
+[kernel:annot:missing-spec] simple.i:9: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/struct.res.oracle

 [variadic] struct.i:5: Declaration of variadic function f.
 [variadic] struct.i:10: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] struct.i:5: Warning: 
+[kernel:annot:missing-spec] struct.i:10: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f

src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle

@@ -3,7 +3,7 @@
 [variadic] typedefed_function-with-ghost.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] typedefed_function-with-ghost.i:2: Warning: 
+[kernel:annot:missing-spec] typedefed_function-with-ghost.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f