From 015036a091f80e54152a27dc43cc80d23a5c6403 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 9 Mar 2021 15:57:52 +0100
Subject: [PATCH] Types variant 'for' option
---
src/kernel_services/ast_data/cil_types.mli | 2 +-
src/kernel_services/ast_data/property.ml | 2 +-
src/kernel_services/ast_printing/cil_printer.ml | 7 +++----
src/kernel_services/ast_printing/cil_types_debug.ml | 2 +-
src/kernel_services/ast_queries/logic_typing.ml | 6 +++++-
5 files changed, 11 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index eb920a51c90..0c6f4675096 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1620,7 +1620,7 @@ and predicate = {
}
(** variant of a loop or a recursive function. *)
-and variant = term * string option
+and variant = term * logic_info option
(** allocates and frees.
@since Oxygen-20120901 *)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 506bb221ee1..6d6d06b8b3a 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1121,7 +1121,7 @@ struct
else b.b_name ^ "_"
let variant_suffix = function
- | (_,Some s) -> s
+ | (_,Some s) -> s.l_var_info.lv_name
| _ -> ""
let string_of_termination_kind = function
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 10e359d4b91..a98a8021d4d 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2862,13 +2862,12 @@ class cil_printer () = object (self)
method private decrement kw fmt (t, rel) = match rel with
| None -> fprintf fmt "@[<2>%a@ %a;@]" self#pp_acsl_keyword kw self#term t
- | Some str ->
- (*TODO: replace this string with an interpreted variable*)
- fprintf fmt "@[<2>%a@ %a@ %a@ %s;@]"
+ | Some li ->
+ fprintf fmt "@[<2>%a@ %a@ %a@ %a;@]"
self#pp_acsl_keyword kw
self#term t
self#pp_acsl_keyword "for"
- str
+ self#logic_info li
method decreases fmt v = self#decrement "decreases" fmt v
method variant fmt v = self#decrement "loop variant" fmt v
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 60f93f7bb1b..d180c0eb9b1 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -1037,7 +1037,7 @@ and pp_global_annotation fmt = function
and pp_custom_tree fmt _custom_tree = Format.fprintf fmt "CustomDummy"
-and pp_variant fmt = pp_pair pp_term (pp_option pp_string) fmt
+and pp_variant fmt = pp_pair pp_term (pp_option pp_logic_info) fmt
let pp_kinstr fmt = function
| Kstmt(stmt) -> Format.fprintf fmt "Kstmt(%a)" pp_stmt stmt
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 177bb48546c..a1b0106a435 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3541,7 +3541,11 @@ struct
let type_variant env = function
| (t, None) -> (type_int_term (base_ctxt env) env t, None)
- | (t, r) -> (term env t, r)
+ | (t, Some r) ->
+ let loc = t.lexpr_loc in
+ let t = term env t in
+ let li, _, _, _ = type_logic_app env loc r [] [t; t] in
+ (t, Some li)
let id_predicate env pred = Logic_const.new_predicate (predicate env pred)
--
GitLab