From b70a8d35cc6dd7a9549a9e4585a39f8947d00834 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Sep 2020 09:53:25 +0200
Subject: [PATCH] [printer] printer for generalized check
---
.../ast_printing/cil_printer.ml | 18 +++++++++++++-----
1 file changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 14bab523bb3..7a15dce6488 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2835,13 +2835,17 @@ class cil_printer () = object (self)
method decreases fmt v = self#decrement "decreases" fmt v
method variant fmt v = self#decrement "loop variant" fmt v
+ method private pp_only_check fmt p =
+ if p.tp_only_check then fprintf fmt "%a " self#pp_acsl_keyword "check"
+
method assumes fmt p =
fprintf fmt "@[<hov 2>%a@ %a;@]"
self#pp_acsl_keyword "assumes"
self#identified_predicate p
method requires fmt p =
- fprintf fmt "@[<hov 2>%a@ %a;@]"
+ fprintf fmt "@[<hov 2>%a%a@ %a;@]"
+ self#pp_only_check p.ip_content
self#pp_acsl_keyword "requires"
self#identified_predicate p
@@ -2853,7 +2857,8 @@ class cil_printer () = object (self)
method post_cond fmt (k,p) =
let kw = get_termination_kind_name k in
- fprintf fmt "@[<hov 2>%a@ %a;@]"
+ fprintf fmt "@[<hov 2>%a%a@ %a;@]"
+ self#pp_only_check p.ip_content
self#pp_acsl_keyword kw
self#identified_predicate p
@@ -3091,13 +3096,15 @@ class cil_printer () = object (self)
pp_for_behavs behav
(self#allocation ~isloop:true) af
| AInvariant(behav,true, i) ->
- fprintf fmt "@[<2>%a%a@ %a;@]"
+ fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
+ self#pp_only_check i
self#pp_acsl_keyword "loop invariant"
self#predicate i.tp_statement
| AInvariant(behav,false,i) ->
- fprintf fmt "@[<2>%a%a@ %a;@]"
+ fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
+ self#pp_only_check i
self#pp_acsl_keyword "invariant"
self#predicate i.tp_statement
| AVariant v ->
@@ -3189,7 +3196,8 @@ class cil_printer () = object (self)
| Dlemma(name, is_axiom, labels, tvars, pred, _attr, _) ->
(* attributes are meant to be purely internal for now. *)
let old_lab = current_label in
- fprintf fmt "@[<hv 2>@[<hov 1>%a %a%a%a:@]@ %t%a;@]@\n"
+ fprintf fmt "@[<hv 2>@[<hov 1>%a%a %a%a%a:@]@ %t%a;@]@\n"
+ self#pp_only_check pred
self#pp_acsl_keyword (if is_axiom then "axiom" else "lemma")
self#varname name
self#labels labels
--
GitLab