[deduction] Emit clearer model files

meta_deduce.ml

@@ -234,8 +234,8 @@ let pp_property preds globals mp =
 
 let generate_mp prefix preds globals fmt (mp, tset) =
     let print, preds = pp_property preds globals mp in
-    Format.fprintf fmt "meta_%s(\"%s\", %a, {%a}). %% %s@."
-    prefix
+    Format.fprintf fmt "%% Export of HILARE %s@.meta_%s(\"%s\", %a, {%a}).@."
+    mp.mp_name prefix
     (match mp.mp_context with
         | Weak_invariant -> "Weak invariant"
         | Strong_invariant -> "Strong invariant"
@@ -247,8 +247,7 @@ let generate_mp prefix preds globals fmt (mp, tset) =
         | Calling -> "Calling"
     )
     print ()
-    (print_set pp_ta) tset
-    mp.mp_name;
+    (print_set pp_ta) tset;
     preds
 
 let all_preds = ref None
@@ -297,12 +296,19 @@ let deduce flags mp ip mps =
   in
 
   Format.fprintf fmt {|
+%% This file is automatically generated by MetAcsl.
+%% It is provided as an input to run.pl in order to attempt HILARE deduction.
+
+%% == Export of the list of functions ==
 targets({%a}).
 
+%% == Export of the call graph's edges ==
 %a
 
+%% == Export already established HILAREs ==
 %a
 
+%% This is the HILARE we want to prove
 go :- %a
 |}
     (print_setlist pp_ta) targets