From 09038ca5a9c20f3f6d5b99c0b04a4dfe3428a2b2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 29 Mar 2024 15:28:51 +0100
Subject: [PATCH] [wp] type logic function _calls_ with C type
---
src/plugins/wp/LogicSemantics.ml | 7 ++++++-
.../wp_acsl/oracle/user_def_type_guard.res.oracle | 10 ++++++++--
.../user_def_type_guard.2.res.oracle | 15 ++++++++++-----
.../wp/tests/wp_acsl/user_def_type_guard.i | 2 +-
4 files changed, 25 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index e1ae3720d51..aac2295277c 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/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"
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
index 37f7d58dc5b..d2766c72bfc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/user_def_type_guard.res.oracle
+++ b/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).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
index 4dd7571870e..1ab51dfc811 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
+++ b/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%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i b/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i
index 6dd01e0b069..32606dca6f3 100644
--- a/src/plugins/wp/tests/wp_acsl/user_def_type_guard.i
+++ b/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){}
--
GitLab