diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index deb19048d7f1333a4ec631f1fe381759d97aa286..b982750d8a3aac211fcd53a7c92a82a46ea9e798 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -228,11 +228,19 @@ let reverse_loop_contract l = {
   loop_assigns = List.rev l.loop_assigns ;
 }
 
+let default_assigns stmt l = {
+  l with
+  loop_assigns =
+    if l.loop_assigns <> [] then l.loop_assigns
+    else [WpPropId.mk_loop_any_assigns_info stmt]
+}
+
 let get_loop_contract kf stmt : loop_contract =
   let labels = NormAtLabels.labels_loop stmt in
   let normalize_pred p = NormAtLabels.preproc_annot labels p in
   let normalize_annot (i,p) = i, normalize_pred p in
   let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
+  default_assigns stmt @@
   reverse_loop_contract @@
   Annotations.fold_code_annot
     begin fun _emitter ca l ->
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 6c491d3f8d7289d8ac8b5171fc9dfa6f254047dc..dc142fc329cc32e090d18143b1f80fe319193e0f 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -143,7 +143,10 @@ struct
   let use_assigns env (a : assigns) w =
     match a with
     | NoAssignsInfo -> assert false
-    | AssignsAny ad -> W.use_assigns env.we None ad w
+    | AssignsAny ad ->
+        Wp_parameters.warning ~current:true ~once:true
+          "Missing assigns clause (assigns 'everything' instead)" ;
+        W.use_assigns env.we None ad w
     | AssignsLocations(ap,ad) -> W.use_assigns env.we (Some ap) ad w
 
   let prove_assigns env (a : assigns) w =