aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cutil.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-20 14:45:56 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-20 14:45:56 +0200
commited6043fe910f7a320f7af6d3f9d35f39f5cf7ee1 (patch)
tree3fab134f5444f0472a1ff8c06e5b7686a40648dc /cparser/Cutil.mli
parent4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (diff)
parent8a95c3e07fd02eaa87f8cca447bc7d7c2642eb22 (diff)
downloadcompcert-ed6043fe910f7a320f7af6d3f9d35f39f5cf7ee1.tar.gz
compcert-ed6043fe910f7a320f7af6d3f9d35f39f5cf7ee1.zip
Merge remote-tracking branch 'origin/master' into named-externals
Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml
Diffstat (limited to 'cparser/Cutil.mli')
-rw-r--r--cparser/Cutil.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index ef1266d5..8b6c609b 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -56,6 +56,10 @@ val attr_is_type_related: attribute -> bool
(* Is an attribute type-related (true) or variable-related (false)? *)
val attr_inherited_by_members: attribute -> bool
(* Is an attribute of a composite inherited by members of the composite? *)
+val strip_attributes_type: typ -> attribute list -> typ
+ (* Remove all attributes from the given type that are not contained in the list *)
+val strip_last_attribute: typ -> attribute option * typ
+ (* Remove the last top level attribute and return it *)
(* Type compatibility *)