Merge branch 'fix/blanchard/wp/logic-app-type' into 'master'

[wp] type logic function _calls_ with C type

Closes #1332

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

src/plugins/wp/LogicSemantics.ml

@@ -681,7 +681,12 @@ struct
         | ACSLDEF -> C.call_fun env result f ls vs
         | HACK phi -> phi vs
         | LFUN f -> e_fun ~result f vs
-      in Vexp r
+      in
+      begin match t.term_type with
+        | Ctype t -> Lang.assume (Cvalues.has_ctype t r)
+        | _ -> ()
+      end ;
+      Vexp r
 
     | Tlambda _ ->
       Warning.error "Lambda-functions not yet implemented"

src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle

@@ -24,7 +24,13 @@ Prove: (0 <= L_t) /\ (L_t <= 127).
 ------------------------------------------------------------
 
 Goal Post-condition 'A' in 'g':
-Assume { (* Heap *) Type: region(p.base) <= 0. }
-Prove: L_x(Mint_0, p) <= 255.
+Let x = Mint_0[p].
+Let x_1 = L_x(Mint_0, p).
+Assume {
+  Type: is_uint8(x) /\ is_uint8(x_1).
+  (* Heap *)
+  Type: region(p.base) <= 0.
+}
+Prove: (x = x_1) /\ (x_1 <= 255).
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle

@@ -43,15 +43,20 @@ end
     
     (* use frama_c_wp.memaddr.MemAddr *)
     
+    (* use frama_c_wp.cint.Cint *)
+    
     (* use Axiomatic1 *)
     
     goal wp_goal :
-      forall t:addr -> int, a:addr. region (a.base) <= 0 -> L_x t a <= 255
+      forall t:addr -> int, a:addr.
+       let x = get t a in
+       let x1 = L_x t a in
+       region (a.base) <= 0 -> is_uint8 x -> is_uint8 x1 -> x = x1 /\ x1 <= 255
   end
-[wp] [Unsuccess] typed_g_ensures_A (Alt-Ergo) (Cached)
-[wp] Proved goals:    0 / 1
-  Unsuccess:       1
+[wp] [Valid] typed_g_ensures_A (Alt-Ergo) (Cached)
+[wp] Proved goals:    1 / 1
+  Alt-Ergo:        1
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  g                         -        -        1       0.0%
+  g                         -        1        1       100%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/user_def_type_guard.i

@@ -16,5 +16,5 @@
   @ ensures qed_ko: 0<=t<128 ; */
 void f(void) {return;}
 
-//@ ensures A: x(p) <= 255 ;
+//@ ensures A: *p == x(p) <= 255 ;
 void g(unsigned char* p){}