[tests] Fix and update Populate_spec example

doc/developer/Makefile

@@ -86,7 +86,7 @@ check-hello-v7: check-hello-clean
 # For check-examples, we perform no explicit oracle comparisons:
 # we simply build the code and run tests (which must always succeed).
 check-examples: check-examples-acsl_extension_foo check-examples-acsl_extension_ext_types \
-  check-examples-callstack check-examples-syntactic_check
+  check-examples-callstack check-examples-syntactic_check check-examples-populate_spec
 
 check-examples-clean:
 	$(ECHO) Cleaning example files...
@@ -105,6 +105,8 @@ check-examples-callstack: check-examples-clean
 check-examples-syntactic_check: check-examples-clean
 	cd examples/syntactic_check && $(duneb) @install && frama-c-ptests >/dev/null && $(duneb) @ptests 2>&1
 
+check-examples-populate_spec: check-examples-clean
+	cd examples/populate_spec && $(duneb) @install && frama-c-ptests >/dev/null && $(duneb) @ptests 2>&1
 
 check-all: developer.pdf
 	$(MAKE) -C ../.. check-devguide

doc/developer/examples/populate_spec/populate.ml

@@ -15,14 +15,14 @@ let gen_exits _ _ =
 (* Generate assigns for prototypes. *)
 let gen_assigns kf _ =
   if Kernel_function.has_definition kf then
-    WritesAny
+    Writes []
   else Writes (Infer_assigns.from_prototype kf)
 
 (* Generate requires \false clauses. *)
 let gen_requires _ _ = [ Logic_const.(new_predicate pfalse) ]
 
 (* Generate allocates \nothing clauses. *)
-let gen_allocates kf _ =
+let gen_allocates _ _ =
   FreeAlloc([],[])
 
 (* Generate terminates \false for prototypes. *)

doc/developer/examples/populate_spec/tests/example/oracle/div.res.oracle

-[kernel] Parsing div.c (with preprocessing)
-/* Generated by Frama-C */
-int main(void)
-{
-  int a;
-  int b;
-  int c;
-  a = 1;
-  b = 2;
-  /*@ assert b ≢ 0; */
-  c = a / b;
-  return c;
-}
-
-

doc/developer/examples/populate_spec/tests/example/oracle/populate.res.oracle

+Registering a new spec generation mode
+[kernel] Parsing populate.c (with preprocessing)
+[kernel:annot:missing-spec] populate.c:13: Warning: 
+  Neither code nor explicit exits, assigns, requires, allocates and terminates for function f,
+   generating default clauses (some from the specification). See -generated-spec-* options for more info
+/* Generated by Frama-C */
+/*@ requires \false;
+    terminates \false;
+    exits \false;
+    assigns *bar;
+    assigns *bar \from bar;
+    allocates \nothing;
+    
+    behavior A:
+      assigns *bar;
+      assigns *bar \from bar;
+    
+    behavior B:
+      assigns \nothing;
+    
+    complete behaviors B, A;
+ */
+int f(int *bar);
+
+/*@ requires \false;
+    exits \false;
+    assigns \nothing;
+    allocates \nothing; */
+int g(void)
+{
+  int tmp;
+  int foo = 42;
+  tmp = f(& foo);
+  return tmp;
+}
+
+

doc/developer/examples/populate_spec/tests/example/div.c → doc/developer/examples/populate_spec/tests/example/populate.c

 /* run.config
-   OPT: -check -generated-spec-mode mymode -then-last -print
+   OPT: -check -generated-spec-mode mymode -print
 */
 
 /*@ behavior A: