diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 682e9adb223dc0f278e5096391f8651254377669..f2bbd01805f4ec415aa9716668e1d3c0e4ac0efc 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -1082,12 +1082,85 @@ struct
(* --- CheckAssigns --- *)
(* -------------------------------------------------------------------------- *)
- let check_assigns sigma ~written ~assignable =
+ let rec decompose_region (obj, sloc) =
+ let is_primitive_int t = Lang.F.is_int t && Lang.F.is_primitive t in
+ match sloc with
+ | Sloc loc ->
+ begin match obj with
+ | C_pointer _ | C_int _ | C_float _
+ | C_comp { cfields = None } | C_array { arr_flat = None } ->
+ [obj, sloc]
+
+ | C_comp { cfields = Some fields } ->
+ let slocs_of_field f =
+ let obj = Ctypes.object_of f.ftype in
+ decompose_region (obj, (Sloc (M.field loc f)))
+ in
+ List.(concat (map slocs_of_field fields))
+
+ | C_array { arr_flat = Some { arr_size=len ; arr_cell=typ } } ->
+ let obj = Ctypes.object_of typ in
+ decompose_range loc obj Z.zero (Z.of_int (len - 1))
+ end
+
+ | Sarray (loc, obj, n) ->
+ decompose_range loc obj Z.zero (Z.of_int (n - 1))
+
+ | Srange (loc, obj, Some b, Some e)
+ when is_primitive_int b && is_primitive_int e ->
+ let b, e = match Lang.F.repr b, Lang.F.repr e with
+ | Kint b, Kint e -> b, e
+ | _ -> assert false (* by match guard *)
+ in
+ decompose_range loc obj b e
+
+ | _ ->
+ (* It is not trivial to go further: the list of regions depends on some
+ unknown values (length of the range, property, ...) *)
+ [obj, sloc]
+
+ and decompose_range l obj b e =
+ let rec generate_i l f i =
+ if Z.leq i b then l
+ else generate_i (f i :: l) f (Z.sub i Z.one)
+ in
+ let slocs_of_index i =
+ let l = M.shift l obj (e_zint i) in
+ decompose_region (obj, (Sloc l))
+ in
+ List.(concat (generate_i [] slocs_of_index e))
+
+ let rec assignable_region ~unfold reg assignable =
+ let check_inclusion reg =
+ p_any (L.included reg) assignable
+ in
+ if unfold then
+ (* This phase unfolds terms that cannot be "statically" unfolded *)
+ let logic_decompose = function
+ | (_, Sloc _) as s -> check_inclusion s
+ | (_, Sarray _) -> assert false (* decompose always remove Sarray *)
+ | (obj, Sdescr(xs, l, p)) ->
+ let sloc = obj, Sloc l in
+ p_forall xs
+ (p_imply p (assignable_region ~unfold:true sloc assignable))
+ | (_, Srange(l, obj, low, up)) ->
+ let x = Lang.freshvar ~basename:"k" Lang.t_int in
+ let k = e_var x in
+ let p = Vset.in_range k low up in
+ let sloc = obj, Sloc (M.shift l obj k) in
+ p_forall [x]
+ (p_imply p (assignable_region ~unfold:true sloc assignable))
+ in
+ p_all logic_decompose (decompose_region reg)
+ else
+ check_inclusion reg
+
+ let check_assigns ~unfold sigma ~written ~assignable =
p_all
- (fun seg ->
+ (fun reg ->
p_imply
- (p_not (L.invalid sigma seg))
- (p_any (L.included seg) assignable)
+ (p_not (L.invalid sigma reg))
+ (assignable_region ~unfold reg assignable)
) (written : region)
end
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 1b594803754f617a5c0b63f94f1216275517fed2..7973ef55de1f91cbfe3add483da6c92857d7fe99 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -812,7 +812,8 @@ sig
Compute a formula that checks whether written locations are either
invalid (at the given memory location)
or included in some assignable region. *)
- val check_assigns : sigma -> written:region -> assignable:region -> pred
+ val check_assigns :
+ unfold:bool -> sigma -> written:region -> assignable:region -> pred
end
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ebf53f21db45ecbb6bf1ff01e0d28e5bc80355b2..4c8d46d3d00443aaefd896971c047f3baa1f6441 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -517,7 +517,8 @@ struct
(* -------------------------------------------------------------------------- *)
let assigns_condition (region : L.region) (e:effect) : F.pred =
- L.check_assigns e.e_valid ~written:region ~assignable:e.e_region
+ let unfold = Wp_parameters.UnfoldAssigns.get () in
+ L.check_assigns ~unfold e.e_valid ~written:region ~assignable:e.e_region
exception COLLECTED
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
index 60291308af6ae635ff1c00dd98d81a973bf7cae4..8178bf2d553950d783cd9c829f626c5574b4736e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
@@ -97,6 +97,47 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3
Call Effect at line 30
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function PARTIAL_ASSIGNS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Assume {
+ Have: 0 <= n.
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, x).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
+ included(a, x, shift_sint32(p, n), 1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Assume {
+ Have: 0 <= n.
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, x).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
+ included(a, x, shift_sint32(p, n), 1).
+
------------------------------------------------------------
------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
index f681ec0f92309c15f8c0dc760963fec77f356d88..cb15fe7af3f09bc7706116d160649805b61523ac 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
@@ -79,6 +79,43 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3
Call Effect at line 30
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function PARTIAL_ASSIGNS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= n) /\
+ (!invalid(Malloc_0, shift_sint32(p, 0), 1 + n)).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/
+ included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= n) /\
+ (!invalid(Malloc_0, shift_sint32(p, 0), 1 + n)).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/
+ included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1).
+
------------------------------------------------------------
------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
index 54ba848675c17ebfc2d7605e528b461568515c34..24c9a9347bd05dfa3c7f3f9c139b8b04a090fc21 100644
--- a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
+++ b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
@@ -64,3 +64,12 @@ void ASSIGN_NO_UNFOLD_KO(struct S *s) {
struct S p = { 0,1 };
*s = p ;
}
+
+/*@ assigns *(p+(0..n)); */
+void f_assigns_array(int *p, unsigned n);
+
+/*@ requires n > 4 ;
+ assigns *(p+0), *(p+(1..n-1)), *(p+n); */
+void PARTIAL_ASSIGNS(int *p, unsigned n) {
+ f_assigns_array(p, n);
+}