release RPP v0.0.3

rpp_predicate_visitor.ml

@@ -475,40 +475,49 @@ let inliner env inline_data data globals data_annot num proof =
 let make_separate env inline_info call_side_effect_data=
   Queue.add(fun () ->
       let separated_terms =
-        List.fold_left(fun data i ->
+        List.map(fun i ->
             let terms = List.map
                 (fun x -> Rpp_generator.do_one_terms_vis
                     i.kf i.formals i.locals i.id_option
                     call_side_effect_data
                     env.self x)
                 i.separated_terms
-            in terms @ data
-          ) [] (inline_info)
+            in terms
+          ) (inline_info)
       in
-      begin
-        match separated_terms with
-        | h::_ ->
-          let pointer_predicate_separated =
-            Pseparated(separated_terms)
-          in
-          let predicate_name =
-            {pred_name = [];pred_loc=h.term_loc; pred_content= pointer_predicate_separated}
-          in
-          let requires =
-            Logic_const.new_predicate predicate_name
-          in
-          let funbehs =
-            Cil.mk_behavior ~name:"default!" ~requires:([requires]) ()
-          in
-          Annotations.add_behaviors ~register_children:true
-            (Rpp_options.emitter) (Globals.Functions.get (env.new_funct.svar)) ([funbehs]);
-
-        | [] ->  ()
-      end)
+      let aux3 term l2 =
+        List.map (fun term2 -> term :: [term2]) l2
+      in
+      let rec aux2 term l2 =
+        match l2 with
+        | h :: q -> ( aux3 term h) @ aux2 term q
+        | [] -> []
+      in
+      let rec aux1 l =
+        match l with
+        | h :: q ->
+          (List.fold_left (fun data term -> aux2 term q @ data) [] h) @ aux1 q
+        | [] -> []
+      in
+      let separated_terms = aux1 separated_terms in
+      let make_separated separated_terms =
+        let predicate_name =
+          Logic_const.unamed (Pseparated(separated_terms))
+        in
+        let requires =
+          Logic_const.new_predicate predicate_name
+        in
+        let funbehs =
+          Cil.mk_behavior ~name:"default!" ~requires:([requires]) ()
+        in
+        Annotations.add_behaviors ~register_children:true
+          (Rpp_options.emitter) (Globals.Functions.get (env.new_funct.svar)) ([funbehs]);
+      in
+      List.iter make_separated separated_terms;)
     env.self#get_filling_actions;
 
   (**
-     Visitor for checking there is no memory charing
+     Visitor for checking there is no memory sharing
   *)
 class separate_checker loc terms id = object(_)
   inherit Visitor.frama_c_inplace

rpp_predicate_visitor_axiom.ml

@@ -24,25 +24,33 @@ open Rpp_predicate_visitor
 
 let make_separate env separated call_data =
   let separated_terms =
-    List.fold_left(fun data i ->
+    List.map (fun i ->
         let terms = List.map
             (fun x -> Rpp_generator.do_one_terms_vis_axiom
                 i.id_sep call_data i.formal_binder
                 env.self_axiom x)
             i.separated_terms_axiom
-        in terms @ data
-      ) [] separated
+        in terms
+      ) separated
   in
+  let aux3 term l2 =
+    List.map (fun term2 -> term :: [term2]) l2
+  in
+  let rec aux2 l2 term =
+    match l2 with
+    | h :: q -> (aux3 term h) @ aux2 q term
+    | [] -> []
+  in
+  let rec aux1 l =
+    match l with
+    | h :: q ->
+      (List.fold_left (fun data term -> aux2 q term @ data) [] h) @ aux1 q
+    | [] -> []
+  in
+  let separated_terms = aux1 separated_terms in
   match separated_terms with
