[Logic] add attributes to identified_axiomatics

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) ->

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 = {