From f03ea97dfb4c3c117ae2b72451d800f11738c849 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 4 Oct 2023 17:57:51 +0200
Subject: [PATCH] Mode Skip is available in -generated-spec-custom option
---
src/kernel_internals/typing/populate_spec.ml | 20 ++++---
.../plugin_entry_points/kernel.ml | 7 ++-
tests/spec/default_spec_mode.i | 4 +-
.../oracle/default_spec_mode.3.res.oracle | 14 +++--
.../oracle/default_spec_mode.4.res.oracle | 53 +++++++++++++++++--
.../oracle/default_spec_mode.6.res.oracle | 4 ++
6 files changed, 85 insertions(+), 17 deletions(-)
create mode 100644 tests/spec/oracle/default_spec_mode.6.res.oracle
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 33896006eeb..ee60e886ad2 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -23,9 +23,11 @@
open Cil_types
type mode =
- | ACSL | Safe | Frama_C (* Modes available for specification generation. *)
- | Skip (* Internally used to skip generation. *)
- | Other of string (* Allow user to use a custom mode, see {!register}. *)
+ (* Modes available for specification generation. Skip is only available via
+ -generated-spec-custom (cf. option description). *)
+ | ACSL | Safe | Frama_C | Skip
+ (* Allow user to use a custom mode, see {!register}. *)
+ | Other of string
(* Allow customization, each clause can be handled with a different {!mode}. *)
type config = {
@@ -733,10 +735,16 @@ module Allocates = Make(Allocates_generator)
module Terminates = Make(Terminates_generator)
(* Convert string from parameter [-generated-spec-mode] to [mode]. *)
-let get_mode = function
+let get_mode ~allow_skip = function
| "frama-c" -> Frama_C
| "acsl" -> ACSL
| "safe" -> Safe
+ | "skip" when allow_skip -> Skip
+ | "skip" ->
+ Kernel.warning ~once:true
+ "Mode skip is only available via -generated-spec-custom.@, The mode \
+ frama-c will be used instead";
+ Frama_C
| s -> Other s
(* Given a [mode], returns the configuration for each clause. *)
@@ -751,14 +759,14 @@ let build_config mode =
(* Build configuration from parameter [-generated-spec-mode]. *)
let get_config_mode () =
- Kernel.GeneratedSpecMode.get () |> get_mode |> build_config
+ Kernel.GeneratedSpecMode.get () |> get_mode ~allow_skip:false |> build_config
(* Build the default configuration, then select modes depending on the
parameter [-generated-spec-custom]. *)
let get_config_custom () =
let default = get_config_mode () in
let collect (k,v) config =
- let mode = get_mode (Option.get v) in
+ let mode = get_mode ~allow_skip:true (Option.get v) in
match k with
| "exits" -> {config with c_exits = mode}
| "assigns" -> {config with c_assigns = mode}
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 27772d39e1f..4e4bef6d7a1 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1486,8 +1486,11 @@ module GeneratedSpecCustom =
let arg_name = "c1:m1,c2:m2,..."
let default = Datatype.String.Map.empty
let help =
- "Fine-tune missing specification generation by manually choosing \
- modes for each clause. See user manual for more information."
+ "Fine-tune missing specification generation by manually selecting \
+ modes for each clause. Can be one of: frama-c, acsl, safe, skip or \
+ the name of a custom registered mode. Do not use skip mode for \
+ assigns unless you know what you are doing! See user manual for more \
+ information."
end)
let normalization_parameters () =
diff --git a/tests/spec/default_spec_mode.i b/tests/spec/default_spec_mode.i
index e9023087582..87586463611 100644
--- a/tests/spec/default_spec_mode.i
+++ b/tests/spec/default_spec_mode.i
@@ -3,8 +3,8 @@
STDOPT: +"-generated-spec-mode acsl"
STDOPT: +"-generated-spec-mode safe"
STDOPT: +"-generated-spec-mode frama-c"
- STDOPT: +"-generated-spec-custom exits:acsl,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
-
+ STDOPT: +"-generated-spec-mode skip"
+ STDOPT: +"-generated-spec-custom exits:skip,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
EXIT: 1
STDOPT: +"-generated-spec-custom wrong_clause:safe"
STDOPT: +"-generated-spec-custom wrong_clause:"
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index 45eacc7b262..dfede74e220 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel] Warning: Mode skip is only available via -generated-spec-custom.
+ The mode frama-c will be used instead
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor specification for function f1,
generating default exits. See -generated-spec-* options for more info
@@ -6,7 +8,7 @@
Neither code nor explicit assigns for function f1,
generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Neither code nor explicit requires for function f1,
+ Neither code nor explicit allocates for function f1,
generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor explicit terminates for function f1,
@@ -17,14 +19,17 @@
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor explicit assigns for function f3,
generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor explicit allocates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor explicit terminates for function f3,
generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
-/*@ requires \false;
- terminates \true;
+/*@ terminates \true;
exits \false;
- assigns \nothing; */
+ assigns \nothing;
+ allocates \nothing; */
void f1(void);
/*@ terminates \true;
@@ -43,6 +48,7 @@ void f2(void)
assigns \result, *a;
assigns \result \from *a;
assigns *a \from *a;
+ allocates \nothing;
*/
int f3(int *a);
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
index d131bef3d3d..ac0f46d5162 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -1,4 +1,51 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
-[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
- Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
-[kernel] Frama-C aborted: invalid user input.
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor specification for function f1,
+ generating default assigns. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor explicit requires for function f1,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor explicit terminates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor explicit assigns for function f3,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor explicit terminates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
+/* Generated by Frama-C */
+/*@ requires \false;
+ terminates \true;
+ assigns \nothing; */
+void f1(void);
+
+/*@ terminates \true;
+ assigns \nothing;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ requires \true;
+ terminates \true;
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ */
+int f3(int *a);
+
+/*@ requires \true;
+ terminates \true;
+ assigns *b;
+ allocates \nothing; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.6.res.oracle b/tests/spec/oracle/default_spec_mode.6.res.oracle
new file mode 100644
index 00000000000..d131bef3d3d
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.6.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
+ Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
+[kernel] Frama-C aborted: invalid user input.
--
GitLab