-  | h::_ ->
-    let pointer_predicate_separated =
-      Pseparated(separated_terms)
-    in
-    let pred =
-      {pred_name = [];pred_loc=h.term_loc; pred_content= pointer_predicate_separated}
-    in
-    Some pred
-  | [] ->  None
+  | [] -> []
+  | _ ->  List.map (fun x -> Pseparated x) separated_terms
 
 let id_convert_axiom identifier loc call_side_effect_data =
   let source = fst loc in
@@ -1124,20 +1132,15 @@ let predicate_visitor predicate self_behavior =
         env quan (new_quant,new_labels,new_pred_axiom) new_axiome_predicate
       =
       let loc = env.loc_axiom in
-      let new_pred_axiom =
-        List.fold_left
-          (fun acc predicate_axiom ->
-             Logic_const.(pimplies ~loc (unamed ~loc predicate_axiom, acc)))
-          new_axiome_predicate new_pred_axiom
-      in
-      let pred =
+      let sep_pred =
         make_separate
           env !call_data_separated !call_side_effect_data
       in
       let new_pred_axiom =
-        match pred with
-        | None -> new_pred_axiom
-        | Some x -> Logic_const.pimplies ~loc (x,new_pred_axiom)
+        List.fold_left
+          (fun acc predicate_axiom ->
+             Logic_const.(pimplies ~loc (unamed ~loc predicate_axiom, acc)))
+          new_axiome_predicate (new_pred_axiom @ sep_pred)
       in
       let new_axiome_predicate =
         Logic_const.pforall ~loc (quan@(new_quant),new_pred_axiom)
@@ -1150,20 +1153,15 @@ let predicate_visitor predicate self_behavior =
         env (new_quant,new_labels,new_pred_axiom) new_axiome_predicate
       =
       let loc = env.loc_axiom in
-      let new_pred_axiom =
-        List.fold_left
-          (fun acc predicate_axiom ->
-             Logic_const.(pimplies ~loc (unamed ~loc predicate_axiom,acc)))
-          new_axiome_predicate new_pred_axiom
-      in
-      let pred =
+      let sep_pred =
         make_separate
           env !call_data_separated !call_side_effect_data
       in
       let new_pred_axiom =
-        match pred with
-        | None -> new_pred_axiom
-        | Some x -> Logic_const.pimplies ~loc (x,new_pred_axiom)
+        List.fold_left
+          (fun acc predicate_axiom ->
+             Logic_const.(pimplies ~loc (unamed ~loc predicate_axiom,acc)))
+          new_axiome_predicate (new_pred_axiom @ sep_pred)
       in
       let predicate = Logic_const.pforall ~loc (new_quant,new_pred_axiom) in
       let logic = {predicate_info= predicate_info} in

tests/rpp/oracle/axiom_separated.res.oracle

