From 7e039e7b042e48aafb05558df48017fb96a175b8 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 30 Jan 2025 16:22:37 +0100
Subject: [PATCH] [Cil] Remove attribute annotation (Cil.AttrAnnot)
---
src/kernel_internals/parsing/clexer.mll | 1 -
src/kernel_internals/parsing/cparser.mly | 9 -
src/kernel_internals/parsing/logic_lexer.mll | 2 +-
src/kernel_internals/parsing/logic_parser.mly | 17 +-
src/kernel_internals/typing/cabs2cil.ml | 103 ++++------
src/kernel_internals/typing/ghost_cfg.ml | 2 +-
src/kernel_internals/typing/mergecil.ml | 2 +-
src/kernel_internals/typing/rmtmps.ml | 8 +-
.../typing/translate_lightweight.ml | 13 +-
.../ast_building/cil_builder.ml | 8 +-
src/kernel_services/ast_data/cil_types.ml | 16 +-
.../ast_printing/cabs_debug.ml | 1 -
.../ast_printing/cil_printer.ml | 194 ++++++++----------
.../ast_printing/cil_types_debug.ml | 6 +-
src/kernel_services/ast_printing/cprint.ml | 1 -
.../ast_printing/printer_tag.ml | 4 +-
.../ast_queries/ast_attributes.ml | 35 ++--
.../ast_queries/ast_attributes.mli | 6 +-
src/kernel_services/ast_queries/cil.ml | 36 ++--
.../ast_queries/cil_builtins.ml | 2 +-
src/kernel_services/ast_queries/cil_const.ml | 4 +-
.../ast_queries/cil_datatype.ml | 19 +-
src/kernel_services/ast_queries/file.ml | 4 +-
.../ast_queries/logic_const.ml | 2 +-
.../ast_queries/logic_utils.ml | 10 +-
.../ast_transformations/inline.ml | 2 +-
src/kernel_services/parsetree/cabs.ml | 3 +-
src/kernel_services/parsetree/cabshelper.ml | 2 -
src/kernel_services/parsetree/cabshelper.mli | 5 -
src/kernel_services/parsetree/logic_ptree.ml | 1 -
src/plugins/aorai/aorai_utils.ml | 4 +-
.../e-acsl/doc/refman/speclang_modern.tex | 8 -
.../src/project_initializer/prepare_ast.ml | 8 +-
src/plugins/eva/domains/cvalue/cvalue_init.ml | 2 +-
src/plugins/instantiate/basic_blocks.ml | 2 +-
src/plugins/obfuscator/obfuscate.ml | 7 +-
src/plugins/variadic/generic.ml | 2 +-
src/plugins/wp/RefUsage.ml | 5 +-
src/plugins/wp/doc/manual/nullable.c | 3 +-
src/plugins/wp/tests/wp_plugin/nullable.i | 8 +-
.../wp_plugin/oracle/nullable.res.oracle | 9 +-
.../oracle/nullable_ext.0.res.oracle | 9 +-
.../oracle_qualif/nullable.res.oracle | 9 +-
.../oracle_qualif/nullable_ext.res.oracle | 9 +-
tests/spec/ghost_attribute.i | 41 +++-
tests/spec/ghost_attribute.ml | 1 +
tests/spec/oracle/ghost_attribute.res.oracle | 53 ++++-
tests/spec/oracle/parsing.res.oracle | 2 +-
.../ghost_cv_parsing_errors.2.res.oracle | 12 +-
49 files changed, 350 insertions(+), 362 deletions(-)
create mode 100644 tests/spec/ghost_attribute.ml
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 6acfc8312b2..52c2a35484c 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -423,7 +423,6 @@ let make_annot ~one_line default lexbuf s =
parsing of the annotation will only occur in the cparser.mly rule. *)
| Logic_ptree.Acode_annot (loc,a) -> CODE_ANNOT (a, loc)
| Logic_ptree.Aloop_annot (loc,a) -> LOOP_ANNOT (a,loc)
- | Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc)
(* Initialize the pointer in Errormsg *)
let () =
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index fe028dcc3e2..6e356eb8f31 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -328,7 +328,6 @@ let type_to_expr_for_builtin ~loc ~builtin specifier decl_type =
%token <Logic_ptree.decl list> DECL
%token <Logic_ptree.code_annot * Cabs.cabsloc> CODE_ANNOT
%token <Logic_ptree.code_annot list * Cabs.cabsloc> LOOP_ANNOT
-%token <string * Cabs.cabsloc> ATTRIBUTE_ANNOT
%token <string> IDENT
%token <int64 list * Cabs.cabsloc> CST_CHAR
@@ -1574,13 +1573,6 @@ cvspec:
| VOLATILE { SpecCV(CV_VOLATILE), $1 }
| RESTRICT { SpecCV(CV_RESTRICT), $1 }
| GHOST { SpecCV(CV_GHOST), $1 }
-| ATTRIBUTE_ANNOT {
- let annot, loc = $1 in
- if String.compare annot "\\ghost" = 0 then begin
- Errorloc.parse_error ~loc "Use of \\ghost out of ghost code"
- end else
- SpecCV(CV_ATTRIBUTE_ANNOT annot), loc
- }
;
/*** GCC attributes ***/
@@ -1625,7 +1617,6 @@ attribute:
| RESTRICT { ("restrict",[]), $1 }
| VOLATILE { ("volatile",[]), $1 }
| GHOST { ("ghost",[]), $1 }
-| ATTRIBUTE_ANNOT { let annot, loc = $1 in (mk_attr_annot annot), loc }
;
/* (* sm: I need something that just includes __attribute__ and nothing more,
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 0f3b3b978c7..38197f98163 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -250,7 +250,7 @@
"\\freeable", FREEABLE;
"\\fresh", FRESH;
"\\from", FROM;
- "\\ghost", BSGHOST;
+ "\\ghost", GHOST;
"\\initialized", INITIALIZED;
"\\dangling", DANGLING;
"\\in", IN;
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 9926373fa56..05d22f6ddad 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -254,9 +254,9 @@
let str = Str.global_replace regex1 "\\1\\\\3" str in
Str.global_replace regex2 "\\1\\\\" str
- let cv_const = Attr ("const", [])
- let cv_volatile = Attr ("volatile", [])
- let cv_ghost = Attr("ghost", [])
+ let cv_const = ("const", [])
+ let cv_volatile = ("volatile", [])
+ let cv_ghost = ("ghost", [])
let toplevel_pred tp_kind tp_statement = { tp_kind; tp_statement }
@@ -312,7 +312,7 @@
%token VOLATILE READS WRITES
%token LOGIC PREDICATE INDUCTIVE AXIOM LEMMA LBRACE RBRACE
%token AXIOMATIC MODULE IMPORT
-%token GHOST MODEL CASE
+%token MODEL CASE
%token VOID CHAR SIGNED UNSIGNED SHORT LONG DOUBLE STRUCT ENUM UNION
%token BSUNION INTER
%token TYPE BEHAVIOR BEHAVIORS ASSUMES COMPLETE DISJOINT
@@ -320,7 +320,7 @@
%token BIFF BIMPLIES STARHAT HAT HATHAT PIPE TILDE GTGT LTLT
%token SIZEOF LAMBDA LET
%token TYPEOF BSTYPE
-%token WITH CONST BSGHOST
+%token WITH CONST GHOST
%token INITIALIZED DANGLING
%token LSQUAREPIPE RSQUAREPIPE
%token IN
@@ -787,7 +787,7 @@ logic_type: logic_type_gen(typesymbol) { $1 }
cv:
CONST { cv_const }
| VOLATILE { cv_volatile }
-| BSGHOST { cv_ghost }
+| GHOST { cv_ghost }
;
type_spec_cv:
@@ -1386,8 +1386,6 @@ annotation:
(Not_well_formed (loc $sloc,
"Only one code annotation is allowed per comment"))
}
-| identifier { Aattribute_annot (loc $sloc, $1) }
-| BSGHOST { Aattribute_annot(loc $sloc,"\\ghost") }
| unknown_extension SEMICOLON { raise Unknown_ext }
;
@@ -2080,7 +2078,7 @@ bs_keyword:
| AS { () }
| BASE_ADDR { () }
| BLOCK_LENGTH { () }
-| BSGHOST { () }
+| GHOST { () }
| DYNAMIC { () }
| EMPTY { () }
| FALSE { () }
@@ -2139,7 +2137,6 @@ wildcard:
| EQUAL { () }
| EXISTS { () }
| GE { () }
-| GHOST { () }
| GT { () }
| GTGT { () }
| HAT { () }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 732978be941..fcb9b07f95b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -98,15 +98,6 @@ let () =
(fun a -> Ast_attributes.register_attribute a AttrIgnored)
erased_attributes
-(* JS: return [Some s] if the attribute string is the attribute annotation [s]
- and [None] if it is not an annotation. *)
-let attrAnnot s =
- let r = Str.regexp "~attrannot:\\(.+\\)" in
- if Str.string_match r s 0 then
- try Some (Str.matched_group 1 s) with Not_found -> assert false
- else
- None
-
let stripUnderscore s =
if String.length s = 1 then begin
if s = "_" then
@@ -119,11 +110,6 @@ let stripUnderscore s =
if List.mem res unsupported_attributes then
Kernel.error ~current:true "unsupported attribute: %s" s
else begin
- match attrAnnot res with
- | Some _ ->
- (* Attribute annotation are always considered known *)
- ()
- | None ->
if not (Ast_attributes.is_known_attribute res) then
Kernel.warning
~once:true ~current:true ~wkey:Kernel.wkey_unknown_attribute
@@ -391,7 +377,7 @@ let get_current_stdheader () =
*)
let (>>?) opt f =
match opt with
- | Some (Attr(name, args)) -> f name args
+ | Some (name, args) -> f name args
| _ -> opt
let process_stdlib_pragma name args =
@@ -403,8 +389,8 @@ let process_stdlib_pragma name args =
let relative_name = Filepath.relativize ~base_name s in
push_stdheader relative_name;
None
- | _ -> Some (Attr(name, args))
- end else Some (Attr(name, args))
+ | _ -> Some (name, args)
+ end else Some (name, args)
let fc_stdlib_attribute attrs =
let open Ast_attributes in
@@ -417,7 +403,7 @@ let fc_stdlib_attribute attrs =
drop_attribute fc_stdlib attrs
end else [AStr s], attrs
in
- add_attribute (Attr (fc_stdlib, payload)) attrs
+ add_attribute (fc_stdlib, payload) attrs
end
(* ICC align/noalign pragmas (not supported by GCC/MSVC with this syntax).
Implemented by translating them to 'aligned' attributes. Currently,
@@ -512,7 +498,7 @@ let process_pack_pragma name args =
"packing pragma: setting alignment to %a" Integer.pretty n;
current_packing_pragma := new_pragma; None
end else
- Some (Attr (name, args))
+ Some (name, args)
| [ACons ("push",[])] (* #pragma pack(push) *) ->
Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
"packing pragma: pushing alignment %t" pretty_current_packing_pragma;
@@ -526,7 +512,7 @@ let process_pack_pragma name args =
Stack.push !current_packing_pragma packing_pragma_stack;
current_packing_pragma:= new_pragma; None
end else
- Some (Attr (name, args))
+ Some (name, args)
| ACons ("push",[]) :: args (* unknown push directive *) ->
Kernel.warning ~current:true
"Unsupported argument for pragma pack push directive: `%a'."
@@ -554,20 +540,20 @@ let process_pack_pragma name args =
None
end
| [ACons ("show",[])] (* #pragma pack(show) *) ->
- Some (Attr (name, args))
+ Some (name, args)
| _ ->
Kernel.warning ~current:true
"Unsupported packing pragma not honored by Frama-C: #pragma pack(%a)"
(Pretty_utils.pp_list ~sep:", " ~empty:"<empty>"
Cil_printer.pp_attrparam) args;
- Some (Attr (name, args))
+ Some (name, args)
end
- | _ -> Some (Attr (name, args))
+ | _ -> Some (name, args)
end
let force_packed_attribute a =
if Ast_attributes.has_attribute "packed" a then a
- else Ast_attributes.add_attribute (Attr("packed",[])) a
+ else Ast_attributes.add_attribute ("packed",[]) a
let is_power_of_two i = i > 0 && i land (i-1) = 0
@@ -591,7 +577,7 @@ let eval_aligned_attrparams aps =
let warn_invalid_align_attribute aps =
Kernel.warning ~current:true ~once:true
"ignoring invalid aligned attribute: %a"
- Cil_printer.pp_attribute (Attr("aligned", aps))
+ Cil_printer.pp_attribute ("aligned", aps)
(* If there is more than one 'aligned' attribute, GCC's behavior is to
consider the maximum among them. This function computes this value
@@ -602,7 +588,7 @@ let combine_aligned_attributes attrs =
| aligned_attrs ->
List.fold_left (fun acc attr ->
match attr with
- | Attr("aligned", aps) ->
+ | ("aligned", aps) ->
begin
let align = eval_aligned_attrparams aps in
if align = None then begin
@@ -614,6 +600,7 @@ let combine_aligned_attributes attrs =
| Some old_n, Some new_n -> Some (Integer.max old_n new_n)
end
| _ -> assert false (* attributes were previously filtered by name *)
+
) None aligned_attrs
let warn_incompatible_pragmas_attributes apragma has_attrs =
@@ -630,7 +617,7 @@ let warn_incompatible_pragmas_attributes apragma has_attrs =
let check_aligned attrs =
List.fold_right (fun attr acc ->
match attr with
- | Attr("aligned", aps) ->
+ | ("aligned", aps) ->
if eval_aligned_attrparams aps = None then
(warn_invalid_align_attribute aps; acc)
else attr :: acc
@@ -661,7 +648,7 @@ let process_pragmas_pack_align_comp_attributes loc ci cattrs =
Kernel.feedback ~source ~dkey:Kernel.dkey_typing_pragma
"adding aligned(%a) attribute to comp '%s' due to packing pragma"
Integer.pretty n ci.cname;
- add_attribute (Attr("aligned",[AInt n])) (drop_attribute "aligned" cattrs)
+ add_attribute ("aligned",[AInt n]) (drop_attribute "aligned" cattrs)
end
| Some local ->
(* The largest aligned wins with GCC. Don't know
@@ -670,7 +657,7 @@ let process_pragmas_pack_align_comp_attributes loc ci cattrs =
Kernel.feedback ~source ~dkey:Kernel.dkey_typing_pragma
"setting aligned(%a) attribute to comp '%s' due to packing pragma"
Integer.pretty align ci.cname;
- add_attribute (Attr("aligned",[AInt align]))
+ add_attribute ("aligned",[AInt align])
(drop_attribute "aligned" cattrs)
in
force_packed_attribute with_aligned_attributes
@@ -679,7 +666,7 @@ let process_pragmas_pack_align_comp_attributes loc ci cattrs =
| None, Some false ->
force_packed_attribute
(add_attribute
- (Attr("aligned",[AInt Integer.one]))
+ (("aligned",[AInt Integer.one]))
(drop_attribute "aligned" cattrs))
(* Takes into account the possible effect of '#pragma pack' directives on
@@ -721,13 +708,13 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
"%s aligned(%a) attribute to field '%s.%s' due to packing pragma"
(if Option.is_none field_align then "adding" else "setting")
Integer.pretty new_align fi.fcomp.cname fi.fname;
- let new_attr = Attr ("aligned", [AInt new_align]) in
+ let new_attr = ("aligned", [AInt new_align]) in
add_attribute new_attr (drop_attribute "aligned" fattrs)
| None, Some true ->
drop_attribute "aligned" fattrs
| None, Some false ->
(add_attribute
- (Attr("aligned",[AInt Integer.one]))
+ ("aligned",[AInt Integer.one])
(drop_attribute "aligned" fattrs))
@@ -2576,7 +2563,7 @@ let rec clean_up_cond_locals =
let cabsAddAttributes al0 (al: attributes) : attributes =
if al0 == [] then al else
List.fold_left
- (fun acc (Attr(an, _) | AttrAnnot an as a) ->
+ (fun acc ((an, _) as a) ->
(* See if the attribute is already in there *)
match Ast_attributes.filter_attributes an acc with
| [] -> Ast_attributes.add_attribute a acc (* Nothing with that name *)
@@ -2627,7 +2614,7 @@ let rec cabsTypeCombineAttributes what a0 t =
List.fold_left
(fun (ik', a0') a0one ->
match a0one with
- | Attr("mode", [ACons(mode,[])]) -> begin
+ | ("mode", [ACons(mode,[])]) -> begin
(* (trace "gccwidth" (dprintf "I see mode %s applied to an int type\n"
mode )); *)
(* the cases below encode the 32-bit assumption.. *)
@@ -2880,7 +2867,7 @@ let setupBuiltin ?(force_keep=false) name ?spec (resTyp, args_or_argtypes, isva)
cabsPushGlobal (GFunDecl (funspec, v, Cil_builtins.builtinLoc));
Cil.unsafeSetFormalsDecl v args;
if force_keep then
- v.vattr <- Ast_attributes.add_attribute (Attr ("FC_BUILTIN",[])) v.vattr;
+ v.vattr <- Ast_attributes.add_attribute ("FC_BUILTIN",[]) v.vattr;
v
(* builtin is never ghost *)
@@ -3931,7 +3918,7 @@ let append_chunk_to_annot ~ghost annot_chunk current_chunk =
let locals = b.blocals in
b.blocals <- [];
b.battrs <-
- Ast_attributes.add_attributes [Attr(frama_c_keep_block,[])] b.battrs;
+ Ast_attributes.add_attributes [(frama_c_keep_block,[])] b.battrs;
let block = mkStmt ~ghost ~valid_sid (Block b) in
let chunk = s2c block in
let chunk = { chunk with cases = current_chunk.cases } in
@@ -4498,7 +4485,6 @@ and convertCVtoAttr (src: Cabs.cvspec list) : Cabs.attribute list =
| CV_CONST :: tl -> ("const",[]) :: (convertCVtoAttr tl)
| CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
| CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
- | CV_ATTRIBUTE_ANNOT a :: tl -> (Cabshelper.mk_attr_annot a) :: convertCVtoAttr tl
| CV_GHOST :: tl -> ("ghost",[]) :: (convertCVtoAttr tl)
and makeVarInfoCabs
@@ -4579,9 +4565,6 @@ and doAttr ghost (a: Cabs.attribute) : attribute list =
(* Strip the leading and trailing underscore *)
match a with
| ("__attribute__", []) -> [] (* An empty list of gcc attributes *)
- | (s, []) ->
- let s = stripUnderscore s in
- [ match attrAnnot s with None -> Attr(s, []) | Some s -> AttrAnnot s ]
| (s, el) ->
let rec attrOfExp (strip: bool)
@@ -4655,7 +4638,7 @@ and doAttr ghost (a: Cabs.attribute) : attribute list =
(* Sometimes we need to convert attrarg into attr *)
let arg2attrs = function
| ACons (s, _) when List.mem s erased_attributes -> []
- | ACons (s, args) -> [Attr (s, args)]
+ | ACons (s, args) -> [(s, args)]
| a ->
Kernel.fatal ~current:true
"Invalid form of attribute: %a"
@@ -4669,7 +4652,7 @@ and doAttr ghost (a: Cabs.attribute) : attribute list =
else if s = "__declspec" then
fold_attrs (attrOfExp false ~foldenum:false) el
else
- [Attr(stripUnderscore s, List.map (attrOfExp ~foldenum:false false) el)]
+ [(stripUnderscore s, List.map (attrOfExp ~foldenum:false false) el)]
and doAttributes (ghost:bool) (al: Cabs.attribute list) : attribute list =
List.fold_left (fun acc a -> cabsAddAttributes (doAttr ghost a) acc) [] al
@@ -4687,7 +4670,7 @@ and cabsPartitionAttributes
| a :: rest ->
let an, kind = match doAttr ghost a with
| [] -> "", default
- | (Attr(an, _) | AttrAnnot an)::_ ->
+ | (an, _)::_ ->
(* doAttr already strip underscores of the attribute if necessary so
we do not need to strip then before calling get_attribute_class
here. *)
@@ -4708,9 +4691,9 @@ and cabsPartitionAttributes
and doType (ghost:bool) (context: type_context)
(nameortype: Ast_attributes.attribute_class) (* This is AttrName if we are doing
- * the type for a name, or AttrType
- * if we are doing this type in a
- * typedef *)
+ * the type for a name, or AttrType
+ * if we are doing this type in a
+ * typedef *)
?(allowZeroSizeArrays=false)
?(allowVarSizeArrays=false)
(bt: typ) (* The base type *)
@@ -5005,13 +4988,13 @@ and doType (ghost:bool) (context: type_context)
| None -> []
| Some l -> begin
let static = if Ast_attributes.has_attribute "static" a then
- [Attr ("static",[])]
+ [("static",[])]
else []
in
(* Transform the length into an attribute expression *)
try
let la : attrparam = expToAttrParam l in
- Attr("arraylen", [ la ]) :: static
+ ("arraylen", [ la ]) :: static
with NotAnAttrParam _ -> begin
Kernel.warning ~once:true ~current:true
"Cannot represent the length '%a' of array as an attribute"
@@ -5055,7 +5038,7 @@ and doType (ghost:bool) (context: type_context)
let arg_type_from_vi vi =
let attrs =
if vi.vghost then
- cabsAddAttributes [Attr (Ast_attributes.frama_c_ghost_formal, [])] vi.vattr
+ cabsAddAttributes [(Ast_attributes.frama_c_ghost_formal, [])] vi.vattr
else
vi.vattr
in (vi.vname, vi.vtype, attrs)
@@ -5232,7 +5215,7 @@ and makeCompType loc ghost (isstruct: bool)
end;
let ftype =
typeAddAttributes
- [Attr (Ast_attributes.bitfield_attribute_name, [AInt (Integer.of_int s)])]
+ [(Ast_attributes.bitfield_attribute_name, [AInt (Integer.of_int s)])]
ftype
in
w, ftype
@@ -6501,7 +6484,7 @@ and doExp local_env
Kernel.debug ~dkey:Kernel.dkey_typing_global
"Calling function %s without prototype." n ;
let ftype =
- mk_tfun ~tattr:[Attr("missingproto",[])] intType None false
+ mk_tfun ~tattr:[("missingproto",[])] intType None false
in
(* Add a prototype to the environment *)
let proto, _ =
@@ -8913,7 +8896,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
in
checkArray inite vi;
vi.vname <- newname;
- let attrs = Ast_attributes.add_attribute (Attr (fc_local_static,[])) vi.vattr in
+ let attrs = Ast_attributes.add_attribute (fc_local_static,[]) vi.vattr in
vi.vattr <- fc_stdlib_attribute attrs;
(* However, we have a problem if a real global appears later with the
@@ -8981,7 +8964,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
if isvarsize then begin
let free = vla_free_fun () in
let destructor = AStr free.vname in
- let attr = Attr (frama_c_destructor, [destructor]) in
+ let attr = (frama_c_destructor, [destructor]) in
vi.vdefined <- true;
vi.vattr <- Ast_attributes.add_attribute attr vi.vattr;
end;
@@ -9208,7 +9191,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
| [] -> (* ordinary prototype. *)
ignore (createGlobal l local_env.is_ghost logic_spec spec_res name)
(* E.log "%s is not aliased\n" name *)
- | [Attr("alias", [AStr othername])] ->
+ | [("alias", [AStr othername])] ->
if not (isFunctionType vtype) || local_env.is_ghost then begin
Kernel.warning ~current:true
"%a: CIL only supports attribute((alias)) for C functions."
@@ -9257,7 +9240,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
| Cabs.PRAGMA (a, _) when isglobal -> begin
match doAttr local_env.is_ghost ("dummy", [a]) with
- | [Attr("dummy", [a'])] ->
+ | [("dummy", [a'])] ->
let a'' =
match a' with
| ACons (s, args) ->
@@ -9266,7 +9249,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
process_pack_pragma
| _ -> (* Cil.fatal "Unexpected attribute in #pragma" *)
Kernel.warning ~current:true "Unexpected attribute in #pragma";
- Some (Attr ("", [a']))
+ Some ( ("", [a']))
in
Option.iter
(fun a'' ->
@@ -10023,7 +10006,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.BLOCK (b, _, _) ->
let c = doBodyScope local_env b in
let b = c2block ~ghost c in
- b.battrs <- Ast_attributes.add_attributes [Attr(frama_c_keep_block,[])] b.battrs;
+ b.battrs <- Ast_attributes.add_attributes [(frama_c_keep_block,[])] b.battrs;
let res = s2c (mkStmt ~ghost ~valid_sid (Block b)) in
{ res with cases = c.cases }
@@ -10044,7 +10027,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let loc' = convLoc loc in
let break_cond = breakChunk ~ghost loc' in
exitLoop ();
- loopChunk ~ghost ~sattr:[Attr("while",[])] a
+ loopChunk ~ghost ~sattr:[("while",[])] a
((doCondition ~is_loop:true local_env CNoConst e skipChunk break_cond)
@@@ (s', ghost))
@@ -10079,7 +10062,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
CNoConst e skipChunk (breakChunk ~ghost loc'))
in
exitLoop ();
- loopChunk ~ghost ~sattr:[Attr("dowhile",[])] a (s' @@@ (s'', ghost))
+ loopChunk ~ghost ~sattr:[("dowhile",[])] a (s' @@@ (s'', ghost))
| Cabs.FOR(a,fc1,e2,e3,s,loc) -> begin
let loc' = convLoc loc in
@@ -10107,7 +10090,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| _ ->
doCondition ~is_loop:true local_env CNoConst e2 skipChunk break_cond @@@ (c, ghost)
in
- let res = se1 @@@ (loopChunk ~sattr:[Attr("for",[])] ~ghost a c, ghost) in
+ let res = se1 @@@ (loopChunk ~sattr:[("for",[])] ~ghost a c, ghost) in
exitScope ();
if has_decl then begin
let chunk = s2c (mkStmt ~ghost ~valid_sid (Block (c2block ~ghost res)))
diff --git a/src/kernel_internals/typing/ghost_cfg.ml b/src/kernel_internals/typing/ghost_cfg.ml
index 056b1d4cd2e..d361913ab25 100644
--- a/src/kernel_internals/typing/ghost_cfg.ml
+++ b/src/kernel_internals/typing/ghost_cfg.ml
@@ -61,7 +61,7 @@ let noGhostFD prj fd =
DoChildren
| _ ->
let o = self#original s in
- s.sattr <- if has_annot o then [AttrAnnot annot_attr] else [] ;
+ s.sattr <- if has_annot o then [(annot_attr, [])] else [] ;
DoChildren
end
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index c709f175d30..6cd7a38dcec 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -1657,7 +1657,7 @@ let oneFilePass1 (f:file) : unit =
end else attrprm
in
let attrs = Ast_attributes.drop_attribute "fc_stdlib" newrep.ndata.vattr in
- let attrs = Ast_attributes.add_attribute (Attr ("fc_stdlib", attrprm)) attrs in
+ let attrs = Ast_attributes.add_attribute ("fc_stdlib", attrprm) attrs in
newrep.ndata.vattr <- attrs;
end;
newrep.ndata.vdefined <- vi.vdefined || oldvi.vdefined;
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 8cd686cb7c7..47c4ed14280 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -132,7 +132,7 @@ let categorizePragmas ast =
in
function
- | GPragma (Attr ("cilnoremove" as directive, args), (location,_)) ->
+ | GPragma (("cilnoremove" as directive, args), (location,_)) ->
(* a very flexible pragma: can retain typedefs, enums,
* structs, unions, or globals (functions or variables) *)
begin
@@ -174,7 +174,7 @@ let categorizePragmas ast =
(* Look for alias attributes, e.g. Linux modules *)
match Ast_attributes.filter_attributes "alias" v.vattr with
| [] -> () (* ordinary prototype. *)
- | [ Attr("alias", [AStr othername]) ] ->
+ | [ ("alias", [AStr othername]) ] ->
Hashtbl.add keepers.defines othername ()
| _ ->
Kernel.fatal ~current:true
@@ -224,8 +224,8 @@ let isPragmaRoot keepers = function
*)
let hasExportingAttribute funvar =
let isExportingAttribute = function
- | Attr ("constructor", []) -> true
- | Attr ("destructor", []) -> true
+ | ("constructor", []) -> true
+ | ("destructor", []) -> true
| _ -> false
in
List.exists isExportingAttribute funvar.vattr
diff --git a/src/kernel_internals/typing/translate_lightweight.ml b/src/kernel_internals/typing/translate_lightweight.ml
index 61ab66aa212..4cf9e528784 100644
--- a/src/kernel_internals/typing/translate_lightweight.ml
+++ b/src/kernel_internals/typing/translate_lightweight.ml
@@ -69,15 +69,10 @@ class annotateFunFromDeclspec =
in
aux attrparam
in
- let recover_from_attribute params attr =
- match attr with
- | Attr(name,attrparams) ->
- begin
- try
- Some(name, List.map (recover_from_attr_param params) attrparams)
- with No_recovery -> None
- end
- | AttrAnnot _ -> None
+ let recover_from_attribute params (name,attrparams) =
+ try
+ Some(name, List.map (recover_from_attr_param params) attrparams)
+ with No_recovery -> None
in
(* Add precondition based on declspec on parameters *)
diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index abb8f391315..975d9c9e754 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -90,7 +90,7 @@ struct
let attribute (s, t) name params =
match t with
| Ctype t ->
- let tattr = Ast_attributes.add_attribute (Attr (name, params)) t.tattr in
+ let tattr = Ast_attributes.add_attribute (name, params) t.tattr in
s, Ctype { t with tattr }
| _ -> raise NotACType
@@ -835,7 +835,7 @@ struct
let if_ ?(ghost_else=false) cond ~then_ ~else_ =
let else_attributes =
if ghost_else
- then [Cil_types.Attr (Ast_attributes.frama_c_ghost_else,[])]
+ then [(Ast_attributes.frama_c_ghost_else,[])]
else []
in
`stmt (If (
@@ -1087,7 +1087,7 @@ struct
Cil_types.If (ifthen_exp, block, Cil.mkBlock [], b.loc)
| IfThenElse { ifthenelse_exp; then_block; ghost_else } ->
if ghost_else then
- block.battrs <- [Cil_types.Attr (Ast_attributes.frama_c_ghost_else,[])];
+ block.battrs <- [(Ast_attributes.frama_c_ghost_else,[])];
Cil_types.If (ifthenelse_exp, then_block, block, b.loc)
| Switch { switch_exp } ->
let open Cil_types in
@@ -1349,7 +1349,7 @@ struct
fundec.svar.vattr <- Ast_attributes.add_attribute attr fundec.svar.vattr
let add_new_attribute attr params =
- add_attribute (Cil_types.Attr (attr, params))
+ add_attribute (attr, params)
let add_stdlib_generated () =
add_new_attribute "fc_stdlib_generated" []
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index e2a0beaa036..f96eca54b1f 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -373,15 +373,13 @@ and typ_node =
(** {2 Attributes} *)
(* ************************************************************************* *)
-and attribute =
- | Attr of string * attrparam list
- (** An attribute has a name and some optional parameters. The name should not
- start or end with underscore. When CIL parses attribute names it will
- strip leading and ending underscores (to ensure that the multitude of GCC
- attributes such as const, __const and __const__ all mean the same
- thing.) *)
-
- | AttrAnnot of string
+(** An attribute has a name and some optional parameters. The name should not
+ start or end with underscore. When CIL parses attribute names it will
+ strip leading and ending underscores (to ensure that the multitude of GCC
+ attributes such as const, __const and __const__ all mean the same
+ thing.)
+*)
+and attribute = string * attrparam list
(** Attributes are lists sorted by the attribute name. Use the functions
{!Ast_attributes.add_attribute} and {!Ast_attributes.add_attributes} to
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index 3e533504d93..809ca3f3ae7 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -38,7 +38,6 @@ let pp_cvspec fmt = function
| CV_CONST -> fprintf fmt "CV_CONST"
| CV_VOLATILE -> fprintf fmt "CV_VOLATILE"
| CV_RESTRICT -> fprintf fmt "CV_RESTRICT"
- | CV_ATTRIBUTE_ANNOT s -> fprintf fmt "CV_ATTRIBUTE_ANNOT %s" s
| CV_GHOST -> fprintf fmt "CV_GHOST"
let pp_const fmt = function
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a1048dbd7e9..a7e3f50f3ca 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -122,10 +122,8 @@ let () = register_shallow_attribute Ast_attributes.frama_c_init_obj
let () = register_shallow_attribute Ast_attributes.frama_c_inlined
let () = register_shallow_attribute Ast_attributes.anonymous_attribute_name
-let keep_attr = function
- | Attr _ as a ->
- not (List.mem (Ast_attributes.attribute_name a) !reserved_attributes)
- | AttrAnnot _ -> true
+let keep_attr a =
+ not (List.mem (Ast_attributes.attribute_name a) !reserved_attributes)
let filter_printing_attributes l =
if Kernel.(is_debug_key_enabled dkey_print_attrs) then l
@@ -1856,7 +1854,7 @@ class cil_printer () = object (self)
self#line_directive fmt l;
fprintf fmt "__asm__(\"%s\");@\n" (Escape.escape_string s)
- | GPragma (Attr(an, args), l) ->
+ | GPragma ((an, args), l) ->
(* sm: suppress printing pragmas that gcc does not understand *)
(* assume anything starting with "ccured" is ours *)
(* also don't print the 'combiner' pragma *)
@@ -1888,11 +1886,6 @@ class cil_printer () = object (self)
end;
if suppress then fprintf fmt " */@\n" else fprintf fmt "@\n"
- | GPragma (AttrAnnot _, _) ->
- assert false
- (* self#line_directive fmt l;
- fprintf fmt "/* #pragma %s */@\n" a*)
-
| GAnnot (decl,l) ->
(* attributes are purely internal. *)
self#line_directive fmt l;
@@ -2084,11 +2077,11 @@ class cil_printer () = object (self)
let print_size_info fmt =
match size_info with
| [] -> printAttributes fmt a
- | [Attr("arraylen",[s])]->
+ | [("arraylen",[s])]->
Format.fprintf fmt "%a%t%a"
printAttributes atts_elem sep self#attrparam s
- | [Attr("static",[]); Attr("arraylen",[s])]
- | [Attr("arraylen", [s]); Attr("static", [])] ->
+ | [("static",[]); ("arraylen",[s])]
+ | [("arraylen", [s]); ("static", [])] ->
Format.fprintf fmt "static%a@ %a"
printAttributes atts_elem self#attrparam s
| _ -> ()
@@ -2179,101 +2172,92 @@ class cil_printer () = object (self)
(* Print one attribute. Return also an indication whether this attribute
should be printed inside the __attribute__ list *)
- method attribute fmt = function
- | Attr(an, args) ->
- (* Recognize and take care of some known cases *)
- (match an, args with
- | "const", [] -> self#pp_keyword fmt "const"; false
- (* Put the aconst inside the attribute list *)
- | "aconst", [] when not (Machine.msvcMode ()) -> fprintf fmt "__const__"; true
- | "thread", [ ACons ("c11",[]) ]
- when not state.print_cil_as_is ->
- fprintf fmt "_Thread_local"; false
- | "thread", [] when not (Machine.msvcMode ()) -> fprintf fmt "__thread"; false
- | "volatile", [] -> self#pp_keyword fmt "volatile"; false
- | "ghost", [] -> self#pp_keyword fmt "\\ghost"; false
- | "restrict", [] ->
- if Machine.msvcMode () then
- fprintf fmt "__restrict"
- else
- self#pp_keyword fmt "restrict";
- false
- | "missingproto", [] ->
- if self#display_comment () then fprintf fmt "/* missing proto */";
- false
- | "cdecl", [] when Machine.msvcMode () ->
- fprintf fmt "__cdecl"; false
- | "stdcall", [] when Machine.msvcMode () ->
- fprintf fmt "__stdcall"; false
- | "fastcall", [] when Machine.msvcMode () ->
- fprintf fmt "__fastcall"; false
- | "declspec", args when Machine.msvcMode () ->
- fprintf fmt "__declspec(%a)"
- (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
- false
- | "w64", [] when Machine.msvcMode () ->
- fprintf fmt "__w64"; false
- | "asm", args ->
- fprintf fmt "__asm__(%a)"
- (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
- false
- (* we suppress printing mode(__si__) because it triggers an
- internal compiler error in all current gcc versions
- sm: I've now encountered a problem with mode(__hi__)...
- I don't know what's going on, but let's try disabling all "mode". *)
- | "mode", [ACons(tag,[])] ->
- if self#display_comment () then fprintf fmt "/* mode(%s) */" tag;
- false
-
- (* sm: also suppress "format" because we seem to print it in
- a way gcc does not like *)
- | "format", _ ->
- if self#display_comment () then fprintf fmt "/* format attribute */";
- false
-
- | "hidden", _ -> (* hidden attribute list *)
- false
- (* sm: here's another one I don't want to see gcc warnings about.. *)
- | "mayPointToStack", _ when not state.print_cil_input ->
- (* [matth: may be inside another comment.]
- -> text "/*mayPointToStack*/", false *)
- false
-
- | "arraylen", [a] ->
- if self#display_comment () then fprintf fmt "/*[%a]*/" self#attrparam a;
- false
- | "static",_ ->
- if self#display_comment () then fprintf fmt "/* static */"; false
- | "", _ ->
- fprintf fmt "%a "
- (Pretty_utils.pp_list ~sep:" " self#attrparam) args;
- true
- | s, _ when
- s = Ast_attributes.bitfield_attribute_name &&
- not state.print_cil_as_is &&
- not (Kernel.is_debug_key_enabled Kernel.dkey_print_bitfields) ->
- false
- | _ -> (* This is the default case *)
- (* Add underscores to the name *)
- let an' =
- if Machine.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
- in
- (match args with
- | [] -> fprintf fmt "%s" an'
- | _ :: _ ->
- fprintf fmt "%s(%a)"
- an'
- (Pretty_utils.pp_list ~sep:"," self#attrparam) args);
- true)
- | AttrAnnot s ->
- let block = false in
- fprintf fmt "%t %s %t"
- (fun fmt -> self#pp_open_annotation ~block fmt)
- s
- (fun fmt -> self#pp_close_annotation ~block fmt);
+ method attribute fmt (an, args) =
+ (* Recognize and take care of some known cases *)
+ match an, args with
+ | "const", [] -> self#pp_keyword fmt "const"; false
+ (* Put the aconst inside the attribute list *)
+ | "aconst", [] when not (Machine.msvcMode ()) -> fprintf fmt "__const__"; true
+ | "thread", [ ACons ("c11",[]) ]
+ when not state.print_cil_as_is ->
+ fprintf fmt "_Thread_local"; false
+ | "thread", [] when not (Machine.msvcMode ()) -> fprintf fmt "__thread"; false
+ | "volatile", [] -> self#pp_keyword fmt "volatile"; false
+ | "ghost", [] -> self#pp_keyword fmt "\\ghost"; false
+ | "restrict", [] ->
+ if Machine.msvcMode () then
+ fprintf fmt "__restrict"
+ else
+ self#pp_keyword fmt "restrict";
+ false
+ | "missingproto", [] ->
+ if self#display_comment () then fprintf fmt "/* missing proto */";
+ false
+ | "cdecl", [] when Machine.msvcMode () ->
+ fprintf fmt "__cdecl"; false
+ | "stdcall", [] when Machine.msvcMode () ->
+ fprintf fmt "__stdcall"; false
+ | "fastcall", [] when Machine.msvcMode () ->
+ fprintf fmt "__fastcall"; false
+ | "declspec", args when Machine.msvcMode () ->
+ fprintf fmt "__declspec(%a)"
+ (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
+ false
+ | "w64", [] when Machine.msvcMode () ->
+ fprintf fmt "__w64"; false
+ | "asm", args ->
+ fprintf fmt "__asm__(%a)"
+ (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
+ false
+ (* we suppress printing mode(__si__) because it triggers an
+ internal compiler error in all current gcc versions
+ sm: I've now encountered a problem with mode(__hi__)...
+ I don't know what's going on, but let's try disabling all "mode". *)
+ | "mode", [ACons(tag,[])] ->
+ if self#display_comment () then fprintf fmt "/* mode(%s) */" tag;
+ false
+ (* sm: also suppress "format" because we seem to print it in
+ a way gcc does not like *)
+ | "format", _ ->
+ if self#display_comment () then fprintf fmt "/* format attribute */";
+ false
+
+ | "hidden", _ -> (* hidden attribute list *)
+ false
+ (* sm: here's another one I don't want to see gcc warnings about.. *)
+ | "mayPointToStack", _ when not state.print_cil_input ->
+ (* [matth: may be inside another comment.]
+ -> text "/*mayPointToStack*/", false *)
false
+ | "arraylen", [a] ->
+ if self#display_comment () then fprintf fmt "/*[%a]*/" self#attrparam a;
+ false
+ | "static",_ ->
+ if self#display_comment () then fprintf fmt "/* static */"; false
+ | "", _ ->
+ fprintf fmt "%a "
+ (Pretty_utils.pp_list ~sep:" " self#attrparam) args;
+ true
+ | s, _ when
+ s = Ast_attributes.bitfield_attribute_name &&
+ not state.print_cil_as_is &&
+ not (Kernel.is_debug_key_enabled Kernel.dkey_print_bitfields) ->
+ false
+ | _ -> (* This is the default case *)
+ (* Add underscores to the name *)
+ let an' =
+ if Machine.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
+ in
+ (match args with
+ | [] -> fprintf fmt "%s" an'
+ | _ :: _ ->
+ fprintf fmt "%s(%a)"
+ an'
+ (Pretty_utils.pp_list ~sep:"," self#attrparam) args);
+ true
+
method private attribute_prec (contextprec: int) fmt (a: attrparam) =
let thisLevel = Precedence.getParenthLevelAttrParam a in
let needParens =
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 9c02660d5e2..33369ab523b 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -166,10 +166,8 @@ and pp_fkind fmt = function
| FDouble -> Format.fprintf fmt "FDouble"
| FLongDouble -> Format.fprintf fmt "FLongDouble"
-and pp_attribute fmt = function
- | Attr(string,attrparam_list) ->
- Format.fprintf fmt "Attr(%a,%a)" pp_string string (pp_list pp_attrparam) attrparam_list
- | AttrAnnot(string) -> Format.fprintf fmt "AttrAnnot(%a)" pp_string string
+and pp_attribute fmt (string,attrparam_list) =
+ Format.fprintf fmt "(%a,%a)" pp_string string (pp_list pp_attrparam) attrparam_list
and pp_attributes fmt attributes = (pp_list pp_attribute) fmt attributes
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 8da3a7d6b25..429bf58c7a2 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -191,7 +191,6 @@ let rec print_specifiers fmt (specs: spec_elem list) =
| SpecCV CV_CONST -> fprintf fmt "const"
| SpecCV CV_VOLATILE -> fprintf fmt "volatile"
| SpecCV CV_RESTRICT -> fprintf fmt "restrict"
- | SpecCV (CV_ATTRIBUTE_ANNOT a) -> fprintf fmt "/*@@ %s */" a
| SpecCV CV_GHOST -> fprintf fmt "\\ghost"
| SpecAttr al -> print_attribute fmt al
| SpecType bt -> print_type_spec fmt bt
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 5eec71c9923..1c5ee580498 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -111,10 +111,10 @@ let declaration = function
-> GVarDecl(vi,loc)
| GAsm(_,loc) -> GAsm("…",loc)
| GText s when String.length s > 20 -> GText(String.sub s 0 20 ^ "…")
- | GPragma(Attr(a,_),loc) -> GPragma(Attr(a,[]),loc)
+ | GPragma((a,_),loc) -> GPragma((a,[]),loc)
| GAnnot _ -> GText "Global annotation"
| ( GType _ | GCompTagDecl _ | GEnumTagDecl _
- | GVarDecl _ | GText _ | GPragma _) as g -> g
+ | GVarDecl _ | GText _ ) as g -> g
let signature_of_declaration = function
| SEnum ei -> GEnumTagDecl(ei,Location.unknown)
diff --git a/src/kernel_services/ast_queries/ast_attributes.ml b/src/kernel_services/ast_queries/ast_attributes.ml
index 7616975da90..b708c5698b0 100644
--- a/src/kernel_services/ast_queries/ast_attributes.ml
+++ b/src/kernel_services/ast_queries/ast_attributes.ml
@@ -25,7 +25,7 @@
open Cil_types
(* Construct sorted lists of attributes *)
-let attribute_name (Attr(an, _) | AttrAnnot an) =
+let attribute_name (an, _) =
Extlib.strip_underscore an
let has_attribute an al =
@@ -42,10 +42,10 @@ let has_attribute an al =
The result is [].
*)
-let add_attribute (Attr(an, _) | AttrAnnot an as a) al =
+let add_attribute ((an, _) as a) al =
let rec insert_sorted = function
| [] -> [a]
- | ((Attr(an0, _) | AttrAnnot an0 as a0) :: rest) as l ->
+ | (((an0, _) as a0) :: rest) as l ->
if an < an0 then a :: l
else if Cil_datatype.Attribute.equal a a0 then l (* Do not add if already in there *)
else a0 :: insert_sorted rest (* Make sure we see all attributes with
@@ -76,10 +76,8 @@ let rec drop_attributes anl al =
let find_attribute an al =
let an = Extlib.strip_underscore an in
- List.fold_left (fun acc a ->
- match a with
- | Attr (_, param) as a0 when attribute_name a0 = an -> param @ acc
- | _ -> acc
+ List.fold_left (fun acc ((_, param) as a) ->
+ if attribute_name a = an then param @ acc else acc
) [] al
let filter_attributes an al =
@@ -150,8 +148,8 @@ let partition_attributes
(attrs: attribute list) :
attribute list * attribute list * attribute list =
let rec loop (n,f,t) = function
- [] -> n, f, t
- | (Attr(an, _) | AttrAnnot an as a) :: rest ->
+ | [] -> n, f, t
+ | ((an, _) as a) :: rest ->
match get_attribute_class ~default an with
AttrName _ -> loop (add_attribute a n, f, t) rest
| AttrFunType _ ->
@@ -201,7 +199,7 @@ let () = register_attribute bitfield_attribute_name AttrType
let anonymous_attribute_name = "fc_anonymous"
let () = register_attribute anonymous_attribute_name AttrIgnored
-let anonymous_attribute = Attr(anonymous_attribute_name, [])
+let anonymous_attribute = (anonymous_attribute_name, [])
let qualifier_attributes = [ "const"; "restrict"; "volatile"; "ghost" ]
let () = register_attributes AttrType qualifier_attributes
@@ -243,13 +241,10 @@ let () =
let () =
Cil_datatype.drop_unknown_attributes :=
- let is_annot_or_known_attr = function
- | Attr (name, _) -> is_known_attribute name
- (* Attribute annotations are always known. *)
- | AttrAnnot _ -> true
+ let is_annot_or_known_attr (name, _) =
+ is_known_attribute name
in
- (fun attributes ->
- List.filter is_annot_or_known_attr attributes)
+ (fun attributes -> List.filter is_annot_or_known_attr attributes)
(**********************)
(* Utility functions *)
@@ -262,7 +257,7 @@ let split_array_attributes al =
List.partition (fun a -> List.mem (attribute_name a) qualifier_attributes) al
let split_storage_modifier al =
- let isstoragemod (Attr(an, _) | AttrAnnot an : attribute) : bool =
+ let isstoragemod ((an, _) : attribute) : bool =
try
match Hashtbl.find attribute_hash an with
| AttrName issm -> issm
@@ -275,10 +270,6 @@ let split_storage_modifier al =
(* Put back the declspec. Put it without the leading __ since these will
* be added later *)
let stom' =
- List.map (fun a ->
- match a with
- | Attr(an, args) -> Attr("declspec", [ACons(an, args)])
- | AttrAnnot _ -> assert false
- ) stom
+ List.map (fun (an, args) -> ("declspec", [ACons(an, args)])) stom
in
stom', rest
diff --git a/src/kernel_services/ast_queries/ast_attributes.mli b/src/kernel_services/ast_queries/ast_attributes.mli
index 71bc759ca28..5eebd3923aa 100644
--- a/src/kernel_services/ast_queries/ast_attributes.mli
+++ b/src/kernel_services/ast_queries/ast_attributes.mli
@@ -145,19 +145,19 @@ type attribute_class =
ignored by functions {!get_attribute_class} and {!partition_attributes}. *)
| AttrIgnored
-(* Table containing all registered attributes. *)
+(** Table containing all registered attributes. *)
val attribute_hash : (string, attribute_class) Hashtbl.t
(** Add a new attribute with a specified class *)
val register_attribute : string -> attribute_class -> unit
(** Register a list of attributes with a given class. *)
-val register_attribute : string list -> attribute_class -> unit
+val register_attributes : attribute_class -> string list -> unit
(** Remove an attribute previously registered. *)
val remove_attribute : string -> unit
-(** Return the class of an attributes. The class `default' is returned for
+(** Return the class of an attribute. The class `default' is returned for
unknown and ignored attributes.
*)
val get_attribute_class : default:attribute_class -> string -> attribute_class
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 7cd64940bf5..ad331563b47 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -231,7 +231,7 @@ let typeHasAttributeMemoryBlock a (ty:typ): bool =
let typeAddGhost typ =
if not (typeHasAttribute "ghost" typ) then
- typeAddAttributes [Attr ("ghost", [])] typ
+ typeAddAttributes [("ghost", [])] typ
else
typ
@@ -917,7 +917,7 @@ let transient_block b =
"ignoring request to mark transient a block with local variables:@\n%a"
Cil_datatype.Block.pretty b
end else
- b.battrs <- add_attribute (Attr (vis_tmp_attr,[])) b.battrs; b
+ b.battrs <- add_attribute (vis_tmp_attr,[]) b.battrs; b
let block_of_transient b =
if has_attribute vis_tmp_attr b.battrs then begin
@@ -2033,7 +2033,7 @@ and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
let make i = mkStmt ~ghost:res.ghost (Instr i) in
let last = mkStmt ~ghost:res.ghost res.skind in
let block = mkBlockNonScoping (List.map make instr_list @ [ last ]) in
- block.battrs <- add_attribute (Attr (vis_tmp_attr, [])) block.battrs;
+ block.battrs <- add_attribute (vis_tmp_attr, []) block.battrs;
(* Make our statement contain the instructions to prepend *)
res.skind <- Block block;
vis#pop_stmt s; res
@@ -2305,14 +2305,10 @@ and visitCilAttributes (vis: cilVisitor) (al: attribute list) : attribute list=
add_attributes al' []
else
al
-and childrenAttribute (vis: cilVisitor) (a: attribute) : attribute =
+and childrenAttribute (vis: cilVisitor) ((n, args) as a: attribute) : attribute =
let fAttrP a = visitCilAttrParams vis a in
- match a with
- | Attr (n, args) ->
- let args' = Extlib.map_no_copy fAttrP args in
- if args' != args then Attr(n, args') else a
- | AttrAnnot _ ->
- a
+ let args' = Extlib.map_no_copy fAttrP args in
+ if args' != args then (n, args') else a
and visitCilAttrParams (vis: cilVisitor) (a: attrparam) : attrparam =
doVisitCil vis id vis#vattrparam childrenAttrparam a
@@ -2993,11 +2989,11 @@ let mkLoop ?sattr ~(guard:exp) ~(body: stmt list) () : stmt list =
body), guard.eloc, None, None)) ]
let mkWhile ?sattr ~(guard:exp) ~(body: stmt list) () : stmt list =
- let sattr = [Attr("while", [])] @ Option.value ~default:[] sattr in
+ let sattr = [("while", [])] @ Option.value ~default:[] sattr in
mkLoop ~sattr ~guard ~body ()
let mkDoWhile ?sattr ~(body: stmt list) ~(guard:exp) () : stmt list =
- let sattr = [Attr("dowhile", [])] @ Option.value ~default:[] sattr in
+ let sattr = [("dowhile", [])] @ Option.value ~default:[] sattr in
let exit_stmt =
mkStmt ~valid_sid:true
(If(guard, mkBlock [mkStmt ~valid_sid:true (Break guard.eloc)],
@@ -3008,7 +3004,7 @@ let mkDoWhile ?sattr ~(body: stmt list) ~(guard:exp) () : stmt list =
let mkFor ?sattr ~(start: stmt list) ~(guard: exp) ~(next: stmt list)
~(body: stmt list) () : stmt list =
- let sattr = [Attr("for", [])] @ Option.value ~default:[] sattr in
+ let sattr = [("for", [])] @ Option.value ~default:[] sattr in
(start @
(mkLoop ~sattr ~guard ~body:(body @ next)) ())
@@ -3293,7 +3289,7 @@ let rec typeOf (e: exp) : typ =
| Const(CStr _s) -> string_literal_type ()
| Const(CWStr _s) ->
- let typ = typeAddAttributes [Attr("const",[])] (wchar_type ()) in
+ let typ = typeAddAttributes [("const",[])] (wchar_type ()) in
Cil_const.mk_tptr typ
| Const(CReal (_, fk, _)) -> Cil_const.mk_tfloat fk
@@ -3778,7 +3774,7 @@ and process_aligned_attribute (pp:Format.formatter->unit) ~may_reduce attrs defa
Kernel.warning ~current:true "ignoring recursive align attributes on %t"
pp;
default_align ()
- | (Attr(_, [a]) as at)::rest -> begin
+ | ((_, [a]) as at)::rest -> begin
if rest <> [] then
Kernel.warning ~current:true "ignoring duplicate align attributes on %t"
pp;
@@ -3789,7 +3785,7 @@ and process_aligned_attribute (pp:Format.formatter->unit) ~may_reduce attrs defa
!pp_attribute_ref at pp;
default_align ()
end
- | Attr(_, [])::rest ->
+ | (_, [])::rest ->
(* aligned with no arg means a power of two at least as large as
any alignment on the system.*)
if rest <> [] then
@@ -4727,7 +4723,7 @@ let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") ?loc name typ :
let makeit name =
let vi = makeLocal ~ghost ?loc ~formal:true fdec name typ in
if ghost && not fdec.svar.vghost then
- vi.vattr <- add_attribute (Attr(frama_c_ghost_formal, [])) vi.vattr ;
+ vi.vattr <- add_attribute (frama_c_ghost_formal, []) vi.vattr ;
vi
in
let error () = Kernel.fatal ~current:true
@@ -6797,7 +6793,7 @@ let pushGlobal (g: global)
let varsintype : (varinfo list * location) option =
match g with
GType (_, l) | GCompTag (_, l) -> Some (getVarsInGlobal g, l)
- | GEnumTag (_, l) | GPragma (Attr("pack", _), l)
+ | GEnumTag (_, l) | GPragma (("pack", _), l)
| GCompTagDecl (_, l) | GEnumTagDecl (_, l) -> Some ([], l)
(* Move the warning pragmas early
| GPragma(Attr(s, _), l) when hasPrefix "warning" s -> Some ([], l)
@@ -7191,8 +7187,8 @@ class dropAttributes ?select () = object(self)
| None -> ChangeTo []
| Some l ->
(match a with
- | (Attr (s,_) | AttrAnnot s) when List.mem s l -> ChangeTo []
- | Attr _ | AttrAnnot _ -> DoChildren)
+ | (s,_) when List.mem s l -> ChangeTo []
+ | _ -> DoChildren)
method! vtype ty = match ty.tnode with
| TNamed internal_ty ->
let tty = typeAddAttributes ty.tattr internal_ty.ttype in
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index a99e24f9295..402c60ae9fc 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -45,7 +45,7 @@
open Cil_datatype
open Cil_types
-let typeAddVolatile typ = Cil.typeAddAttributes [Attr ("volatile", [])] typ
+let typeAddVolatile typ = Cil.typeAddAttributes [("volatile", [])] typ
module Frama_c_builtins =
State_builder.Hashtbl
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index bb1b53f1429..2b16c75e0ba 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -77,12 +77,12 @@ let charPtrType = mk_tptr charType
let scharPtrType = mk_tptr scharType
let ucharPtrType = mk_tptr ucharType
let charConstPtrType =
- let charConst = mk_tint ~tattr:[Attr ("const", [])] IChar in
+ let charConst = mk_tint ~tattr:[("const", [])] IChar in
mk_tptr charConst
let voidPtrType = mk_tptr voidType
let voidConstPtrType =
- let voidConst = mk_tvoid ~tattr:[Attr ("const", [])] () in
+ let voidConst = mk_tvoid ~tattr:[("const", [])] () in
mk_tptr voidConst
let intPtrType = mk_tptr intType
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 30cbd6c1509..4d27119afab 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -407,12 +407,8 @@ type type_compare_config =
unroll: bool;
no_attrs:bool; }
-let rec compare_attribute config a1 a2 = match a1, a2 with
- | Attr (s1, l1), Attr (s2, l2) ->
- compare_chain (=?=) s1 s2 (compare_attrparam_list config) l1 l2
- | AttrAnnot s1, AttrAnnot s2 -> s1 =?= s2
- | Attr _, AttrAnnot _ -> -1
- | AttrAnnot _, Attr _ -> 1
+let rec compare_attribute config (s1, l1) (s2, l2) =
+ compare_chain (=?=) s1 s2 (compare_attrparam_list config) l1 l2
and compare_attributes config l1 l2 =
if config.no_attrs then 0
else
@@ -525,11 +521,10 @@ and compare_arg_list config l1 l2 =
compare_type config t1 t2
)) l1 l2
-let hash_attribute _config = function
- | AttrAnnot s -> Hashtbl.hash s
- | Attr (s, _) -> (* We do not hash attrparams. There is a recursivity problem
- with typ, and the equal function will be complicated enough in itself *)
- 3 * Hashtbl.hash s + 117
+let hash_attribute _config (s, _) =
+ (* We do not hash attrparams. There is a recursivity problem with typ, and the
+ equal function will be complicated enough in itself *)
+ 3 * Hashtbl.hash s + 117
let hash_attributes config l =
let attrs = if config.logic_type then !drop_non_logic_attributes l else l in
hash_list (hash_attribute config) attrs
@@ -573,7 +568,7 @@ module Attribute=struct
{ by_name = false; logic_type = false;
unroll = true; no_attrs = false }
let name = "Attribute"
- let reprs = [ AttrAnnot "" ]
+ let reprs = [ ("", []) ]
let compare = compare_attribute config
let hash = hash_attribute config
let equal = Datatype.from_compare
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index d0d9e23f7f9..22e1ba0213b 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -966,7 +966,7 @@ let cleanup file =
*)
b.battrs <- List.filter
(function
- | Attr(l,[]) when l = Cabs2cil.frama_c_keep_block -> false
+ | (l,[]) when l = Cabs2cil.frama_c_keep_block -> false
| _ -> true)
b.battrs;
b
@@ -1397,7 +1397,7 @@ class reorder_ast: Visitor.frama_c_visitor =
in
Datatype.String.Map.fold
(fun k l res ->
- let attr = if k = "" then [] else [ Attr("fc_stdlib", [AStr k])] in
+ let attr = if k = "" then [] else [ ("fc_stdlib", [AStr k])] in
let entries =
List.fold_left
(fun acc g ->
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index eef7a520d52..303bff8e488 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -307,7 +307,7 @@ let treal_zero ?(loc=Cil_datatype.Location.unknown) ?(ltyp=Lreal) () =
let tstring ?(loc=Cil_datatype.Location.unknown) s =
(* Cannot refer to Cil_const.charConstPtrType in this module... *)
- let typ = Cil_const.(mk_tptr (mk_tint ~tattr:[Attr("const", [])] IChar)) in
+ let typ = Cil_const.(mk_tptr (mk_tint ~tattr:[("const", [])] IChar)) in
term ~loc (TConst (LStr s)) (Ctype typ)
let tat ?(loc=Cil_datatype.Location.unknown) (t,label) =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 76e0293ea90..5929c76d877 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -116,7 +116,7 @@ let plain_array_to_ptr ty =
in
(* Normally, overflow is checked in bitsSizeOf itself *)
let la = AInt (Integer.of_int len) in
- [ Attr("arraylen",[la])]
+ [ ("arraylen",[la]) ]
with Cil.SizeOfError _ ->
Kernel.warning ~current:true
"Cannot represent length of array as an attribute";
@@ -818,12 +818,8 @@ let rec is_same_attrparam p1 p2 =
&& is_same_attrparam e1 e2
| _ -> false
-let is_same_attribute a1 a2 =
- match a1,a2 with
- | Attr (s1,prm1), Attr (s2,prm2) ->
- is_same_string s1 s2 && is_same_list is_same_attrparam prm1 prm2
- | AttrAnnot s1, AttrAnnot s2 -> is_same_string s1 s2
- | _ -> false
+let is_same_attribute (s1,prm1) (s2,prm2) =
+ is_same_string s1 s2 && is_same_list is_same_attrparam prm1 prm2
let is_same_attributes l1 l2 = is_same_list is_same_attribute l1 l2
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 041f2f43141..d577b127d1a 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -262,7 +262,7 @@ let inliner functions_to_inline = object (self)
callee return_aux args
in
let fun_name = Kernel_function.get_name callee in
- let new_attribute = Attr (Ast_attributes.frama_c_inlined,[AStr fun_name]) in
+ let new_attribute = (Ast_attributes.frama_c_inlined, [AStr fun_name]) in
block.battrs <- Ast_attributes.add_attribute new_attribute block.battrs;
let skind =
if needs_assign then begin
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index 518230655be..e9947222466 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -79,8 +79,7 @@ and storage =
| NO_STORAGE | AUTO | STATIC | EXTERN | REGISTER
and cvspec =
- | CV_CONST | CV_VOLATILE | CV_RESTRICT
- | CV_ATTRIBUTE_ANNOT of string | CV_GHOST
+ | CV_CONST | CV_VOLATILE | CV_RESTRICT | CV_GHOST
(* Type specifier elements. These appear at the start of a declaration *)
(* Everywhere they appear in this file, they appear as a 'spec_elem list', *)
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index 732ce601a40..cedc83e51f1 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -264,8 +264,6 @@ let mk_asm_templates =
else res in
outer []
-let mk_attr_annot s = "~attrannot:" ^ s, []
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/parsetree/cabshelper.mli b/src/kernel_services/parsetree/cabshelper.mli
index 1b1fbfc418e..018a68768e8 100644
--- a/src/kernel_services/parsetree/cabshelper.mli
+++ b/src/kernel_services/parsetree/cabshelper.mli
@@ -91,8 +91,3 @@ val mk_behavior :
Logic_ptree.behavior
val mk_asm_templates : string list -> string list
-val mk_attr_annot : string -> Cabs.attribute
-(** builds a Cabs attribute annotation
-
- @since 28.0-Nickel
-*)
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index e7ac47576eb..8fb37977157 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -400,7 +400,6 @@ type annot =
*) (** function specification. *)
| Acode_annot of location * code_annot (** code annotation. *)
| Aloop_annot of location * code_annot list (** loop annotation. *)
- | Aattribute_annot of location * string (** attribute annotation. *)
(** ACSL extension for external spec file **)
type ext_decl =
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 4f815c73192..b7e670fd4ce 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -704,7 +704,7 @@ let mk_gvar ?init ~ty name =
(* See if the variable is already declared *)
let vi =
try
- let ty' = typeAddAttributes [Attr ("ghost", [])] ty in
+ let ty' = typeAddAttributes [("ghost", [])] ty in
let vi = Globals.Vars.find_from_astinfo name Global in
if not (Cil_datatype.Typ.equal vi.vtype ty') then
Aorai_option.abort "Global %s is declared with type %a instead of %a"
@@ -935,7 +935,7 @@ class visit_decl_loops_init () =
let name = Data_for_aorai.loopInit ^ "_" ^ (string_of_int stmt.sid) in
let typ =
Cil.typeAddAttributes
- [Attr (Ast_attributes.frama_c_ghost_formal,[])] Cil_const.intType
+ [(Ast_attributes.frama_c_ghost_formal,[])] Cil_const.intType
in
let var = Cil.makeLocalVar ~ghost:true f ~scope name typ in
Data_for_aorai.set_varinfo name var
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index c7192179a9e..3617822cd9a 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -1054,13 +1054,5 @@ Figure~\ref{fig:gram:volatile} summarizes the grammar for volatile constructs.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Logic attribute annotations}
-\absentwhy{logic attributes are implementation dependent; therefore their
- meaning cannot be guessed by a general-purpose (runtime) verification tool}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
\section{Preprocessing for ACSL}
\nodiff
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 169c57e6db4..204f1fc45d7 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -289,7 +289,7 @@ let sufficiently_aligned vi algn =
List.fold_left
(fun acc attr ->
match attr with
- | Attr("align", [AInt i]) ->
+ | ("align", [AInt i]) ->
let alignment = Integer.to_int_exn i in
if acc <> 0 && acc <> alignment then begin
(* multiple align attributes with different values *)
@@ -309,7 +309,7 @@ let sufficiently_aligned vi algn =
algn
end else
alignment
- | Attr("align", _) ->
+ | ("align", _) ->
(* align attribute with an argument other than a single number,
should not happen really *)
assert false
@@ -470,7 +470,7 @@ let prepare_fundec kf =
storage of 32-bit timestamps in a 1:1 shadow. *)
if require_alignment vi 4 then
vi.vattr <-
- Attr("aligned", [ AInt Integer.four ]) :: vi.vattr)
+ ("aligned", [ AInt Integer.four ]) :: vi.vattr)
blk.blocals;
blk)
else
@@ -569,7 +569,7 @@ let sound_verdict_vi =
let vi = Cil.makeGlobalVar name Cil_const.intType in
vi.vstorage <- Extern;
vi.vreferenced <- true;
- vi.vattr <- Ast_attributes.add_attribute (Attr ("FC_BUILTIN", [])) vi.vattr;
+ vi.vattr <- Ast_attributes.add_attribute (("FC_BUILTIN", [])) vi.vattr;
vi)
let sound_verdict () = Lazy.force sound_verdict_vi
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index 5961c5caf16..8af074421fc 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -57,7 +57,7 @@ type validity_hidden_base =
| KnownThenUnknownValidity of Integer.t (* Base is valid on i bits, then
maybe invalid on the remainder of its validity *)
-let stdlib_attribute = Attr ("fc_stdlib_generated", [])
+let stdlib_attribute = ("fc_stdlib_generated", [])
let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
let hidden_var = Eva_utils.create_new_var hidden_var_name pointed_typ in
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 981053791a6..3cd056f257d 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -24,7 +24,7 @@ open Cil
open Cil_types
open Logic_const
-let const_of t = Cil.typeAddAttributes [Attr("const", [])] t
+let const_of t = Cil.typeAddAttributes [("const", [])] t
let size_t () =
Globals.Types.find_type Logic_typing.Typedef "size_t"
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index c42c870b3c3..4f91ad9ca03 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -192,10 +192,9 @@ class visitor = object
Dictionary.fresh Obfuscator_kind.Logic_constructor lci.ctor_name ;
Cil.DoChildren
- method! vattr = function
- | Attr(str, _) | AttrAnnot str ->
- warn "attribute" str;
- Cil.DoChildren
+ method! vattr (str, _) =
+ warn "attribute" str;
+ Cil.DoChildren
method! vattrparam p =
(match p with
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index 69267cfe9d9..52ad6b8f3a1 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -30,7 +30,7 @@ module Build = Cil_builder.Pure
(* Types of variadic parameter and argument *)
let vpar_typ tattr =
- Cil_const.(mk_tptr ~tattr (mk_tptr ~tattr:[Attr ("const", [])] voidType))
+ Cil_const.(mk_tptr ~tattr (mk_tptr ~tattr:[("const", [])] voidType))
let vpar_name = "__va_params"
let vpar =
(vpar_name, vpar_typ [], [])
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 58d876632b4..87bb380a464 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -830,11 +830,14 @@ module Nullable =
struct
let attribute_name = "wp_nullable"
+ let () =
+ Ast_attributes.register_attribute attribute_name (AttrName false)
+
let is_nullable vi =
vi.vformal && Ast_attributes.has_attribute attribute_name vi.vattr
let make_nullable vi =
- vi.vattr <- Ast_attributes.add_attribute (AttrAnnot attribute_name) vi.vattr
+ vi.vattr <- Ast_attributes.add_attribute (attribute_name, []) vi.vattr
module Nullable_extension =
struct
diff --git a/src/plugins/wp/doc/manual/nullable.c b/src/plugins/wp/doc/manual/nullable.c
index f84f31d995e..00ccce385ff 100644
--- a/src/plugins/wp/doc/manual/nullable.c
+++ b/src/plugins/wp/doc/manual/nullable.c
@@ -1,4 +1,5 @@
-void foo(int* p /*@ wp_nullable */, int* q /*@ wp_nullable */){
+void foo(int* p __attribute__((wp_nullable)),
+ int* q __attribute__((wp_nullable))){
}
diff --git a/src/plugins/wp/tests/wp_plugin/nullable.i b/src/plugins/wp/tests/wp_plugin/nullable.i
index ff08ead486c..4350939317a 100644
--- a/src/plugins/wp/tests/wp_plugin/nullable.i
+++ b/src/plugins/wp/tests/wp_plugin/nullable.i
@@ -9,7 +9,7 @@ int x ;
int *g ;
/*@ assigns *g, *p, x ; */
-void nullable_coherence(int* p /*@ wp_nullable */){
+void nullable_coherence(int* p __attribute__((wp_nullable))){
if(p == (void*)0){
//@ check must_fail: \false ;
return;
@@ -22,9 +22,9 @@ void nullable_coherence(int* p /*@ wp_nullable */){
//@ assigns *p, *q, *r, *s, *t ;
void nullable_in_context
-(int* p /*@ wp_nullable */,
- int* q /*@ wp_nullable */,
- int* r /*@ wp_nullable */,
+(int* p __attribute__((wp_nullable)),
+ int* q __attribute__((wp_nullable)),
+ int* r __attribute__((wp_nullable)),
int* s, int* t)
{
*p = 42;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
index 1f364e1c6cf..e043446bfbd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
@@ -50,7 +50,7 @@ Prove: true.
requires \separated(p, &x);
requires p ≢ \null ⇒ \separated(g, p, &x);
*/
- void nullable_coherence(int *p /*@ wp_nullable */);
+ void nullable_coherence(int *p __attribute__((__wp_nullable__)));
[wp] nullable.i:24: Warning:
Memory model hypotheses for function 'nullable_in_context':
/*@
@@ -67,6 +67,7 @@ Prove: true.
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
*/
- void nullable_in_context(int *p /*@ wp_nullable */,
- int *q /*@ wp_nullable */,
- int *r /*@ wp_nullable */, int *s, int *t);
+ void nullable_in_context(int *p __attribute__((__wp_nullable__)),
+ int *q __attribute__((__wp_nullable__)),
+ int *r __attribute__((__wp_nullable__)), int *s,
+ int *t);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle
index d82b278274c..82895937bb7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle
@@ -60,7 +60,7 @@ Prove: true.
requires \separated(p, &x);
requires p ≢ \null ⇒ \separated(g, p, &x);
*/
- void nullable_coherence(int *p /*@ wp_nullable */);
+ void nullable_coherence(int *p __attribute__((__wp_nullable__)));
[wp] nullable_ext.c:36: Warning:
Memory model hypotheses for function 'nullable_in_context':
/*@
@@ -77,9 +77,10 @@ Prove: true.
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
*/
- void nullable_in_context(int *p /*@ wp_nullable */,
- int *q /*@ wp_nullable */,
- int *r /*@ wp_nullable */, int *s, int *t);
+ void nullable_in_context(int *p __attribute__((__wp_nullable__)),
+ int *q __attribute__((__wp_nullable__)),
+ int *r __attribute__((__wp_nullable__)), int *s,
+ int *t);
[wp] nullable_ext.c:47: Warning:
Memory model hypotheses for function 'with_declaration':
/*@ behavior wp_typed_caveat:
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
index 1d2c13060d1..9baa67840e7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
@@ -33,7 +33,7 @@
requires \separated(p, &x);
requires p ≢ \null ⇒ \separated(g, p, &x);
*/
- void nullable_coherence(int *p /*@ wp_nullable */);
+ void nullable_coherence(int *p __attribute__((__wp_nullable__)));
[wp] nullable.i:24: Warning:
Memory model hypotheses for function 'nullable_in_context':
/*@
@@ -50,6 +50,7 @@
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
*/
- void nullable_in_context(int *p /*@ wp_nullable */,
- int *q /*@ wp_nullable */,
- int *r /*@ wp_nullable */, int *s, int *t);
+ void nullable_in_context(int *p __attribute__((__wp_nullable__)),
+ int *q __attribute__((__wp_nullable__)),
+ int *r __attribute__((__wp_nullable__)), int *s,
+ int *t);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
index da1c72f49a5..6fbb7ca2b8d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
@@ -37,7 +37,7 @@
requires \separated(p, &x);
requires p ≢ \null ⇒ \separated(g, p, &x);
*/
- void nullable_coherence(int *p /*@ wp_nullable */);
+ void nullable_coherence(int *p __attribute__((__wp_nullable__)));
[wp] nullable_ext.c:36: Warning:
Memory model hypotheses for function 'nullable_in_context':
/*@
@@ -54,9 +54,10 @@
requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
*/
- void nullable_in_context(int *p /*@ wp_nullable */,
- int *q /*@ wp_nullable */,
- int *r /*@ wp_nullable */, int *s, int *t);
+ void nullable_in_context(int *p __attribute__((__wp_nullable__)),
+ int *q __attribute__((__wp_nullable__)),
+ int *r __attribute__((__wp_nullable__)), int *s,
+ int *t);
[wp] nullable_ext.c:47: Warning:
Memory model hypotheses for function 'with_declaration':
/*@ behavior wp_typed_caveat:
diff --git a/tests/spec/ghost_attribute.i b/tests/spec/ghost_attribute.i
index 5e4db1cae7d..e38e02e72bd 100644
--- a/tests/spec/ghost_attribute.i
+++ b/tests/spec/ghost_attribute.i
@@ -1,9 +1,46 @@
-void foo(int* p /*@ my_attribute */){
+/* run.config
+ MODULE: @PTEST_NAME@
+ STDOPT:
+*/
+
+/* attribute annotation are not supported anymore, they should be replaced with
+ normal attributes which can be registered via the API.
+ The script ghost_attribute.ml registers the attribute "registered_attr" on
+ types.
+*/
+
+/* Not supported anymore, by default annotations will be ignored with a warning
+ in parsing phase
+*/
+void attr_annot(int* p /*@ my_attribute */){
int /*@ my_attribute */ v ;
}
/*@ ghost
- void bar(int* p /@ my_attribute @/){
+ void attr_annot_ghost(int* p /@ my_attribute @/){
int /@ my_attribute @/ v ;
}
*/
+
+/* Unregistered attribute will be kept, but a warning will be emitted, and these
+ attributes are ignored when comparing types.
+*/
+void unregistered_attr(int* p __attribute__((unregistered_attr))){
+ int __attribute__((unregistered_attr)) v ;
+}
+
+/*@ ghost
+ void unregistered_attr_ghost(int* p __attribute__((unregistered_attr))){
+ int __attribute__((unregistered_attr)) v ;
+ }
+*/
+
+void registered_attr(int* p __attribute__((registered_attr))){
+ int __attribute__((registered_attr)) v ;
+}
+
+/*@ ghost
+ void registered_attr_ghost(int* p __attribute__((registered_attr))){
+ int __attribute__((registered_attr)) v ;
+ }
+*/
diff --git a/tests/spec/ghost_attribute.ml b/tests/spec/ghost_attribute.ml
new file mode 100644
index 00000000000..4c84609f897
--- /dev/null
+++ b/tests/spec/ghost_attribute.ml
@@ -0,0 +1 @@
+let () = Ast_attributes.register_attribute "registered_attr" AttrType
diff --git a/tests/spec/oracle/ghost_attribute.res.oracle b/tests/spec/oracle/ghost_attribute.res.oracle
index 1bc096db914..d7dbec0e605 100644
--- a/tests/spec/oracle/ghost_attribute.res.oracle
+++ b/tests/spec/oracle/ghost_attribute.res.oracle
@@ -1,15 +1,60 @@
[kernel] Parsing ghost_attribute.i (no preprocessing)
+[kernel:annot-error] ghost_attribute.i:15: Warning:
+ unexpected token 'my_attribute'
+[kernel:annot-error] ghost_attribute.i:16: Warning:
+ unexpected token 'my_attribute'
+[kernel:annot-error] ghost_attribute.i:20: Warning:
+ unexpected token 'my_attribute'
+[kernel:annot-error] ghost_attribute.i:21: Warning:
+ unexpected token 'my_attribute'
+[kernel:unknown-attribute] ghost_attribute.i:28: Warning:
+ Unknown attribute: unregistered_attr
+[kernel:unknown-attribute] ghost_attribute.i:29: Warning:
+ Unknown attribute: unregistered_attr
+[kernel:unknown-attribute] ghost_attribute.i:33: Warning:
+ Unknown attribute: unregistered_attr
+[kernel:unknown-attribute] ghost_attribute.i:34: Warning:
+ Unknown attribute: unregistered_attr
/* Generated by Frama-C */
-void foo(int *p /*@ my_attribute */)
+void attr_annot(int *p)
{
- int /*@ my_attribute */ v;
+ int v;
+ return;
+}
+
+/*@ ghost void attr_annot_ghost(int *p)
+ {
+ int v;
+ return;
+ }
+
+*/
+
+void unregistered_attr(int *p __attribute__((__unregistered_attr__)))
+{
+ int __attribute__((__unregistered_attr__)) v;
+ return;
+}
+
+/*@ ghost
+ void unregistered_attr_ghost(int *p __attribute__((__unregistered_attr__)))
+ {
+ int __attribute__((__unregistered_attr__)) v;
+ return;
+ }
+
+*/
+
+void registered_attr(int * __attribute__((__registered_attr__)) p)
+{
+ int __attribute__((__registered_attr__)) v;
return;
}
/*@ ghost
- void bar(int *p /@ my_attribute @/)
+ void registered_attr_ghost(int * __attribute__((__registered_attr__)) p)
{
- int /@ my_attribute @/ v;
+ int __attribute__((__registered_attr__)) v;
return;
}
diff --git a/tests/spec/oracle/parsing.res.oracle b/tests/spec/oracle/parsing.res.oracle
index 0fff45c528f..7dc69f6d6b5 100644
--- a/tests/spec/oracle/parsing.res.oracle
+++ b/tests/spec/oracle/parsing.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing parsing.c (with preprocessing)
-[kernel:annot-error] parsing.c:27: Warning: unexpected token 'bla'
+[kernel:annot-error] parsing.c:27: Warning: unexpected token 'private'
[kernel:annot-error] parsing.c:15: Warning:
comparison of incompatible types: 𔹠and ℤ. Ignoring global annotation
[kernel:annot-error] parsing.c:19: Warning:
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
index 23eb9fb13e2..86213717217 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
@@ -1,11 +1,5 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] ghost_cv_parsing_errors.c:26:
- Use of \ghost out of ghost code:
- Location: line 26, between columns 8 and 14, before or at token: global
- 24 #ifdef IN_GHOST_ATTR
- 25
- 26 int /*@ \ghost */ global ;
- ^^^^^^
- 27
- 28 #endif
+[kernel:annot-error] ghost_cv_parsing_errors.c:26: Warning:
+ unexpected token '\ghost'
+[kernel] User Error: warning annot-error treated as fatal error.
[kernel] Frama-C aborted: invalid user input.
--
GitLab