From 4fe330e6f5a78dfc5908a38a9259c6bdab5094ad Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 1 Oct 2020 11:44:56 +0200
Subject: [PATCH] [Logic] add attributes to identified_axiomatics
---
src/kernel_services/ast_data/property.ml | 12 +++++++-----
src/kernel_services/ast_data/property.mli | 3 ++-
2 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 18cc9a2e325..27ac25d6e97 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -119,7 +119,8 @@ type identified_extended = {
and identified_axiomatic = {
iax_name : string;
- iax_props : identified_property list
+ iax_props : identified_property list;
+ iax_attrs : attributes;
}
and identified_lemma = {
@@ -849,10 +850,11 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_toplevel_predicate il_pred
Cil_types_debug.pp_attributes il_attrs
Cil_types_debug.pp_location il_loc
- | IPAxiomatic {iax_name; iax_props} ->
- Format.fprintf fmt "IPAxiomatic(%a,%a)"
+ | IPAxiomatic {iax_name; iax_props; iax_attrs} ->
+ Format.fprintf fmt "IPAxiomatic(%a,%a,%a)"
Cil_types_debug.pp_string iax_name
(Cil_types_debug.pp_list pretty_debug) iax_props
+ Cil_types_debug.pp_attributes iax_attrs
| IPLemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} ->
Format.fprintf fmt "IPLemma(%a,%a,%a,%a,%a,%a)"
Cil_types_debug.pp_string il_name
@@ -1549,9 +1551,9 @@ let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
let ip_of_global_annotation a =
let once = true in
let rec aux acc = function
- | Daxiomatic(iax_name, l, _, _) ->
+ | Daxiomatic(iax_name, l, iax_attrs, _) ->
let iax_props = List.fold_left aux [] l in
- IPAxiomatic {iax_name; iax_props} :: (iax_props @ acc)
+ IPAxiomatic {iax_name; iax_props; iax_attrs} :: (iax_props @ acc)
| Dlemma(il_name, true, il_labels, il_args, il_pred, il_attrs, il_loc) ->
ip_axiom {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} :: acc
| Dlemma(il_name, false, il_labels, il_args, il_pred, il_attrs, il_loc) ->
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index a5eeab81769..6ad7e28371f 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -149,7 +149,8 @@ type identified_extended = {
and identified_axiomatic = {
iax_name : string;
- iax_props : identified_property list
+ iax_props : identified_property list;
+ iax_attrs : attributes;
}
and identified_lemma = {
--
GitLab