[kernel] Fix crash with populated spec copy

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) ->

tests/spec/non_ast_spec_copy.i

+/* run.config
+   MODULE: @PTEST_NAME@
+   OPT: -copy
+*/
+
+// to be populated by non_ast_spec_copy.ml
+void function(void){
+
+}

tests/spec/non_ast_spec_copy.ml

+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

tests/spec/oracle/non_ast_spec_copy.res.oracle

+[kernel] Parsing tests/spec/non_ast_spec_copy.i (no preprocessing)