From fe0c10a84916ee55ed09d4b5d598c95c7b26d7ef Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Thu, 28 Oct 2021 15:45:30 +0200
Subject: [PATCH] [deduction] Emit clearer model files
---
meta_deduce.ml | 14 ++++++++++----
1 file changed, 10 insertions(+), 4 deletions(-)
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 0d2e831..ac19952 100644
--- a/meta_deduce.ml
+++ b/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
--
GitLab