propagate labels on functions

src/programs/pgm_wp.ml

@@ -691,7 +691,9 @@ let rec remove_at f = match f.t_node with
 let add_wp_decl ps f uc =
   let name = ps.ps_pure.ls_name in
   let s = "WP_" ^ name.id_string in
-  let label = ["expl:" ^ name.id_string] in
+  let label = 
+    ("expl:" ^ name.id_string) :: ps.ps_pure.ls_name.id_label
+  in
   let id = id_fresh ~label ?loc:name.id_loc s in
   let f = bool_to_prop uc (remove_at f) in
   let km = get_known (pure_uc uc) in

tests/my_cosine.mlw

@@ -36,7 +36,7 @@ lemma method_error
     forall x:real.
     abs x  <=. 0x1p-5 -> abs (1.0 -. x*.x*.0.5 -. cos x) <=. 0x1p-24
 
-let my_cosine "Safety of function my_cosine" #"my_cosine.c" 8 0 153#
+let my_cosine "expl:Safety of function my_cosine" #"my_cosine.c" 8 0 153#
     (x:single) : single =
 { abs (value x) <=. 0x1p-5 }
   assert {