@@ -12,7 +12,6 @@ axiomatic Relational_axiome_1 {
 
   lemma Relational_lemma_1{pre_id1}:
     ∀ int x, int *tb, int *y_id1, int return_variable_relational_1;
-      \separated(y_id1, tb + (0 .. x)) ⇒
       k_acsl_1(tb, x, y_id1, return_variable_relational_1) ⇒
       return_variable_relational_1 ≡
       \at(*(tb + 1),pre_id1) + \at(*(tb + (x - 1)),pre_id1);
@@ -36,10 +35,8 @@ int k(int *t, int n)
 
 int *y_id1_1;
 
-/*@ requires \separated(y_id1_1, tb + (0 .. x));
-    requires \separated(tb + (0 .. x), y_id1_1);
-    requires x > 0;
- */
+/*@ requires \separated(tb + (0 .. x), y_id1_1);
+    requires x > 0; */
 void relational_wrapper_1(int x, int *tb)
 {
   int return_variable_relational_1;

tests/rpp/oracle/bug_varinfo.res.oracle

@@ -27,10 +27,15 @@ axiomatic Relational_axiome_1 {
 
   lemma Relational_lemma_1{pre_id2, post_id2, pre_id1, post_id1}:
     ∀ int *a1, int *a2, int *b1, int *b2, int *c1, int *c2, int n;
-      \separated(
-        c1 + (0 .. n * n - 1), a1 + (0 .. n * n - 1), b1 + (0 .. n * n - 1),
-        c2 + (0 .. n * n - 1), a2 + (0 .. n * n - 1), b2 + (0 .. n * n - 1)
-        ) ⇒
+      \separated(c2 + (0 .. n * n - 1), b1 + (0 .. n * n - 1)) ⇒
+      \separated(c2 + (0 .. n * n - 1), a1 + (0 .. n * n - 1)) ⇒
+      \separated(c2 + (0 .. n * n - 1), c1 + (0 .. n * n - 1)) ⇒
+      \separated(a2 + (0 .. n * n - 1), b1 + (0 .. n * n - 1)) ⇒
+      \separated(a2 + (0 .. n * n - 1), a1 + (0 .. n * n - 1)) ⇒
+      \separated(a2 + (0 .. n * n - 1), c1 + (0 .. n * n - 1)) ⇒
+      \separated(b2 + (0 .. n * n - 1), b1 + (0 .. n * n - 1)) ⇒
+      \separated(b2 + (0 .. n * n - 1), a1 + (0 .. n * n - 1)) ⇒
+      \separated(b2 + (0 .. n * n - 1), c1 + (0 .. n * n - 1)) ⇒
       matrix_mult_acsl_1{pre_id2, post_id2}(a2, b2, c2, n) ⇒
       matrix_mult_acsl_1{pre_id1, post_id1}(a1, b1, c1, n) ⇒
       \at(*c1,post_id1) < \at(*c2,post_id2);
@@ -46,9 +51,6 @@ axiomatic Relational_axiome_2 {
 
   lemma Relational_lemma_2{pre_id3, post_id3}:
     ∀ int *a1, int *c1, int *b1, int n;
-      \separated(
-        c1 + (0 .. n * n - 1), a1 + (0 .. n * n - 1), b1 + (0 .. n * n - 1)
-        ) ⇒
       matrix_mult_acsl_2{pre_id3, post_id3}(a1, b1, c1, n) ⇒
       \at(*c1,post_id3) < 0;
 
@@ -158,11 +160,15 @@ void matrix_mult_id3(int *a, int *b, int *c, int n);
  */
 void matrix_mult_id1(int *a, int *b, int *c, int n);
 
-/*@ requires
-      \separated(
-        c1 + (0 .. n * n - 1), a1 + (0 .. n * n - 1), b1 + (0 .. n * n - 1),
-        c2 + (0 .. n * n - 1), a2 + (0 .. n * n - 1), b2 + (0 .. n * n - 1)
-        );
+/*@ requires \separated(c2 + (0 .. n * n - 1), b1 + (0 .. n * n - 1));
+    requires \separated(c2 + (0 .. n * n - 1), a1 + (0 .. n * n - 1));
+    requires \separated(c2 + (0 .. n * n - 1), c1 + (0 .. n * n - 1));
+    requires \separated(a2 + (0 .. n * n - 1), b1 + (0 .. n * n - 1));
+    requires \separated(a2 + (0 .. n * n - 1), a1 + (0 .. n * n - 1));
+    requires \separated(a2 + (0 .. n * n - 1), c1 + (0 .. n * n - 1));
+    requires \separated(b2 + (0 .. n * n - 1), b1 + (0 .. n * n - 1));
+    requires \separated(b2 + (0 .. n * n - 1), a1 + (0 .. n * n - 1));
+    requires \separated(b2 + (0 .. n * n - 1), c1 + (0 .. n * n - 1));
     requires \separated(a2 + (0 .. n * n - 1), c2 + (0 .. n * n - 1));
     requires \separated(b2 + (0 .. n * n - 1), c2 + (0 .. n * n - 1));
     requires \valid_read(a2 + (0 .. n * n - 1));
@@ -244,11 +250,7 @@ void relational_wrapper_1(int *a1, int *a2, int *b1, int *b2, int *c1,
   return;
 }
 
-/*@ requires
-      \separated(
-        c1 + (0 .. n * n - 1), a1 + (0 .. n * n - 1), b1 + (0 .. n * n - 1)
-        );
-    requires \separated(a1 + (0 .. n * n - 1), c1 + (0 .. n * n - 1));
+/*@ requires \separated(a1 + (0 .. n * n - 1), c1 + (0 .. n * n - 1));
     requires \separated(b1 + (0 .. n * n - 1), c1 + (0 .. n * n - 1));
     requires \valid_read(a1 + (0 .. n * n - 1));
     requires \valid_read(b1 + (0 .. n * n - 1));

tests/rpp/oracle/includes.res.oracle

@@ -87,7 +87,6 @@ axiomatic Relational_axiome_4 {
 
   lemma Relational_lemma_4{pre_id1}:
     ∀ uint8_t *x_id1, uint8_t return_variable_relational_3;
-      \separated(x_id1) ⇒
       h_acsl_4(x_id1, return_variable_relational_3) ⇒
       return_variable_relational_3 ≡ 0;
 
@@ -163,7 +162,6 @@ void relational_wrapper_3(void)
 
 uint8_t *x_id1_4;
 
-/*@ requires \separated(x_id1_4); */
 void relational_wrapper_4(void)
 {
   uint8_t return_variable_relational_5;

tests/rpp/oracle/max.res.oracle

@@ -12,10 +12,12 @@ axiomatic Relational_axiome_1 {
     ∀ int *t1, int *t2, int *tn, int *t, int return_variable_relational_4,
         int return_variable_relational_3, int return_variable_relational_2,
         int return_variable_relational_1;
-      \separated(
-        t1 + (0 .. (int)2), t2 + (0 .. (int)2), tn + (0 .. (int)2),
-        t + (0 .. (int)4)
-        ) ⇒
+      \separated(t2 + (0 .. (int)2), t1 + (0 .. (int)2)) ⇒
+      \separated(tn + (0 .. (int)2), t1 + (0 .. (int)2)) ⇒
+      \separated(tn + (0 .. (int)2), t2 + (0 .. (int)2)) ⇒
+      \separated(t + (0 .. (int)4), t1 + (0 .. (int)2)) ⇒
+      \separated(t + (0 .. (int)4), t2 + (0 .. (int)2)) ⇒
+      \separated(t + (0 .. (int)4), tn + (0 .. (int)2)) ⇒
       f_acsl_1{pre_id4}(t, (int)4, return_variable_relational_4) ⇒
       f_acsl_1{pre_id3}(tn, (int)2, return_variable_relational_3) ⇒
       f_acsl_1{pre_id2}(t2, (int)2, return_variable_relational_2) ⇒
@@ -105,8 +107,27 @@ int f_id1(int *t, int n);
 
 /*@ requires
       \separated(
-        t1 + (0 .. aux_local_variable_1), t2 + (0 .. aux_local_variable_2),
-        tn + (0 .. aux_local_variable_3), t + (0 .. aux_local_variable_4)
+        t2 + (0 .. aux_local_variable_2), t1 + (0 .. aux_local_variable_1)
+        );
+    requires
+      \separated(
+        tn + (0 .. aux_local_variable_3), t1 + (0 .. aux_local_variable_1)
+        );
+    requires
+      \separated(
+        tn + (0 .. aux_local_variable_3), t2 + (0 .. aux_local_variable_2)
+        );
+    requires
+      \separated(
+        t + (0 .. aux_local_variable_4), t1 + (0 .. aux_local_variable_1)
+        );
+    requires
+      \separated(
+        t + (0 .. aux_local_variable_4), t2 + (0 .. aux_local_variable_2)
+        );
+    requires
+      \separated(
+        t + (0 .. aux_local_variable_4), tn + (0 .. aux_local_variable_3)
         );
     requires \valid(t + (0 .. 4));
     requires 4 ≥ 1;

tests/rpp/oracle/monotonie_side_effect_pointer.res.oracle

@@ -11,7 +11,7 @@ axiomatic Relational_axiome_1 {
 
   lemma Relational_lemma_1{pre_id2, post_id2, pre_id1, post_id1}:
     ∀ int x, int *y_id2, int *y_id1;
-      \separated(y_id1, y_id2) ⇒
+      \separated(y_id2, y_id1) ⇒
       k_acsl_1{pre_id2, post_id2}(x, y_id2) ⇒
       k_acsl_1{pre_id1, post_id1}(x, y_id1) ⇒
       \at(*y_id1,pre_id1) < \at(*y_id2,pre_id2) ∧ x > 0 ⇒
@@ -40,7 +40,7 @@ axiomatic Relational_axiome_2 {
 
   lemma Relational_lemma_2{pre_id4, post_id4, pre_id3, post_id3}:
     ∀ int *x1, int *x2;
-      \separated(x1, x2) ⇒
+      \separated(x2, x1) ⇒
       f_acsl_2{pre_id4, post_id4}(x2) ⇒
       f_acsl_2{pre_id3, post_id3}(x1) ⇒
       \at(*x1,pre_id3) < \at(*x2,pre_id4) ⇒
@@ -66,7 +66,7 @@ int *y_id1_1;
 
 int *y_id2_1;
 
-/*@ requires \separated(y_id1_1, y_id2_1);
+/*@ requires \separated(y_id2_1, y_id1_1);
     requires \valid(y_id2_1);
     requires *y_id2_1 > 0;
     requires \valid(y_id1_1);
@@ -90,7 +90,7 @@ void relational_wrapper_1(int x)
   return;
 }
 
-/*@ requires \separated(x1, x2);
+/*@ requires \separated(x2, x1);
     requires \valid(x2);
     requires \valid(x1); */
 void relational_wrapper_2(int *x1, int *x2)

tests/rpp/oracle/more_pointer.res.oracle

@@ -14,7 +14,7 @@ axiomatic Relational_axiome_1 {
 
   lemma Relational_lemma_1{pre_id2, post_id2, pre_id1, post_id1}:
     ∀ int *x1, int *x2;
-      \separated(x1 + (0 .. 1), x2 + (0 .. 1)) ⇒
+      \separated(x2 + (0 .. 1), x1 + (0 .. 1)) ⇒
       f_acsl_1{pre_id2, post_id2}(x2) ⇒
       f_acsl_1{pre_id1, post_id1}(x1) ⇒
       is_eq{post_id1, pre_id2}(x1, x2, 2) ⇒
@@ -38,7 +38,7 @@ void f(int *x)
   return;
 }
 
-/*@ requires \separated(x1 + (0 .. 1), x2 + (0 .. 1));
+/*@ requires \separated(x2 + (0 .. 1), x1 + (0 .. 1));
     requires \valid(x2 + (0 .. 1));
     requires \valid(x1 + (0 .. 1));
  */

tests/rpp/oracle/pointer.res.oracle

@@ -41,7 +41,7 @@ axiomatic Relational_axiome_2 {
   lemma Relational_lemma_2{pre_id4, pre_id3}:
     ∀ int *y_id4, int return_variable_relational_4, int *y_id3,
         int return_variable_relational_3;
-      \separated(y_id3, y_id4) ⇒
+      \separated(y_id4, y_id3) ⇒
       h_acsl_2{pre_id4}(y_id4, return_variable_relational_4) ⇒
       h_acsl_2{pre_id3}(y_id3, return_variable_relational_3) ⇒
       \at(*y_id3,pre_id3) ≡ \at(*y_id4,pre_id4) ⇒
@@ -117,7 +117,7 @@ int *y_id3_2;
 
 int *y_id4_2;
 
-/*@ requires \separated(y_id3_2, y_id4_2); */
+/*@ requires \separated(y_id4_2, y_id3_2); */
 void relational_wrapper_2(void)
 {
   int return_variable_relational_3;