Merge branch 'fix/martin/kernel/do-not-add-empty-default-behavior' into 'master'

Add the newly created behavior only if it is not empty

See merge request frama-c/frama-c!4370

src/kernel_internals/typing/populate_spec.ml

@@ -869,19 +869,23 @@ let do_populate ?loc kf clauses =
 
   let generated original = function
     | Kept -> original
-    | Generated g -> g
+    | Generated clauses -> clauses
   in
 
   let bhv = Cil.mk_behavior () in
-  let bhv = { bhv with b_post_cond = generated bhv.b_post_cond exits } in
-  let bhv = { bhv with b_assigns = generated bhv.b_assigns assigns } in
-  let bhv = { bhv with b_requires = generated bhv.b_requires requires } in
-  let bhv = { bhv with b_allocation = generated bhv.b_allocation allocates } in
+  bhv.b_post_cond <- generated bhv.b_post_cond exits;
+  bhv.b_assigns <- generated bhv.b_assigns assigns;
+  bhv.b_requires <- generated bhv.b_requires requires;
+  bhv.b_allocation <- generated bhv.b_allocation allocates;
+
+  let is_empty_bhv =
+    exits = Kept && assigns = Kept && requires = Kept && allocates = Kept
+  in
 
   let spec = Cil.empty_funspec () in
-  let spec = { spec with spec_behavior = [ bhv ] } in
-  let spec =
-    { spec with spec_terminates = generated spec.spec_terminates terminates } in
+  spec.spec_behavior <- if is_empty_bhv then spec.spec_behavior else [ bhv ];
+  spec.spec_terminates <- generated spec.spec_terminates terminates;
+
   Annotations.add_spec emitter_populate kf spec;
   Exits.emit config.c_exits kf bhv exits;
   Assigns.emit config.c_assigns kf bhv assigns;

tests/value/oracle/behavior_statuses.1.res.oracle

@@ -13,9 +13,6 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[kernel:prop-status:emit] 
-  Frama-C kernel emits status unknown for property default behavior
-  under 2 hypothesis
 [eva] computing for function f <- main.
   Called from behavior_statuses.i:26.
 [eva] using specification for function f