From a336be9b3f29a2bf18f7501e6637cddcaa66abc6 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 2 Aug 2023 15:29:38 +0200
Subject: [PATCH] Only generate proto specs from Annotations.funspec
---
src/kernel_internals/typing/populate_spec.ml | 21 +++++++++++++------
src/kernel_internals/typing/populate_spec.mli | 2 +-
src/kernel_services/ast_queries/file.ml | 3 ++-
tests/spec/default_spec_combine.ml | 8 ++++++-
tests/spec/default_spec_custom.ml | 10 ++++++++-
tests/spec/default_spec_mode.i | 1 +
.../oracle/default_spec_custom.0.res.oracle | 4 ++++
.../oracle/default_spec_custom.1.res.oracle | 4 ++++
.../oracle/default_spec_mode.0.res.oracle | 1 +
.../oracle/default_spec_mode.1.res.oracle | 1 +
.../oracle/default_spec_mode.2.res.oracle | 5 ++---
.../oracle/default_spec_mode.3.res.oracle | 4 +---
.../oracle/default_spec_mode.4.res.oracle | 7 ++-----
.../oracle/default_spec_mode.5.res.oracle | 5 +----
14 files changed, 51 insertions(+), 25 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 24d88efe2ed..bbbbd7b7fc2 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -549,11 +549,11 @@ let build_config mode =
terminates = mode;
}
-let get_config_default () =
+let get_config_mode () =
build_config @@ get_mode @@ Kernel.GeneratedSpecMode.get ()
let get_config () =
- let default = get_config_default () in
+ let default = get_config_mode () in
let collect (k,v) conf =
let mode = get_mode (Option.get v) in
match k with
@@ -572,7 +572,6 @@ let get_config () =
let do_populate kf original_spec =
let config = get_config () in
-
let exits = Exits.get_default config.exits kf original_spec in
let assigns = Assigns.get_default config.assigns kf original_spec in
let requires = Requires.get_default config.requires kf original_spec in
@@ -613,12 +612,22 @@ module Is_populated =
let () = Ast.add_linked_state Is_populated.self
-let populate_funspec kf spec =
- if not @@ Kernel.GenerateDefaultSpec.get() || Is_populated.mem kf then false
+let populate_funspec ~force kf spec =
+ let is_proto = not @@ Kernel_function.has_definition kf in
+ let skip_generation = not @@ Kernel.GenerateDefaultSpec.get () in
+ let is_empty_spec = Cil.is_empty_funspec spec in
+ let skip_proto = is_proto && not force && is_empty_spec in
+ if (not force && skip_generation) || Is_populated.mem kf || skip_proto
+ then false
else begin
+ if is_proto && is_empty_spec then
+ Kernel.warning ~once:true ~current:true ~wkey:Kernel.wkey_missing_spec
+ "Neither code nor specification for function %a, \
+ generating default specs from the prototype"
+ Kernel_function.pretty kf;
do_populate kf spec;
Is_populated.add kf ();
true
end
-let () = Annotations.populate_spec_ref := populate_funspec
+let () = Annotations.populate_spec_ref := populate_funspec ~force:true
diff --git a/src/kernel_internals/typing/populate_spec.mli b/src/kernel_internals/typing/populate_spec.mli
index 940da158cfb..27ae84f04b6 100644
--- a/src/kernel_internals/typing/populate_spec.mli
+++ b/src/kernel_internals/typing/populate_spec.mli
@@ -60,4 +60,4 @@ val register :
?status_terminates:status ->
string -> unit
-val populate_funspec : kernel_function -> spec -> bool
+val populate_funspec : force:bool -> kernel_function -> spec -> bool
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 3b93f038bb9..36bb0e417a4 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1189,7 +1189,8 @@ let () =
let populate_spec () =
let add_spec kf =
- ignore @@ Populate_spec.populate_funspec kf (Annotations.funspec kf)
+ ignore @@ Populate_spec.populate_funspec ~force:false kf
+ (Annotations.funspec ~populate:false kf)
in
Globals.Functions.iter add_spec
diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml
index dd81d458061..6261077f996 100644
--- a/tests/spec/default_spec_combine.ml
+++ b/tests/spec/default_spec_combine.ml
@@ -14,6 +14,12 @@ let status_allocates = Property_status.Dont_know
let gen_terminates _ _ = None
let status_terminates = Property_status.Dont_know
+let run () =
+ let get_spec kf =
+ ignore(Annotations.funspec kf)
+ in
+ Globals.Functions.iter get_spec
+
let populate () =
Format.printf "Registering an mode that does nothing@.";
Populate_spec.register
@@ -25,4 +31,4 @@ let populate () =
"donothing"
- let () = Cmdline.run_after_configuring_stage populate
+let () = Cmdline.run_after_configuring_stage populate
diff --git a/tests/spec/default_spec_custom.ml b/tests/spec/default_spec_custom.ml
index 5220b814145..826cd252d44 100644
--- a/tests/spec/default_spec_custom.ml
+++ b/tests/spec/default_spec_custom.ml
@@ -26,6 +26,12 @@ let status_assigns = Property_status.True
let status_allocates = Property_status.Dont_know
let status_terminates = Property_status.Dont_know
+let run () =
+ let get_spec kf =
+ ignore(Annotations.funspec kf)
+ in
+ Globals.Functions.iter get_spec
+
let populate () =
Format.printf "Registering an empty spec generation mode@.";
Populate_spec.register "emptymode";
@@ -39,4 +45,6 @@ let populate () =
"mymode"
- let () = Cmdline.run_after_configuring_stage populate
+let () = Cmdline.run_after_configuring_stage populate
+
+let () = Db.Main.extend run
diff --git a/tests/spec/default_spec_mode.i b/tests/spec/default_spec_mode.i
index 8c987bb116f..de2d911f8ef 100644
--- a/tests/spec/default_spec_mode.i
+++ b/tests/spec/default_spec_mode.i
@@ -21,6 +21,7 @@ void f2(){
}
// Test for automatic assigns
+//@ requires \true;
int f3(int* a);
// Has behavior by default
diff --git a/tests/spec/oracle/default_spec_custom.0.res.oracle b/tests/spec/oracle/default_spec_custom.0.res.oracle
index 72faead364b..fda41e6d630 100644
--- a/tests/spec/oracle/default_spec_custom.0.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.0.res.oracle
@@ -6,10 +6,14 @@ Registering a new spec generation mode
[kernel] Warning: Custom generation from mode emptymode not defined for requires, using frama-c mode instead
[kernel] Warning: Custom generation from mode emptymode not defined for allocates, using frama-c mode instead
[kernel] Warning: Custom generation from mode emptymode not defined for terminates, using frama-c mode instead
+[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+ Neither code nor specification for function f1, generating default specs from the prototype
[kernel] Warning: Custom status from mode emptymode not defined for exits
[kernel] Warning: Custom status from mode emptymode not defined for assigns
[kernel] Warning: Custom status from mode emptymode not defined for allocates
[kernel] Warning: Custom status from mode emptymode not defined for terminates
+[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+ Neither code nor specification for function f3, generating default specs from the prototype
/* Generated by Frama-C */
/*@ terminates \true;
exits \false;
diff --git a/tests/spec/oracle/default_spec_custom.1.res.oracle b/tests/spec/oracle/default_spec_custom.1.res.oracle
index 7c6188e9550..3151473f64c 100644
--- a/tests/spec/oracle/default_spec_custom.1.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.1.res.oracle
@@ -1,6 +1,10 @@
Registering an empty spec generation mode
Registering a new spec generation mode
[kernel] Parsing default_spec_custom.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+ Neither code nor specification for function f1, generating default specs from the prototype
+[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+ Neither code nor specification for function f3, generating default specs from the prototype
/* Generated by Frama-C */
/*@ requires \false;
terminates \false;
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index 9624686acc4..e36e7137656 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -8,6 +8,7 @@ void f2(void)
return;
}
+/*@ requires \true; */
int f3(int *a);
/*@ requires \true;
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
index 9624686acc4..e36e7137656 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -8,6 +8,7 @@ void f2(void)
return;
}
+/*@ requires \true; */
int f3(int *a);
/*@ requires \true;
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index ecda6945556..e3d1b2a70b4 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -1,7 +1,5 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
/* Generated by Frama-C */
-/*@ terminates \true;
- allocates \nothing; */
void f1(void);
/*@ terminates \true;
@@ -12,7 +10,8 @@ void f2(void)
return;
}
-/*@ terminates \true;
+/*@ requires \true;
+ terminates \true;
allocates \nothing; */
int f3(int *a);
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index 9ae4d897289..a9f745a0148 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,7 +1,5 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
/* Generated by Frama-C */
-/*@ requires \false;
- terminates \false; */
void f1(void);
/*@ terminates \true;
@@ -14,7 +12,7 @@ void f2(void)
return;
}
-/*@ requires \false;
+/*@ requires \true;
terminates \false; */
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 272ef95df50..90038462eb5 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -1,9 +1,5 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
/* Generated by Frama-C */
-/*@ terminates \true;
- exits \false;
- assigns \nothing;
- allocates \nothing; */
void f1(void);
/*@ terminates \true;
@@ -15,7 +11,8 @@ void f2(void)
return;
}
-/*@ terminates \true;
+/*@ requires \true;
+ terminates \true;
exits \false;
assigns \result, *a;
assigns \result \from *a;
diff --git a/tests/spec/oracle/default_spec_mode.5.res.oracle b/tests/spec/oracle/default_spec_mode.5.res.oracle
index 1fa027e6baf..69c1b68dab3 100644
--- a/tests/spec/oracle/default_spec_mode.5.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.5.res.oracle
@@ -1,8 +1,5 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
/* Generated by Frama-C */
-/*@ requires \false;
- terminates \true;
- assigns \nothing; */
void f1(void);
/*@ terminates \true;
@@ -13,7 +10,7 @@ void f2(void)
return;
}
-/*@ requires \false;
+/*@ requires \true;
terminates \true;
assigns \result, *a;
assigns \result \from *a;
--
GitLab