From 099c5445b446ec416e3124c35b78fc83c6cfbbd5 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 1 Aug 2023 14:23:54 +0200
Subject: [PATCH] Skip allocates by default until WP support them
---
src/kernel_internals/typing/populate_spec.ml | 17 ++++++++++-------
tests/spec/default_spec_combine.i | 4 ++--
tests/spec/default_spec_mode.i | 6 +++---
3 files changed, 15 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index b8e231f8f76..24d88efe2ed 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 7910730ee26..29c80655c6c 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 5ddda215b76..8c987bb116f 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
--
GitLab