Merge branch 'fix/blanchard/wp/ref-usage-lemmas' into 'master'

Assure that aliases in lemmas are taken in account by RefUsage

Closes #931

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

src/plugins/wp/LogicUsage.ml

@@ -501,6 +501,11 @@ let iter_lemmas f =
   let d = Database.get () in
   SMap.iter (fun _name (lem,_) -> f lem) d.lemmas
 
+let fold_lemmas f =
+  compute () ;
+  let d = Database.get () in
+  SMap.fold (fun _name (lem,_) -> f lem) d.lemmas
+
 let logic_lemma l = fst (get_lemma l)
 
 let section_of_lemma l = snd (get_lemma l)

src/plugins/wp/LogicUsage.mli

@@ -60,6 +60,7 @@ val compute : unit -> unit (** To force computation *)
 
 val ip_lemma : logic_lemma -> Property.t
 val iter_lemmas : (logic_lemma -> unit) -> unit
+val fold_lemmas : (logic_lemma -> 'a -> 'a) -> 'a -> 'a
 val logic_lemma : string -> logic_lemma
 val axiomatic : string -> axiomatic
 val section_of_lemma : string -> logic_section

src/plugins/wp/RefUsage.ml

@@ -79,7 +79,7 @@ sig
   val cup : t -> t -> t
   val cup_differ : t -> t -> t * bool
   (* val leq : t -> t -> bool *) (* unused for now *)
-  (* val lcup : t list -> t *) (* unused for now *)
+  val lcup : t list -> t
   val fcup : ('a -> t) -> 'a list -> t
   val get : varinfo -> t -> access
   val access : varinfo -> access -> t -> t
@@ -120,7 +120,7 @@ struct
   (* let leq = Xmap.subset (fun _ -> Access.leq) *)
 
   (* unused for now *)
-  (* let rec lcup = function [] -> bot |[x] -> x |x::xs -> cup x (lcup xs)*)
+  let rec lcup = function [] -> bot |[x] -> x |x::xs -> cup x (lcup xs)
   let rec fcup f = function
       [] -> bot | [x] -> f x | x::xs -> cup (f x) (fcup f xs)
 
@@ -731,6 +731,11 @@ let compute_usage () =
   Wp_parameters.feedback ~ontty:`Transient "Collecting variable usage" ;
   (* initial state from variable initializers *)
   let u_init = Globals.Vars.fold cvarinit E.bot in
+  (* Usage in lemmas *)
+  let u_lemmas =
+    LogicUsage.fold_lemmas
+      (fun l -> E.cup (pred (mk_ctx()) l.lem_property)) E.bot
+  in
   (* initial state by kf *)
   let usage = Globals.Functions.fold (fun kf env ->
       KFmap.insert (fun _ _u _old -> assert false) kf (cfun kf) env)
@@ -790,10 +795,12 @@ let compute_usage () =
       ignore (KFmap.interf (kf_fp state_fp) callers todo);
       fixpoint state_fp.todo
   in fixpoint todo ;
+  let u_init = E.cup u_init u_lemmas in
   (* TODO[LC]: prendre en compte la compilation des fonctions logiques et predicats ; Cf. add_lphi *)
   let usage =
     KFmap.map
-      (fun ctx -> E.cup (E.cup ctx.code ctx.spec_globals) ctx.spec_formals)
+      (fun ctx ->
+         E.lcup [ u_lemmas ; ctx.code ; ctx.spec_globals ; ctx.spec_formals])
       usage
   in u_init, usage
 

src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_usage/ref-usage-lemmas.i (no preprocessing)
+[wp] Running WP plugin...
+.................................................
+... Ref Usage
+.................................................
+Init: { &a b }
+Function foo: { &a b *x }
+Function main: { &a b __retres }
+.................................................
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Pre-condition (file tests/wp_usage/ref-usage-lemmas.i, line 30) in 'main':
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i

+/* run.config
+  OPT: -wp-msg-key refusage
+*/
+/* run.config_qualif
+  DONTRUN:
+*/
+
+int a ;
+int b ;
+
+/*@ axiomatic A{
+    logic int* get reads \nothing ;
+    logic int* get_h = &a ;
+
+    axiom a: get_h == get ;
+    }
+
+*/
+
+/*@ axiomatic B{
+  logic integer value reads \nothing ;
+  axiom b: value == b ;
+  }
+*/
+
+void foo(int* x){
+  *x = a = b ;
+}
+
+/*@ requires a <= b ; */
+int main(void){
+  int e ;
+  foo(&e) ;
+}