Skip allocates by default until WP support them

src/kernel_internals/typing/populate_spec.ml

@@ -538,13 +538,16 @@ let get_mode = function
   | "skip" -> Skip
   | s -> Other s
 
-let build_config mode = {
-  exits = mode;
-  assigns = mode;
-  requires = mode;
-  allocates = mode;
-  terminates = mode;
-}
+let build_config mode =
+  (* For now Allocates are skipped by default *)
+  let skip_mode = match mode with Other _ -> mode | _ -> Skip in
+  {
+    exits = mode;
+    assigns = mode;
+    requires = mode;
+    allocates = skip_mode;
+    terminates = mode;
+  }
 
 let get_config_default () =
   build_config @@ get_mode @@ Kernel.GeneratedSpecMode.get ()

tests/spec/default_spec_combine.i

@@ -2,8 +2,8 @@
 
    MODULE: @PTEST_NAME@
    STDOPT: +"-generated-spec-mode donothing"
-   STDOPT: +"-generated-spec-mode safe"
-   STDOPT: +"-generated-spec-mode frama-c"
+   STDOPT: +"-generated-spec-mode safe -generated-spec-custom allocates:safe"
+   STDOPT: +"-generated-spec-mode frama-c -generated-spec-custom allocates:frama-c"
 */
 
 /*@ axiomatic a {

tests/spec/default_spec_mode.i

 /* run.config
    STDOPT: +"-no-generate-default-spec"
    STDOPT: +"-generated-spec-mode skip"
-   STDOPT: +"-generated-spec-mode acsl"
-   STDOPT: +"-generated-spec-mode safe"
-   STDOPT: +"-generated-spec-mode frama-c"
+   STDOPT: +"-generated-spec-mode acsl -generated-spec-custom allocates:acsl"
+   STDOPT: +"-generated-spec-mode safe -generated-spec-custom allocates:safe"
+   STDOPT: +"-generated-spec-mode frama-c -generated-spec-custom allocates:frama-c"
    STDOPT: +"-generated-spec-custom exits:acsl,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
 
    EXIT: 1