diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 24d88efe2edc27fe3fb0cbb3fef8f2f178fbd45f..bbbbd7b7fc2f0d5e6df9c55181c2114865da1167 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 940da158cfb4ac7278bf6643c4cab05684390afd..27ae84f04b666934a5b768c68b53b05fda3b1ea2 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 3b93f038bb97a2d4f44e1f0da1d34c918a509ef7..36bb0e417a434e938b8c589cf42f5ddbe3d2241d 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 dd81d458061a8bb554e1786101617512e4768d12..6261077f996b4fcc155bba54723938dfea1bbf3d 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 5220b81414525f0cb8b1d67061ff3e0a51c585c6..826cd252d4412701ec30b57f22b403ff2e334582 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 8c987bb116f20c5e32154d4cdadff3aa31b1e2d3..de2d911f8eff7565ffae7f058c8865dfc174dfa8 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 72faead364b09e6ffb977a3f17cc0d821bcce069..fda41e6d63057da79517b773ecfedf608db05d4b 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 7c6188e9550932bf83949bb00aed55eb51aafbd8..3151473f64cd26f33ade3c2431e795f2627acd78 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 9624686acc4dc681db6c3c4cdb8154d4c0d74e2e..e36e713765661974785859139e5a07493fce89a5 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 9624686acc4dc681db6c3c4cdb8154d4c0d74e2e..e36e713765661974785859139e5a07493fce89a5 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 ecda6945556f64107334dff2970a6f836316414a..e3d1b2a70b4ab679c2049d735103be40dc5b7c66 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 9ae4d897289ffbd8f74e0cf478d39b5d3a0f23c8..a9f745a014834522381957113332b8a16232fdb6 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 272ef95df50d5a12434417a83eba8f2a9de6d888..90038462eb51543ab393e7acacb7d4349423df21 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 1fa027e6bafbd8c8b87585758b685659038e1249..69c1b68dab380444d5914c928ff3a3f6a6f7417c 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;