diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml index b8e231f8f763164dfa77646806e5639f2878d070..24d88efe2edc27fe3fb0cbb3fef8f2f178fbd45f 100644 --- a/src/kernel_internals/typing/populate_spec.ml +++ b/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 () diff --git a/tests/spec/default_spec_combine.i b/tests/spec/default_spec_combine.i index 7910730ee26c916363e7519c8d9f091afe659635..29c80655c6cc90912e6967dfd83a900104237911 100644 --- a/tests/spec/default_spec_combine.i +++ b/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 { diff --git a/tests/spec/default_spec_mode.i b/tests/spec/default_spec_mode.i index 5ddda215b76545bc735ce5cc493a4116a0a29a99..8c987bb116f20c5e32154d4cdadff3aa31b1e2d3 100644 --- a/tests/spec/default_spec_mode.i +++ b/tests/spec/default_spec_mode.i @@ -1,9 +1,9 @@ /* 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