[wp] Refacto CfgAnnot

src/plugins/wp/cfgAnnot.ml

@@ -190,35 +190,54 @@ let wp_populate_terminates =
     ~correctness:[] (* TBC *)
     ~tuning:[] (* TBC *)
 
-let get_terminates kf =
+type terminates_clause =
+  | Defined of WpPropId.prop_id * predicate
+  | Assumed of predicate
+
+let get_terminates_clause kf =
+  (* Note:
+   *  - user-defined terminates always returns Defined
+   *  - generated "terminates \true" are:
+   *      - first handled in a None case and returns Defined
+   *      - then handled in a Some case (as user defined) and returns Defined *)
+  let defined p =
+    Defined (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p) in
+  let populate_true () =
+    let p = Logic_const.new_predicate @@ Logic_const.ptrue in
+    Wp_parameters.warning
+      ~source:(fst @@ Kernel_function.get_location kf) ~once:true
+      "Missing terminates clause for %a, populates 'terminates \\true'"
+      Kernel_function.pretty kf ;
+    Annotations.add_terminates wp_populate_terminates kf p ;
+    defined p
+  in
   match Annotations.terminates kf with
-  | None
-    when Kernel_function.is_definition kf &&
-         Wp_parameters.TerminatesDefinitions.get () ->
-      let p = Logic_const.new_predicate @@ Logic_const.ptrue in
-      Wp_parameters.warning
-        ~source:(fst @@ Kernel_function.get_location kf) ~once:true
-        "Missing terminates clause for %a, populates 'terminates \\true'"
-        Kernel_function.pretty kf ;
-      Annotations.add_terminates wp_populate_terminates kf p ;
-      Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
+  | 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 ()
+      then Assumed Logic_const.pfalse
+      else populate_true ()
   | None ->
-      None
+      if not @@ Wp_parameters.TerminatesExtDeclarations.get ()
+      then Assumed Logic_const.pfalse
+      else Assumed Logic_const.ptrue
   | Some p ->
-      Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
+      defined p
+
+let get_terminates_goal kf =
+  match get_terminates_clause kf with
+  | Assumed _ -> None
+  | Defined (id, p) -> Some (id, p)
 
 let get_terminates_hyp kf =
-  let to_default option =
-    if option then Logic_const.ptrue else Logic_const.pfalse in
-  match Annotations.terminates kf with
-  | Some p ->
-      false, normalize_terminates p
-  | None when Kernel_function.is_in_libc kf ->
-      false, to_default @@ Wp_parameters.TerminatesFCDeclarations.get ()
-  | None when Kernel_function.is_definition kf ->
-      true, to_default @@ Wp_parameters.TerminatesDefinitions.get ()
-  | None ->
-      true, to_default @@  Wp_parameters.TerminatesExtDeclarations.get ()
+  match get_terminates_clause kf with
+  | Defined (_, p) -> false, p
+  | Assumed p -> true, p
 
 (* -------------------------------------------------------------------------- *)
 (* --- Contracts                                                          --- *)

src/plugins/wp/cfgAnnot.mli

@@ -56,7 +56,7 @@ val get_behavior_goals :
 val get_complete_behaviors : kernel_function -> pred_info list
 val get_disjoint_behaviors : kernel_function -> pred_info list
 
-val get_terminates : kernel_function -> pred_info option
+val get_terminates_goal : kernel_function -> pred_info option
 
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Assertions                                    --- *)
@@ -105,7 +105,7 @@ type contract = {
   contract_exit : pred_info list ;
   contract_smoke : pred_info list ;
   contract_assigns : assigns ;
-  contract_terminates : bool * predicate ; (* boolean: default generated *)
+  contract_terminates : bool * predicate ; (* boolean: assumed terminates *)
 }
 
 val get_call_contract : ?smoking:stmt -> kernel_function -> stmt -> contract

src/plugins/wp/cfgCalculus.ml

@@ -414,7 +414,7 @@ struct
          WpLog.SmokeTests.get () &&
          WpLog.SmokeDeadcode.get ()
       then CfgInfos.smoking infos else (fun _ -> false) in
-    let terminates = CfgAnnot.get_terminates kf in
+    let terminates = CfgAnnot.get_terminates_goal kf in
     let env = {
       mode ; props ; body ;
       succ ; dead ; terminates ;

src/plugins/wp/cfgInfos.ml

@@ -328,7 +328,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
     (fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
     infos.doomed ;
   (* Trivial terminates *)
-  begin match CfgAnnot.get_terminates kf with
+  begin match CfgAnnot.get_terminates_goal kf with
     | Some (id, _t)
       when selected_terminates ~prop kf
         && infos.calls = Fset.empty

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

@@ -6,6 +6,10 @@
   Missing terminates clause on call to declaration, defaults to \false
 [wp] tests/wp_acsl/terminates_call_options.c:28: Warning: 
   Missing terminates clause on call to definition, defaults to \false
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+  Missing terminates clause on call to exit, defaults to \false
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: 
+  Missing terminates clause on call to div, defaults to \false
 ------------------------------------------------------------
   Function call_declaration
 ------------------------------------------------------------
@@ -36,8 +40,14 @@ Prove: true.
   Function libc_call
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call':
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (1/2):
 Call Effect at line 37
 Prove: false.
 
 ------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (2/2):
+Call Effect at line 38
+Prove: false.
+
+------------------------------------------------------------

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

@@ -10,6 +10,10 @@
   Missing terminates clause on call to declaration, defaults to \true
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing assigns clause (assigns 'everything' instead)
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+  Missing terminates clause on call to exit, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: 
+  Missing terminates clause on call to div, defaults to \true
 ------------------------------------------------------------
   Function call_declaration
 ------------------------------------------------------------

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

@@ -6,18 +6,23 @@
   Missing terminates clause on call to declaration, defaults to \false
 [wp] tests/wp_acsl/terminates_call_options.c:28: Warning: 
   Missing terminates clause on call to definition, defaults to \false
-[wp] 4 goals scheduled
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+  Missing terminates clause on call to exit, defaults to \false
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: 
+  Missing terminates clause on call to div, defaults to \false
+[wp] 5 goals scheduled
 [wp] [Qed] Goal typed_definition_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_call_declaration_terminates : Unsuccess
 [wp] [Alt-Ergo] Goal typed_call_definition_terminates : Unsuccess
-[wp] [Alt-Ergo] Goal typed_libc_call_terminates : Unsuccess
-[wp] Proved goals:    1 / 4
+[wp] [Alt-Ergo] Goal typed_libc_call_terminates_part1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_libc_call_terminates_part2 : Unsuccess
+[wp] Proved goals:    1 / 5
   Qed:             1 
-  Alt-Ergo:        0  (unsuccess: 3)
+  Alt-Ergo:        0  (unsuccess: 4)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   definition                1        -        1       100%
   call_declaration          -        -        1       0.0%
   call_definition           -        -        1       0.0%
-  libc_call                 -        -        1       0.0%
+  libc_call                 -        -        2       0.0%
 ------------------------------------------------------------

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

@@ -10,6 +10,10 @@
   Missing terminates clause on call to declaration, defaults to \true
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing assigns clause (assigns 'everything' instead)
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+  Missing terminates clause on call to exit, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: 
+  Missing terminates clause on call to div, defaults to \true
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_definition_assigns : Valid
 [wp] [Qed] Goal typed_call_declaration_terminates : Valid

src/plugins/wp/tests/wp_acsl/terminates_call_options.c

@@ -35,4 +35,5 @@ void no_spec_generates_goal(void){
 //@ terminates \true ;
 void libc_call(void){
   (void) div(4,3);
+  exit(0);
 }