[wp] Fixes frame lemmas generation

src/plugins/wp/MemLoader.ml

@@ -117,8 +117,8 @@ struct
     begin
       let prefix = Fun.debug phi in
       let sigma = Sigma.create () in
-      List.iter
-        (fun chunk ->
+      List.iteri
+        (fun i chunk ->
            List.iter
              (fun (name,triggers,conditions,m1,m2) ->
                 let mem1 = assigned sigma chunk m1 chunks in
@@ -137,8 +137,8 @@ struct
                     [ (Trigger.of_term value1 :: triggers );
                       (Trigger.of_term value2 :: triggers ) ]
                 in
-                let l_name = Pretty_utils.sfprintf "%s_%s_%a"
-                    prefix name Chunk.pretty chunk in
+                let l_name = Pretty_utils.sfprintf "%s_%s_%a%d"
+                    prefix name Chunk.pretty chunk i in
                 let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
                 Definitions.define_lemma {
                   l_assumed = true ;

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

+# frama-c -wp -wp-rte -wp-no-let [...]
+[kernel] Parsing tests/wp_acsl/struct_fields.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function foo
+[wp] 2 goals scheduled
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'Chunk' 
+---------------------------------------------
+theory Chunk
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use frama_c_wp.memory.Memory *)
+  
+  (* use frama_c_wp.cint.Cint *)
+  
+  predicate is_sint8_chunk (m:addr -> int) =
+    forall a:addr. is_sint8 (get m a)
+  
+  predicate is_sint16_chunk (m:addr -> int) =
+    forall a:addr. is_sint16 (get m a)
+  
+  predicate is_sint32_chunk (m:addr -> int) =
+    forall a:addr. is_sint32 (get m a)
+end
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'S1_X' 
+---------------------------------------------
+theory S1_X
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  type S1_X =
+    | S1_X1 (F1_X_a:int) (F1_X_b:int) (F1_X_c:int)
+  
+  (* use frama_c_wp.cint.Cint *)
+  
+  predicate IsS1_X (s:S1_X) =
+    (is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
+end
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'Compound' 
+---------------------------------------------
+theory Compound
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use frama_c_wp.memory.Memory *)
+  
+  function shiftfield_F1_X_a (p:addr) : addr = shift p 0
+  
+  function shiftfield_F1_X_b (p:addr) : addr = shift p 1
+  
+  function shiftfield_F1_X_c (p:addr) : addr = shift p 2
+  
+  (* use S1_X *)
+  
+  function Load_S1_X (p:addr) (mchar:addr -> int) (mint:addr -> int) (mint1:
+    addr -> int) : S1_X =
+    S1_X1 (get mchar (shiftfield_F1_X_a p)) (get mint (shiftfield_F1_X_b p))
+    (get mint1 (shiftfield_F1_X_c p))
+  
+  Q_Load_S1_X_update_Mchar0 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
+     separated p 3 q 1 ->
+     Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_eqmem_Mchar0 :
+    forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
+     addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
+     eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
+     eqmem mchar mchar1 q n].
+     included p 3 q n ->
+     eqmem mchar mchar1 q n ->
+     Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_havoc_Mchar0 :
+    forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
+     addr -> int, n:int, p:addr, q:addr
+     [Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
+     separated p 3 q n ->
+     Load_S1_X p (havoc mchar1 mchar q n) mint mint1
+     = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_update_Mint1 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
+     separated p 3 q 1 ->
+     Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
+  
+  Q_Load_S1_X_eqmem_Mint1 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
+     eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
+     eqmem mint1 mint2 q n].
+     included p 3 q n ->
+     eqmem mint1 mint2 q n ->
+     Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
+  
+  Q_Load_S1_X_havoc_Mint1 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr
+     [Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
+     separated p 3 q n ->
+     Load_S1_X p mchar (havoc mint2 mint1 q n) mint
+     = Load_S1_X p mchar mint1 mint
+  
+  Q_Load_S1_X_update_Mint2 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+     addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
+     separated p 3 q 1 ->
+     Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_eqmem_Mint2 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
+     eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
+     eqmem mint1 mint2 q n].
+     included p 3 q n ->
+     eqmem mint1 mint2 q n ->
+     Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
+  
+  Q_Load_S1_X_havoc_Mint2 :
+    forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+     -> int, n:int, p:addr, q:addr
+     [Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
+     separated p 3 q n ->
+     Load_S1_X p mchar mint (havoc mint2 mint1 q n)
+     = Load_S1_X p mchar mint mint1
+end
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use Chunk *)
+    
+    (* use S1_X *)
+    
+    (* use Compound *)
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> int, t2:addr -> int, t3:addr -> int, a:
+       addr.
+       region (base a) <= 0 ->
+       is_sint16_chunk t2 ->
+       is_sint32_chunk t3 ->
+       is_sint8_chunk t1 ->
+       linked t ->
+       sconst t1 ->
+       valid_rd t a 3 -> IsS1_X (Load_S1_X a t1 t2 t3) -> valid_rw t a 3
+  end
+[wp:print-generated] 
+  theory WP1
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use Chunk *)
+    
+    (* use S1_X *)
+    
+    (* use Compound *)
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> int, t2:addr -> int, t3:addr -> int, a:
+       addr.
+       region (base a) <= 0 ->
+       is_sint16_chunk t2 ->
+       is_sint32_chunk t3 ->
+       is_sint8_chunk t1 ->
+       linked t -> sconst t1 -> IsS1_X (Load_S1_X a t1 t2 t3) -> valid_rd t a 3
+  end
+[wp] 2 goals generated
+------------------------------------------------------------
+  Function foo
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0) /\
+      IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+}
+Prove: valid_rd(Malloc_0, p, 3).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
+Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
+Assume {
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+      is_sint8_chunk(Mchar_0).
+  (* Assertion 'rte,mem_access' *)
+  Have: valid_rd(Malloc_0, p, 3).
+  (* Initializer *)
+  Init: a = r.
+}
+Prove: valid_rw(Malloc_0, p, 3).
+
+------------------------------------------------------------

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

+/* run.config
+   OPT:-wp-rte -wp-no-let -wp-gen -wp-prover why3 -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+struct X {
+  char a ;
+  short b ;
+  int c ;
+};
+
+void foo(struct X* p){
+  struct X r = *p ;
+  *p = r ;
+}
\ No newline at end of file

src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle

@@ -60,19 +60,19 @@ theory Compound
   function Load_S2_A (p:addr) (mint:addr -> int) : S2_A =
     S2_A1 (get mint (shiftfield_F2_A_dummy p))
   
-  Q_Load_S2_A_update_Mint :
+  Q_Load_S2_A_update_Mint0 :
     forall mint:addr -> int, p:addr, q:addr, v:int
      [Load_S2_A p (set mint q v)].
      not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
   
-  Q_Load_S2_A_eqmem_Mint :
+  Q_Load_S2_A_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
      eqmem mint mint1 q n].
      included p 1 q n ->
      eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
   
-  Q_Load_S2_A_havoc_Mint :
+  Q_Load_S2_A_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p (havoc mint1 mint q n)].
      separated p 1 q n ->