[wp] Populate terminates true for declarations

src/plugins/wp/cfgAnnot.ml

@@ -215,8 +215,6 @@ let get_terminates_clause kf =
   | None when Kernel_function.is_in_libc kf ->
       if not @@ Wp_parameters.TerminatesFCDeclarations.get ()
       then Assumed Logic_const.pfalse
-      else if not @@ Kernel_function.is_definition kf
-      then Assumed Logic_const.ptrue
       else populate_true ()
   | None when Kernel_function.is_definition kf ->
       if not @@ Wp_parameters.TerminatesDefinitions.get ()
@@ -225,7 +223,7 @@ let get_terminates_clause kf =
   | None ->
       if not @@ Wp_parameters.TerminatesExtDeclarations.get ()
       then Assumed Logic_const.pfalse
-      else Assumed Logic_const.ptrue
+      else populate_true ()
   | Some p ->
       defined p
 

src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle

@@ -6,14 +6,14 @@
   Missing terminates clause for definition, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: 
-  Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:17: Warning: 
+  Missing terminates clause for declaration, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:33: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: 
-  Missing terminates clause on call to exit, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
-  Missing terminates clause on call to div, defaults to \true
+[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning: 
+  Missing terminates clause for exit, populates 'terminates \true'
+[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning: 
+  Missing terminates clause for div, populates 'terminates \true'
 ------------------------------------------------------------
   Function call_declaration
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle

@@ -6,14 +6,14 @@
   Missing terminates clause for definition, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: 
-  Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:17: Warning: 
+  Missing terminates clause for declaration, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:33: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: 
-  Missing terminates clause on call to exit, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
-  Missing terminates clause on call to div, defaults to \true
+[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning: 
+  Missing terminates clause for exit, populates 'terminates \true'
+[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning: 
+  Missing terminates clause for div, populates 'terminates \true'
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_definition_assigns : Valid
 [wp] [Qed] Goal typed_call_declaration_terminates : Valid