From 5c996df8d10e36bbcee7efd42099752eb8a34167 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 3 Sep 2021 09:13:38 +0200
Subject: [PATCH] [kernel] Fix crash with populated spec copy
---
src/kernel_services/visitors/visitor.ml | 10 ++++++----
tests/spec/non_ast_spec_copy.i | 9 +++++++++
tests/spec/non_ast_spec_copy.ml | 14 ++++++++++++++
tests/spec/oracle/non_ast_spec_copy.res.oracle | 1 +
4 files changed, 30 insertions(+), 4 deletions(-)
create mode 100644 tests/spec/non_ast_spec_copy.i
create mode 100644 tests/spec/non_ast_spec_copy.ml
create mode 100644 tests/spec/oracle/non_ast_spec_copy.res.oracle
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 220f5950783..cdb006d3a1e 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -408,10 +408,8 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
{ spec_behavior = snd (List.split old_behaviors);
spec_complete_behaviors = snd (List.split old_complete);
spec_disjoint_behaviors = snd (List.split old_disjoint);
- spec_terminates =
- (Option.map snd) old_terminates;
- spec_variant =
- (Option.map snd) old_decreases
+ spec_terminates = Option.map snd old_terminates;
+ spec_variant = Option.map snd old_decreases
}
in
let res = self#vspec spec in
@@ -430,6 +428,10 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
b')
old_behaviors
in
+ Queue.add
+ (fun () ->
+ ignore (Annotations.funspec ~populate:false new_kf))
+ self#get_filling_actions ;
let new_terminates =
Option.map
(fun (e,t) ->
diff --git a/tests/spec/non_ast_spec_copy.i b/tests/spec/non_ast_spec_copy.i
new file mode 100644
index 00000000000..6b0ef4c550a
--- /dev/null
+++ b/tests/spec/non_ast_spec_copy.i
@@ -0,0 +1,9 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ OPT: -copy
+*/
+
+// to be populated by non_ast_spec_copy.ml
+void function(void){
+
+}
diff --git a/tests/spec/non_ast_spec_copy.ml b/tests/spec/non_ast_spec_copy.ml
new file mode 100644
index 00000000000..03faef2019e
--- /dev/null
+++ b/tests/spec/non_ast_spec_copy.ml
@@ -0,0 +1,14 @@
+let add_terminates_true _ =
+ let terminates pred_loc =
+ Logic_const.(new_predicate { ptrue with pred_loc })
+ in
+ let add_terminates kf =
+ if Annotations.terminates ~populate:false kf = None then
+ Annotations.add_terminates
+ Emitter.kernel kf (terminates @@ Kernel_function.get_location kf)
+ in
+ Globals.Functions.iter add_terminates
+
+let () =
+ let category = File.register_code_transformation_category "my_category" in
+ File.add_code_transformation_after_cleanup category add_terminates_true
diff --git a/tests/spec/oracle/non_ast_spec_copy.res.oracle b/tests/spec/oracle/non_ast_spec_copy.res.oracle
new file mode 100644
index 00000000000..cefe9a19bcb
--- /dev/null
+++ b/tests/spec/oracle/non_ast_spec_copy.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/spec/non_ast_spec_copy.i (no preprocessing)
--
GitLab