[wp/region] swap tests

src/plugins/wp/tests/ptests_config

-DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
-DEFAULT_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
+## General Purpose
+DEFAULT_SUITES= wp wp_manual wp_usage wp_plugin wp_gallery wp_tip wp_bts
+qualif_SUITES=  wp wp_manual wp_usage wp_plugin wp_gallery wp_tip wp_bts
 
-qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
-qualif_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
-qualif_SUITES= why3
+## Memory Models
+DEFAULT_SUITES= wp_acsl wp_hoare wp_store wp_typed wp_bytes wp_region
+qualif_SUITES=  wp_acsl wp_hoare wp_store wp_typed wp_bytes wp_region
 
-ce_SUITES= wp_ce
+## Specific Objectives
+qualif_SUITES=  why3
+DEFAULT_SUITES= wp_ce
+ce_SUITES=      wp_ce

src/plugins/wp/tests/wp_region/oracle/swap.res.oracle

+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing swap.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal swap_aliased_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_aliased_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal swap_separated_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_separated_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+  Function swap_aliased
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 20) in 'swap_aliased':
+Let a = ValueChunk_2[global(P_b_33)].
+Let a_1 = ValueChunk_1[global(P_a_32)].
+Let x = ValueChunk_0[a_1].
+Let x_1 = ValueChunk_0[a].
+Let x_2 = ValueChunk_0[a_1 <- x_1][a <- x][a_1].
+Assume {
+  Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
+  (* Heap *)
+  Type: linked(alloc_0) /\ framed(ValueChunk_1) /\ framed(ValueChunk_2).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, a_1, 4).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, a, 4).
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 21) in 'swap_aliased':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 22) in 'swap_aliased' (1/2):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 22) in 'swap_aliased' (2/2):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function swap_separated
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 5) in 'swap_separated':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 6) in 'swap_separated':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 7) in 'swap_separated' (1/2):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 7) in 'swap_separated' (2/2):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle

+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing swap.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal swap_aliased_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_aliased_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal swap_separated_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_separated_terminates (Cfg) (Trivial)
+[wp] 8 goals scheduled
+[wp] [Valid] region_swap_separated_ensures (Qed)
+[wp] [Valid] region_swap_separated_ensures_2 (Qed)
+[wp] [Valid] region_swap_separated_assigns_part1 (Qed)
+[wp] [Valid] region_swap_separated_assigns_part2 (Qed)
+[wp] [Valid] region_swap_aliased_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_swap_aliased_ensures_2 (Qed)
+[wp] [Valid] region_swap_aliased_assigns_part1 (Qed)
+[wp] [Valid] region_swap_aliased_assigns_part2 (Qed)
+[wp] Proved goals:   12 / 12
+  Terminating:     2
+  Unreachable:     2
+  Qed:             7
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  swap_separated            4        -        4       100%
+  swap_aliased              3        1        4       100%
+------------------------------------------------------------

src/plugins/wp/tests/wp_region/swap.i

+/*@
+  requires \valid(a);
+  requires \valid(b);
+  region A: *a, B: *b;
+  ensures *a == \old(*b);
+  ensures *b == \old(*a);
+  assigns *a, *b;
+  */
+void swap_separated(int *a, int *b)
+{
+  int tmp = *a ;
+  *a = *b;
+  *b = tmp ;
+}
+
+/*@
+  requires \valid(a);
+  requires \valid(b);
+  region R: *a, *b;
+  ensures *a == \old(*b);
+  ensures *b == \old(*a);
+  assigns *a, *b;
+  */
+void swap_aliased(int *a, int *b)
+{
+  int tmp = *a ;
+  *a = *b;
+  *b = tmp ;
+}

src/plugins/wp/tests/wp_region/test_config

+OPT: -wp-model region

src/plugins/wp/tests/wp_region/test_config_qualif

+OPT: -wp-model region