[wp] Fixes stmt assigns handling in CFG

src/plugins/wp/cfgAnnot.ml

@@ -392,7 +392,7 @@ let get_stmt_assigns kf stmt =
               ) l s.spec_behavior
         | _ -> l
       end stmt []
-  in if asgn = [] then [WpPropId.empty_assigns_info] else asgn
+  in if asgn = [] then [WpPropId.mk_stmt_any_assigns_info stmt] else asgn
 
 (* -------------------------------------------------------------------------- *)
 (* --- Code Assertions                                                    --- *)

src/plugins/wp/tests/wp/default-stmt-assigns.i

+void automaton_state_accessor() {
+  __asm__("");
+  //@ assert \false ;
+}

src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp/default-stmt-assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/default-stmt-assigns.i:2: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
+------------------------------------------------------------
+  Function automaton_state_accessor
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp/default-stmt-assigns.i, line 3):
+Prove: false.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp/default-stmt-assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/default-stmt-assigns.i:2: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_automaton_state_accessor_assert : Unsuccess
+[wp] Proved goals:    0 / 1
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  automaton_state_accessor   -       -        1       0.0%
+------------------------------------------------------------