[WP/Why3] Test for inductive definition generation

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

+/* run.config
+   OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+*/
+
+/*@ inductive is_gcd(integer a, integer b, integer d) {
+    case gcd_zero:
+      \forall integer n; is_gcd(n, 0, n);
+    case gcd_succ:
+      \forall integer a, b, d;
+      is_gcd(b, a % b, d) ==> is_gcd(a, b, d);
+    }
+*/
+
+/*@ lemma test_no_label:
+  \forall integer a, b, d ;
+  is_gcd(a, b, d) ==> is_gcd(b, d, a) ==> \false ;
+*/
+
+typedef struct _list { int element; struct _list* next; } list;
+
+/*@ inductive reachable{L} (list* root, list* node) {
+    case root_reachable{L}:
+         \forall list* root; reachable(root,root);
+    case next_reachable{L}:
+         \forall list* root, *node;
+         \valid(root) ==> reachable(root->next, node) ==> reachable(root,node);
+  }
+*/
+
+/*@ lemma test_one_label{L1, L2}:
+  \forall list *l1, *l2 ;
+  reachable{L1}(l1, l2) ==> reachable{L2}(l1, l2) ==> \false ;
+*/
+
+/*@ predicate swap{L1, L2}(int *a, int *b, integer begin, integer i, integer j, integer end) =
+       begin <= i < j < end &&
+       \at(a[i], L1) == \at(b[j], L2) &&
+       \at(a[j], L1) == \at(b[i], L2) &&
+       \forall integer k; begin <= k < end && k != i && k != j ==>
+       \at(a[k], L1) == \at(b[k], L2);
+
+    predicate same_array{L1,L2}(int *a, int *b, integer begin, integer end) =
+      \forall integer k; begin <= k < end ==> \at(a[k],L1) == \at(b[k],L2);
+
+    inductive same_elements{L1, L2}(int *a, int *b, integer begin, integer end) {
+      case refl{L1, L2}:
+        \forall int *a, int *b, integer begin, end;
+        same_array{L1,L2}(a, b, begin, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+      case swap{L1, L2}: \forall int *a, int *b, integer begin, i, j, end;
+        swap{L1, L2}(a, b, begin, i, j, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+      case trans{L1, L2, L3}: \forall int* a, int *b, int *c, integer begin, end;
+        same_elements{L1, L2}(a, b, begin, end) ==>
+        same_elements{L2, L3}(b, c, begin, end) ==>
+        same_elements{L1, L3}(a, c, begin, end);
+    }
+*/
+
+/*@ lemma test_multilabel{L1, L2, L3}:
+  \forall int *a, *b, integer b1, b2, e1, e2 ;
+  same_elements{L1, L2}(a, b, b1, e1) ==>
+  same_elements{L2, L3}(b, a, b2, e2) ==>
+    \false ;
+*/
\ No newline at end of file

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/inductive.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 3 goals scheduled
+[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 *)
+    
+    predicate P_is_gcd int int int
+    
+    axiom Q_gcd_zero : forall n:int. P_is_gcd n 0 n
+    
+    axiom Q_gcd_succ :
+      forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
+    
+    lemma Q_test_no_label :
+      forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use Compound *)
+    
+    predicate P_reachable (int -> int) (addr -> addr) addr addr
+    
+    axiom Q_root_reachable :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr.
+       P_reachable malloc mptr root root
+    
+    axiom Q_next_reachable :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+       valid_rw malloc root 2 ->
+       P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
+       P_reachable malloc mptr root node
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> addr, t2:int -> int, t3:addr -> addr, a:
+       addr, a1:addr. P_reachable t2 t3 a a1 -> not P_reachable t t1 a a1
+  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 *)
+    
+    predicate P_is_gcd1 int int int
+    
+    axiom Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
+    
+    axiom Q_gcd_succ1 :
+      forall a:int, b:int, d:int. P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
+    
+    goal wp_goal :
+      forall i:int, i1:int, i2:int. P_is_gcd1 i i1 i2 -> not P_is_gcd1 i1 i2 i
+  end
+[wp:print-generated] 
+  theory WP2
+    (* 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 Compound *)
+    
+    predicate P_reachable1 (int -> int) (addr -> addr) addr addr
+    
+    axiom Q_root_reachable1 :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr.
+       P_reachable1 malloc mptr root root
+    
+    axiom Q_next_reachable1 :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+       valid_rw malloc root 2 ->
+       P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
+       P_reachable1 malloc mptr root node
+    
+    lemma Q_test_one_label :
+      forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
+       addr -> addr, l1:addr, l2:addr.
+       P_reachable1 malloc1 mptr1 l1 l2 -> not P_reachable1 malloc mptr l1 l2
+    
+    predicate P_is_gcd2 int int int
+    
+    axiom Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
+    
+    axiom Q_gcd_succ2 :
+      forall a:int, b:int, d:int. P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
+    
+    lemma Q_test_no_label1 :
+      forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
+    
+    predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
+      addr) (begin:int) (end1:int) =
+      forall i:int.
+       begin <= i ->
+       i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
+    
+    predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
+      (begin:int) (i:int) (j:int) (end1:int) =
+      ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
+          get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
+         begin <= i) /\
+        i < j) /\
+       j < end1) /\
+      (forall i1:int.
+        not i1 = i ->
+        not j = i1 ->
+        begin <= i1 ->
+        i1 < end1 ->
+        get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
+    
+    predicate P_same_elements (addr -> int) (addr -> int) addr addr int int
+    
+    axiom Q_refl :
+      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int,
+       end1:int.
+       P_same_array mint mint1 a b begin end1 ->
+       P_same_elements mint mint1 a b begin end1
+    
+    axiom Q_swap :
+      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int, i:
+       int, j:int, end1:int.
+       P_swap mint mint1 a b begin i j end1 ->
+       P_same_elements mint mint1 a b begin end1
+    
+    axiom Q_trans :
+      forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:addr, b:
+       addr, c:addr, begin:int, end1:int.
+       P_same_elements mint mint1 b c begin end1 ->
+       P_same_elements mint1 mint2 a b begin end1 ->
+       P_same_elements mint mint2 a c begin end1
+    
+    goal wp_goal :
+      forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
+       int, i1:int, i2:int, i3:int.
+       P_same_elements t1 t2 a a1 i i2 -> not P_same_elements t t1 a1 a i1 i3
+  end
+[wp] 3 goals generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma test_multilabel:
+Assume: 'test_one_label' 'test_no_label'
+Prove: (P_same_elements Mint_1 Mint_2 a_0 b_0 b1_0 e1_0)
+       -> (not (P_same_elements Mint_0 Mint_1 b_0 a_0 b2_0 e2_0))
+
+------------------------------------------------------------
+
+Lemma test_no_label:
+Prove: (P_is_gcd a_0 b_0 d_0) -> (not (P_is_gcd b_0 d_0 a_0))
+
+------------------------------------------------------------
+
+Lemma test_one_label:
+Assume: 'test_no_label'
+Prove: (P_reachable Malloc_1 Mptr_1 l1_0 l2_0)
+       -> (not (P_reachable Malloc_0 Mptr_0 l1_0 l2_0))
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.0.report.json

+{ "wp:global": { "wp:main": { "total": 3, "unknown": 3 } },
+  "wp:axiomatics": { "": { "lemma_test_one_label": { "wp:main": { "total": 1,
+                                                                  "unknown": 1 } },
+                           "lemma_test_no_label": { "wp:main": { "total": 1,
+                                                                 "unknown": 1 } },
+                           "lemma_test_multilabel": { "wp:main": { "total": 1,
+                                                                   "unknown": 1 } },
+                           "wp:section": { "wp:main": { "total": 3,
+                                                        "unknown": 3 } } } } }

src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/inductive.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 3 goals scheduled
+[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 Compound *)
+    
+    predicate P_reachable (int -> int) (addr -> addr) addr addr
+    
+    axiom Q_root_reachable :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr.
+       P_reachable malloc mptr root root
+    
+    axiom Q_next_reachable :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+       valid_rw malloc root 2 ->
+       P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
+       P_reachable malloc mptr root node
+    
+    lemma Q_test_one_label :
+      forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
+       addr -> addr, l1:addr, l2:addr.
+       P_reachable malloc1 mptr1 l1 l2 -> not P_reachable malloc mptr l1 l2
+    
+    predicate P_is_gcd int int int
+    
+    axiom Q_gcd_zero : forall n:int. P_is_gcd n 0 n
+    
+    axiom Q_gcd_succ :
+      forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
+    
+    lemma Q_test_no_label :
+      forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
+    
+    predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
+      addr) (begin:int) (end1:int) =
+      forall i:int.
+       begin <= i ->
+       i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
+    
+    predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
+      (begin:int) (i:int) (j:int) (end1:int) =
+      ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
+          get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
+         begin <= i) /\
+        i < j) /\
+       j < end1) /\
+      (forall i1:int.
+        not i1 = i ->
+        not j = i1 ->
+        begin <= i1 ->
+        i1 < end1 ->
+        get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
+    
+    predicate P_same_elements (addr -> int) (addr -> int) addr addr int int
+    
+    axiom Q_refl :
+      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int,
+       end1:int.
+       P_same_array mint mint1 a b begin end1 ->
+       P_same_elements mint mint1 a b begin end1
+    
+    axiom Q_swap :
+      forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int, i:
+       int, j:int, end1:int.
+       P_swap mint mint1 a b begin i j end1 ->
+       P_same_elements mint mint1 a b begin end1
+    
+    axiom Q_trans :
+      forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:addr, b:
+       addr, c:addr, begin:int, end1:int.
+       P_same_elements mint mint1 b c begin end1 ->
+       P_same_elements mint1 mint2 a b begin end1 ->
+       P_same_elements mint mint2 a c begin end1
+    
+    goal wp_goal :
+      forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
+       int, i1:int, i2:int, i3:int.
+       P_same_elements t1 t2 a a1 i i2 -> not P_same_elements t t1 a1 a i1 i3
+  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 *)
+    
+    predicate P_is_gcd1 int int int
+    
+    axiom Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
+    
+    axiom Q_gcd_succ1 :
+      forall a:int, b:int, d:int. P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
+    
+    goal wp_goal :
+      forall i:int, i1:int, i2:int. P_is_gcd1 i i1 i2 -> not P_is_gcd1 i1 i2 i
+  end
+[wp:print-generated] 
+  theory WP2
+    (* 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 *)
+    
+    predicate P_is_gcd2 int int int
+    
+    axiom Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
+    
+    axiom Q_gcd_succ2 :
+      forall a:int, b:int, d:int. P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
+    
+    lemma Q_test_no_label1 :
+      forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use Compound *)
+    
+    predicate P_reachable1 (int -> int) (addr -> addr) addr addr
+    
+    axiom Q_root_reachable1 :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr.
+       P_reachable1 malloc mptr root root
+    
+    axiom Q_next_reachable1 :
+      forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
+       valid_rw malloc root 2 ->
+       P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
+       P_reachable1 malloc mptr root node
+    
+    goal wp_goal :
+      forall t:int -> int, t1:addr -> addr, t2:int -> int, t3:addr -> addr, a:
+       addr, a1:addr. P_reachable1 t2 t3 a a1 -> not P_reachable1 t t1 a a1
+  end
+[wp] 3 goals generated
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/inductive.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/inductive.0.report.json'
+-------------------------------------------------------------
+Axiomatics          WP     Alt-Ergo        Total   Success
+Lemma               -      -                 3       0.0%
+-------------------------------------------------------------