[wp] Do not ignore main declaration

src/plugins/wp/cfgCalculus.ml

@@ -129,7 +129,7 @@ struct
   type env = {
     mode: mode;
     props: props;
-    cfg: Cfg.automaton;
+    cfg: Cfg.automaton option;
     we: W.t_env;
     wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
     mutable wk: W.t_prop; (* end point *)
@@ -179,7 +179,7 @@ struct
 
   exception NonNaturalLoop
 
-  let succ env a = G.succ_e env.cfg.graph a
+  let succ env a = G.succ_e (Option.get env.cfg).graph a
 
   let rec wp (env:env) (a:vertex) : W.t_prop =
     match Vhash.find env.wp a with
@@ -356,11 +356,12 @@ struct
     prove_assigns env b.bhv_exit_assigns w
 
   let do_funbehavior env ~formals (b : CfgAnnot.behavior) w =
+    let cfg = Option.get env.cfg in
     let wpost = do_post env ~formals b w in
     let wexit = do_exit env ~formals b w in
-    Vhash.add env.wp env.cfg.return_point (Some wpost) ;
+    Vhash.add env.wp cfg.return_point (Some wpost) ;
     env.wk <- wexit ;
-    wp env env.cfg.entry_point
+    wp env cfg.entry_point
 
   (* Putting everything together *)
   let compute ~mode ~props =
@@ -381,7 +382,9 @@ struct
       do_global_init env @@
       do_preconditions env ~formals bhv @@
       do_complete_disjoint env @@
-      do_funbehavior env ~formals bhv @@
+      (if Kernel_function.has_definition kf
+       then do_funbehavior env ~formals bhv
+       else Extlib.id) @@
       W.empty
     end
 

src/plugins/wp/cfgGenerator.ml

@@ -162,12 +162,11 @@ let strategy_main model task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
       LogicUsage.iter_lemmas (lemma task ~prop) ;
     Wp_parameters.iter_fct
       (fun kf ->
-         if Kernel_function.has_definition kf then
-           let infos = get_kf_infos model kf ~bhv ~prop () in
-           if CfgInfos.annots infos then
-             if bhv=[]
-             then apply model task ~infos ~kf ()
-             else apply model task ~infos ~kf ~bhvs:(select kf bhv) ()
+         let infos = get_kf_infos model kf ~bhv ~prop () in
+         if CfgInfos.annots infos then
+           if bhv=[]
+           then apply model task ~infos ~kf ()
+           else apply model task ~infos ~kf ~bhvs:(select kf bhv) ()
       ) fct ;
     task.props <- (if prop=[] then `All else `Names prop);
   end

src/plugins/wp/cfgInfos.ml

@@ -30,7 +30,7 @@ module Shash = Cil_datatype.Stmt.Hashtbl
 (* -------------------------------------------------------------------------- *)
 
 type t = {
-  cfg : Cfg.automaton;
+  cfg : Cfg.automaton option;
   mutable annots : bool; (* has goals to prove *)
   mutable doomed : WpPropId.prop_id Bag.t;
   mutable calls : Kernel_function.Set.t;
@@ -60,7 +60,7 @@ let fixpoint h d f =
   in phi
 
 let unreachable infos =
-  let pred = Cfg.G.pred infos.cfg.graph in
+  let pred = Cfg.G.pred (Option.get infos.cfg).graph in
   fixpoint infos.unreachable true
     begin fun phi v -> List.for_all phi (pred v) end
 
@@ -120,6 +120,9 @@ let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
     (List.exists (selected_postcond ~prop) b.b_post_cond)
   end
 
+let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
+  (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop) b
+
 (* -------------------------------------------------------------------------- *)
 (* --- Calls                                                              --- *)
 (* -------------------------------------------------------------------------- *)
@@ -194,7 +197,10 @@ let loop_contract_pids kf stmt =
   | _ -> []
 
 let compile Key.{ kf ; bhv ; prop } =
-  let cfg = Cfg.get_automaton kf in
+  let cfg =
+    if Kernel_function.has_definition kf then Some (Cfg.get_automaton kf)
+    else None
+  in
   let infos = {
     cfg ;
     annots = false ;
@@ -202,36 +208,41 @@ let compile Key.{ kf ; bhv ; prop } =
     calls = Fset.empty ;
     unreachable = Vhash.create 32 ;
   } in
-  (* Root Reachability *)
-  let v0 = cfg.entry_point in
-  Vhash.add infos.unreachable v0 false ;
-  (* Spec Iteration *)
-  if selected_disjoint_complete kf ~bhv ~prop ||
-     List.exists
-       (selected_bhv ~bhv ~prop)
-       (Annotations.behaviors kf)
-  then infos.annots <- true ;
-  (* Stmt Iteration *)
-  Shash.iter
-    (fun stmt (src,_) ->
-       let fs = collect_calls ~bhv stmt in
-       let dead = unreachable infos src in
-       let ca = CfgAnnot.get_code_assertions kf stmt in
-       let ca_pids = List.map fst ca.code_verified in
-       let loop_pids = loop_contract_pids kf stmt in
-       if dead then begin
-         infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
-         infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
-       end else
-         begin
-           if not infos.annots &&
-              ( List.exists (selected ~bhv ~prop) ca_pids ||
-                List.exists (selected ~bhv ~prop) loop_pids ||
-                Fset.exists (selected_call ~bhv ~prop) fs )
-           then infos.annots <- true ;
-           infos.calls <- Fset.union fs infos.calls ;
-         end
-    ) cfg.stmt_table ;
+  let behaviors = Annotations.behaviors kf in
+  if WpStrategy.is_main_init kf then
+    infos.annots <- List.exists (selected_main_bhv ~bhv ~prop) behaviors ;
+
+  if Kernel_function.has_definition kf then begin
+    let cfg = Option.get cfg in
+    (* Root Reachability *)
+    let v0 = cfg.entry_point in
+    Vhash.add infos.unreachable v0 false ;
+    (* Spec Iteration *)
+    if selected_disjoint_complete kf ~bhv ~prop ||
+       (List.exists (selected_bhv ~bhv ~prop) behaviors)
+    then infos.annots <- true ;
+    (* Stmt Iteration *)
+    Shash.iter
+      (fun stmt (src,_) ->
+         let fs = collect_calls ~bhv stmt in
+         let dead = unreachable infos src in
+         let ca = CfgAnnot.get_code_assertions kf stmt in
+         let ca_pids = List.map fst ca.code_verified in
+         let loop_pids = loop_contract_pids kf stmt in
+         if dead then begin
+           infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
+           infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
+         end else
+           begin
+             if not infos.annots &&
+                ( List.exists (selected ~bhv ~prop) ca_pids ||
+                  List.exists (selected ~bhv ~prop) loop_pids ||
+                  Fset.exists (selected_call ~bhv ~prop) fs )
+             then infos.annots <- true ;
+             infos.calls <- Fset.union fs infos.calls ;
+           end
+      ) cfg.stmt_table ;
+  end ;
   (* Collected Infos *)
   infos
 

src/plugins/wp/cfgInfos.mli

@@ -30,7 +30,7 @@ module Cfg = Interpreted_automata
 val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
   unit -> t
 
-val cfg : t -> Cfg.automaton
+val cfg : t -> Cfg.automaton option
 val annots : t -> bool
 val doomed : t -> WpPropId.prop_id Bag.t
 val calls : t -> Kernel_function.Set.t