Merge branch 'fix/blanchard/wp/factory-ref-usage' into 'master'

[wp] fix factory ref-usage

Closes #1491

See merge request frama-c/frama-c!4939

src/plugins/wp/Factory.ml

@@ -140,8 +140,8 @@ end
 (* -------------------------------------------------------------------------- *)
 
 let is_ptr x = Cil.isPointerType x.Cil_types.vtype
-let is_fun_ptr x = Cil.isFunctionType x.Cil_types.vtype
 let is_formal_ptr x = x.Cil_types.vformal && is_ptr x
+
 let is_init kf x =
   CfgInfos.is_entry_point kf ||
   Wp_parameters.AliasInit.get () ||
@@ -156,7 +156,8 @@ let refusage_param ~byref ~context x =
   | RefUsage.ByAddr -> MemoryContext.ByAddr
   | RefUsage.ByValue ->
     if context && is_formal_ptr x then MemoryContext.InContext (validity x)
-    else if is_ptr x && not (is_fun_ptr x) then MemoryContext.ByShift
+    else if is_ptr x && not @@ Cil.isFunPtrType x.Cil_types.vtype
+    then MemoryContext.ByShift
     else MemoryContext.ByValue
   | RefUsage.ByRef ->
     if byref

src/plugins/wp/tests/wp_plugin/oracle/dynamic.0.res.oracle

@@ -415,12 +415,12 @@ Prove: true.
 [wp] dynamic.i:65: Warning: 
   Memory model hypotheses for function 'behavior':
   /*@ behavior wp_typed:
-        requires \separated(p + (..), &X1); */
+        requires \separated(p, &X1); */
   int behavior(int (*p)(void));
 [wp] dynamic.i:78: Warning: 
   Memory model hypotheses for function 'some_behaviors':
   /*@ behavior wp_typed:
-        requires \separated(p + (..), &X1); */
+        requires \separated(p, &X1); */
   int some_behaviors(int (*p)(void));
 [wp] dynamic.i:87: Warning: 
   Memory model hypotheses for function 'missing_context':

src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.0.res.oracle

@@ -97,12 +97,12 @@
 [wp] dynamic.i:65: Warning: 
   Memory model hypotheses for function 'behavior':
   /*@ behavior wp_typed:
-        requires \separated(p + (..), &X1); */
+        requires \separated(p, &X1); */
   int behavior(int (*p)(void));
 [wp] dynamic.i:78: Warning: 
   Memory model hypotheses for function 'some_behaviors':
   /*@ behavior wp_typed:
-        requires \separated(p + (..), &X1); */
+        requires \separated(p, &X1); */
   int some_behaviors(int (*p)(void));
 [wp] dynamic.i:87: Warning: 
   Memory model hypotheses for function 'missing_context':