diff --git a/Changelog b/Changelog
index 032638655591d1acf520615275efbd6427fa30fb..43b29905d82d4de3abf001b0195269bd3fabef8f 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,7 @@
Open Source Release <next-release>
###############################################################################
+- Kernel [2024-10-15] Warn when encountering an unknown attribute
o! Kernel [2024-10-08] introduce logic type Lboolean and constants
- Kernel [2024-10-08] Asm contracts can now have \initialized ensures.
See option -asm-contracts-ensure-init
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4d639ed255a09ae499690bfd07c50c50d7c8e2e9..4ad7be278ca025c73500ba4d94526d29584247e8 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -93,8 +93,21 @@ let unsupported_attributes = ["vector_size"]
(* Attributes which must be erased to avoid issues (e.g., GCC 'malloc'
attributes can refer to erased functions and make the code un-reparsable *)
let erased_attributes = ["malloc"]
+let () =
+ List.iter
+ (fun a -> Cil.registerAttribute a AttrIgnored)
+ erased_attributes
-let stripUnderscore ?(checkUnsupported=true) s =
+(* 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
Kernel.error ~once:true ~current:true "Invalid attribute name %s" s;
@@ -103,24 +116,52 @@ let stripUnderscore ?(checkUnsupported=true) s =
let res = Extlib.strip_underscore s in
if res = "" then
Kernel.error ~once:true ~current:true "Invalid attribute name %s" s;
- if checkUnsupported && List.mem res unsupported_attributes then
- Kernel.error ~current:true "unsupported attribute: %s" 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 (Cil.isKnownAttribute res) then
+ Kernel.warning
+ ~once:true ~current:true ~wkey:Kernel.wkey_unknown_attribute
+ "Unknown attribute: %s" s
+ end;
res
end
let frama_c_keep_block = "FRAMA_C_KEEP_BLOCK"
let () = Cil_printer.register_shallow_attribute frama_c_keep_block
+let () = Cil.registerAttribute frama_c_keep_block AttrStmt
let fc_stdlib = "fc_stdlib"
let fc_stdlib_generated = "fc_stdlib_generated"
let () = Cil_printer.register_shallow_attribute fc_stdlib
let () = Cil_printer.register_shallow_attribute fc_stdlib_generated
+(* fc_stdlib attribute already registered in cil.ml *)
+let () = Cil.registerAttribute fc_stdlib_generated (AttrName false)
let fc_local_static = "fc_local_static"
let () = Cil_printer.register_shallow_attribute fc_local_static
+let () = Cil.registerAttribute fc_local_static (AttrName false)
-let frama_c_destructor = "__fc_destructor"
+let frama_c_destructor = "fc_destructor"
let () = Cil_printer.register_shallow_attribute frama_c_destructor
+let () = Cil.registerAttribute frama_c_destructor (AttrName false)
+
+let () =
+ (* packed and aligned are treated separately, we ignore them
+ during standard processing.
+ *)
+ Cil.registerAttribute "packed" AttrIgnored;
+ Cil.registerAttribute "aligned" AttrIgnored;
+ Cil.registerAttribute "warn_unused_result" (AttrFunType false);
+ Cil.registerAttribute "FC_OLDSTYLEPROTO" (AttrName false);
+ Cil.registerAttribute "static" (AttrName false);
+ Cil.registerAttribute "missingproto" (AttrName false);
+ Cil.registerAttribute "dummy" AttrIgnored
(** A hook into the code that creates temporary local vars. By default this
is the identity function, but you can overwrite it if you need to change the
@@ -3672,15 +3713,6 @@ let continueUsed () =
(****** TYPE SPECIFIERS *******)
-(* 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
-
type local_env =
{ authorized_reads: Lval.Set.t;
@@ -4625,15 +4657,23 @@ and cabsPartitionAttributes
let rec loop (n,f,t) = function
[] -> n, f, t
| a :: rest ->
- let kind = match doAttr ghost a with
- | [] -> default
+ let an, kind = match doAttr ghost a with
+ | [] -> "", default
| (Attr(an, _) | AttrAnnot an)::_ ->
- (try attributeClass an with Not_found -> default)
+ (* doAttr already strip underscores of the attribute if necessary so
+ we do not need to strip then before calling attributeClass here. *)
+ an, attributeClass ~default an
in
match kind with
| AttrName _ -> loop (a::n, f, t) rest
| AttrFunType _ -> loop (n, a::f, t) rest
| AttrType -> loop (n, f, a::t) rest
+ | AttrStmt ->
+ Kernel.warning
+ ~current:true "Ignoring statement attribute %s found in declaration"
+ an;
+ loop (n,f,t) rest
+ | AttrIgnored -> loop (n, f, t) rest
in
loop ([], [], []) attrs
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c018fc00b8bbc864177b46e20ed6d725d8bef91c..a229b8c21798ecd925c7171ad3392143198958a8 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2336,7 +2336,7 @@ class cil_printer () = object (self)
Format.pp_print_string fmt in__attr__;
if not block (* reversed so that highlighting matches *)
then fprintf fmt "))"
- else fprintf fmt ") %s" (for_cil "*/")
+ else fprintf fmt ") %s@\n" (for_cil "*/")
end
| x :: rest ->
let buff = Buffer.create 17 in
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d0ae997cb8a69a18b72a22113e9c7577ecd8353a..045236f50856988505304ba646d240e06a8243ae 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -160,7 +160,7 @@ let stmt_of_instr_list ?(loc=Location.unknown) = function
let bitfield_attribute_name = "FRAMA_C_BITFIELD_SIZE"
-let anonymous_attribute_name = "__fc_anonymous"
+let anonymous_attribute_name = "fc_anonymous"
let anonymous_attribute = Attr(anonymous_attribute_name, [])
(** Construct sorted lists of attributes ***)
@@ -408,7 +408,14 @@ type attributeClass =
(* Attribute of a function type. If argument is true and we are on
* MSVC then the attribute is printed just before the function name *)
- | AttrType (* Attribute of a type *)
+ | AttrType
+ (* Attribute of a type *)
+
+ | AttrStmt
+ (* Attribute of a statement or block *)
+
+ | AttrIgnored
+ (** Attribute that does not correspond to either of the above classes. *)
(* This table contains the mapping of predefined attributes to classes.
* Extend this table with more attributes as you need. This table is used to
@@ -420,8 +427,8 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
[ "section"; "constructor"; "destructor"; "unused"; "used"; "weak";
"no_instrument_function"; "alias"; "no_check_memory_usage";
"exception"; "model"; (* "restrict"; *)
- "aconst"; "__asm__" (* Gcc uses this to specify the name to be used in
- * assembly for a global *)];
+ "aconst"; "asm" (* Gcc uses this to specify the name to be used in
+ * assembly for a global *)];
(* Now come the MSVC declspec attributes *)
List.iter (fun a -> Hashtbl.add table a (AttrName true))
[ "thread"; "naked"; "dllimport"; "dllexport";
@@ -432,12 +439,32 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
[ "stdcall";"cdecl"; "fastcall"; "noreturn"];
List.iter (fun a -> Hashtbl.add table a AttrType)
- [ "const"; "volatile"; "restrict"; "mode" ];
+ ("mode" :: qualifier_attributes);
table
-let attributeClass = Hashtbl.find attributeHash
-
-let registerAttribute = Hashtbl.add attributeHash
+let isKnownAttribute = Hashtbl.mem attributeHash
+
+let attributeClass ~default name =
+ match Hashtbl.find attributeHash name with
+ | exception Not_found -> default
+ | AttrIgnored -> default
+ | ac -> ac
+
+let registerAttribute an ac =
+ if Hashtbl.mem attributeHash an then begin
+ let pp fmt c =
+ match c with
+ | AttrName b -> Format.fprintf fmt "(AttrName %B)" b
+ | AttrFunType b -> Format.fprintf fmt "(AttrFunType %B)" b
+ | AttrType -> Format.fprintf fmt "AttrType"
+ | AttrIgnored -> Format.fprintf fmt "AttrIgnored"
+ | AttrStmt -> Format.fprintf fmt "AttrStmt"
+ in
+ Kernel.warning
+ "Replacing existing class for attribute %s: was %a, now %a"
+ an pp (Hashtbl.find attributeHash an) pp ac
+ end;
+ Hashtbl.replace attributeHash an ac
let removeAttribute = Hashtbl.remove attributeHash
(** Partition the attributes into classes *)
@@ -448,38 +475,42 @@ let partitionAttributes
let rec loop (n,f,t) = function
[] -> n, f, t
| (Attr(an, _) | AttrAnnot an as a) :: rest ->
- match (try Hashtbl.find attributeHash an with Not_found -> default) with
+ match attributeClass ~default an with
AttrName _ -> loop (addAttribute a n, f, t) rest
| AttrFunType _ ->
loop (n, addAttribute a f, t) rest
| AttrType -> loop (n, f, addAttribute a t) rest
+ | AttrStmt ->
+ Kernel.warning "unexpected statement attribute %s" an;
+ loop (n,f,t) rest
+ | AttrIgnored -> loop (n, f, t) rest
in
loop ([], [], []) attrs
-let frama_c_ghost_else = "__fc_ghost_else"
-let () = registerAttribute frama_c_ghost_else (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_ghost_else) (AttrName false)
+let frama_c_ghost_else = "fc_ghost_else"
+let () = registerAttribute frama_c_ghost_else (AttrStmt)
-let frama_c_ghost_formal = "__fc_ghost_formal"
+let frama_c_ghost_formal = "fc_ghost_formal"
let () = registerAttribute frama_c_ghost_formal (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_ghost_formal) (AttrName false)
-let frama_c_init_obj = "__fc_initialized_object"
+let frama_c_init_obj = "fc_initialized_object"
let () = registerAttribute frama_c_init_obj (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
-let frama_c_mutable = "__fc_mutable"
+let frama_c_mutable = "fc_mutable"
let () = registerAttribute frama_c_mutable (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_mutable) (AttrName false)
-let frama_c_inlined = "__fc_inlined"
-let () = registerAttribute frama_c_inlined (AttrName false)
+let frama_c_inlined = "fc_inlined"
+let () = registerAttribute frama_c_inlined (AttrFunType false)
+
let () =
- registerAttribute (Extlib.strip_underscore frama_c_inlined) (AttrName false)
+ registerAttribute bitfield_attribute_name AttrType;
+ registerAttribute anonymous_attribute_name AttrIgnored;
+ List.iter
+ (fun a -> registerAttribute a AttrIgnored)
+ fc_internal_attributes;
+ List.iter
+ (fun a -> registerAttribute a AttrType)
+ cast_irrelevant_attributes
let unrollType (t: typ) : typ =
let rec withAttrs (al: attributes) (t: typ) : typ =
@@ -4777,6 +4808,16 @@ let () = Cil_datatype.drop_non_logic_attributes :=
let () = Cil_datatype.drop_fc_internal_attributes :=
dropAttributes fc_internal_attributes
+let () =
+ Cil_datatype.drop_unknown_attributes :=
+ let is_annot_or_known_attr = function
+ | Attr (name, _) -> isKnownAttribute name
+ (* Attribute annotations are always known. *)
+ | AttrAnnot _ -> true
+ in
+ (fun attributes ->
+ List.filter is_annot_or_known_attr attributes)
+
let need_cast ?(force=false) oldt newt =
let oldt = type_remove_attributes_for_c_cast (unrollType oldt) in
let newt = type_remove_attributes_for_c_cast (unrollType newt) in
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 89ed0c7b2e406d5fec91bc268793392d1930e933..dd36accd6a0acfd37d7bb16c61bc41b5cc36539e 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1331,7 +1331,9 @@ val instr_falls_through : instr -> bool
(** {2 Values for manipulating attributes} *)
(* ************************************************************************* *)
-(** Various classes of attributes *)
+(** Various classes of attributes
+ @before Frama-C+dev [AttrStmt] and [AttrIgnored] didn't exist
+*)
type attributeClass =
AttrName of bool
(** Attribute of a name. If argument is true and we are on MSVC then
@@ -1340,7 +1342,13 @@ type attributeClass =
| AttrFunType of bool
(** Attribute of a function type. If argument is true and we are on
MSVC then the attribute is printed just before the function name *)
- | AttrType (** Attribute of a type *)
+ | AttrType
+ (** Attribute of a type *)
+ | AttrStmt
+ (** Attribute of a statement or a block *)
+ | AttrIgnored
+ (** Attribute that does not correspond to either of the above classes and is
+ ignored by functions [attributeClass] and [partitionAttributes]. *)
val registerAttribute: string -> attributeClass -> unit
(** Add a new attribute with a specified class *)
@@ -1348,11 +1356,23 @@ val registerAttribute: string -> attributeClass -> unit
val removeAttribute: string -> unit
(** Remove an attribute previously registered. *)
-val attributeClass: string -> attributeClass
-(** Return the class of an attributes. *)
+val isKnownAttribute: string -> bool
+(** [isKnownAttribute attrname] returns true if the attribute named [attrname]
+ is known by Frama-C.
+ @since Frama-C+dev
+*)
+
+val attributeClass: default:attributeClass -> string -> attributeClass
+(** Return the class of an attributes. The class `default' is returned for
+ unknown and ignored attributes.
+ @before Frama-C+dev no [default] argument
+*)
-(** Partition the attributes into classes:name attributes, function type,
- and type attributes *)
+(** Partition the attributes into classes: name attributes, function type and
+ type attributes. Unknown and ignored attributes are returned in the
+ `default` attribute class.
+ @before Frama-C+dev no [default] argument
+*)
val partitionAttributes: default:attributeClass ->
attributes -> attribute list * (* AttrName *)
attribute list * (* AttrFunType *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 65c8fe4fdb064a6164a459542b3b91f0267d9f5b..72cb7ce8618667f1b9ccf47343b782fd19b422a7 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -395,8 +395,9 @@ let index_typ = function
let constfoldtoint = Extlib.mk_fun "constfoldtoint"
let punrollType = Extlib.mk_fun "punrollType"
let punrollLogicType = Extlib.mk_fun "punrollLogicType"
-let drop_non_logic_attributes = ref (fun a -> a)
-let drop_fc_internal_attributes = ref (fun a -> a)
+let drop_non_logic_attributes = ref Fun.id
+let drop_fc_internal_attributes = ref Fun.id
+let drop_unknown_attributes = ref Fun.id
let compare_exp_struct_eq = Extlib.mk_fun "compare_exp_struct_eq"
type type_compare_config =
@@ -414,11 +415,14 @@ let rec compare_attribute config a1 a2 = match a1, a2 with
and compare_attributes config l1 l2 =
if config.no_attrs then 0
else
- let l1, l2 = if config.logic_type
+ let l1, l2 =
+ if config.logic_type
then !drop_non_logic_attributes l1, !drop_non_logic_attributes l2
else
!drop_fc_internal_attributes l1, !drop_fc_internal_attributes l2
- in compare_list (compare_attribute config) l1 l2
+ in
+ let l1, l2 = !drop_unknown_attributes l1, !drop_unknown_attributes l2 in
+ compare_list (compare_attribute config) l1 l2
and compare_attrparam_list config l1 l2 =
compare_list (compare_attrparam config) l1 l2
and compare_attrparam config a1 a2 = match a1, a2 with
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 7721ea20804f2149b9e1834aadb0463f878a0e31..6cedf7e01a5d0b86bbbc8a15f15f1c022c25a7b4 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -393,6 +393,7 @@ module Lexpr: S with type t = Logic_ptree.lexpr
(* Forward declarations from Cil et al. *)
val drop_non_logic_attributes : (attributes -> attributes) ref
val drop_fc_internal_attributes : (attributes -> attributes) ref
+val drop_unknown_attributes : (attributes -> attributes) ref
val constfoldtoint : (exp -> Integer.t option) ref
val punrollType: (typ -> typ) ref
val punrollLogicType: (logic_type -> logic_type) ref
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index e704803c577786149f2a0174d9f55535a104dc1b..b6de99d7c30d682b0d9940b5ed741dfc83f02502 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -252,6 +252,8 @@ let () = set_warn_status wkey_c11 Log.Winactive
let wkey_line_directive = register_warn_category "pp:line-directive"
+let wkey_unknown_attribute = register_warn_category "unknown-attribute"
+
(* ************************************************************************* *)
(** {2 Specialised functors for building kernel parameters} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 8472baa286db098f13eb54ced7bb331744d3f3e5..b21f4d05ced4ccb73864090865dad84b37fd7404 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -245,6 +245,9 @@ val wkey_c11: warn_category
val wkey_line_directive: warn_category
(** Warnings related to unknown line directives. *)
+val wkey_unknown_attribute: warn_category
+(** Warning emitted when an unknown attribute is encountered during parsing. *)
+
(* ************************************************************************* *)
(** {2 Functors for late option registration} *)
(** Kernel_function-related options cannot be registered in this module:
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index 1c409c7b8b8d5250f2261e0ac76bc1bcddb7bf68..f1d560d2ec8f2afd8b0e87c23acde891715ed8b9 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -10,7 +10,6 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-#pragma JessieIntegerModel(math)
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int End = 0; */
diff --git a/src/plugins/aorai/tests/ya/test_recursion4.c b/src/plugins/aorai/tests/ya/test_recursion4.c
index 41119f495f30894fc53a67bbb0e92c0b61f8d447..50fa5a5713023696f3a7db04378f3714f626b53a 100644
--- a/src/plugins/aorai/tests/ya/test_recursion4.c
+++ b/src/plugins/aorai/tests/ya/test_recursion4.c
@@ -2,8 +2,6 @@
STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance
*/
-# pragma JessieIntegerModel(math)
-
/*@ requires \valid(t+(0..size-1));
@ requires size>=0;
@ decreases size;
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
index 07ec57256901d02d302a3a43f0054de5871f1f90..12f588bbe0ea457a708f75922d2d40a1e8a7ff78 100644
--- a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
+++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c
@@ -36,7 +36,7 @@ extern size_t __e_acsl_heap_allocation_size;
extern size_t __e_acsl_heap_allocated_blocks;
-/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+/*@ ghost extern int __fc_heap_status; */
/*@ ghost extern int __e_acsl_init; */
diff --git a/src/plugins/variadic/format_parser.ml b/src/plugins/variadic/format_parser.ml
index 900f7c0e9a9c1dc6eb590a06c711c1840975c9cd..a4ec4e75992e0b1d81020e7e6c6eb1b79bbe028a 100644
--- a/src/plugins/variadic/format_parser.ml
+++ b/src/plugins/variadic/format_parser.ml
@@ -55,13 +55,13 @@ let check_flag spec flag =
pp_cs (spec.f_conversion_specifier,spec.f_capitalize);
raise Invalid_format
-let check_cs_compatibility cs capitalized has_field_width has_precision =
+let check_cs_compatibility cs capitalized ~field_width ~precision =
match cs with
- | (`n | `c | `p) as cs when has_precision ->
+ | (`n | `c | `p) as cs when precision <> None ->
warn "Conversion specifier %a does not expect a precision."
pp_cs (cs, capitalized) ;
raise Invalid_format
- | `n when has_field_width ->
+ | `n when field_width <> None ->
warn "Conversion specifier n does not expect a field width.";
raise Invalid_format
| _ -> ()
@@ -83,7 +83,7 @@ let find_typedef : Format_typer.typdef_finder =
let check_f_specification spec =
(* Check the correctness of precision and field width fields *)
check_cs_compatibility spec.f_conversion_specifier spec.f_capitalize
- (spec.f_precision <> None) (spec.f_field_width <> None);
+ ~field_width:spec.f_field_width ~precision:spec.f_precision;
(* Check the combination of conversion specifier and length modifier *)
begin
try ignore (Format_typer.type_f_specifier ~find_typedef spec)
@@ -102,7 +102,7 @@ let check_f_specification spec =
let check_s_specification spec =
(* Check the correctness of field width *)
check_cs_compatibility spec.s_conversion_specifier false
- false (spec.s_field_width <> None);
+ ~field_width:spec.s_field_width ~precision:None;
(* Check the combination of conversion specifier and length modifier *)
begin
try ignore (Format_typer.type_s_specifier ~find_typedef spec)
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 898a29b51911c3b5427d6035edd1ddecef844211..3114385ff210de5416b61b90fa5a4082dfd9c4fc 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -88,6 +88,14 @@
Translating call to printf to a call to the specialized version printf_va_27.
[variadic] printf.c:75:
Translating call to printf to a call to the specialized version printf_va_28.
+[variadic] printf.c:77:
+ Translating call to printf to a call to the specialized version printf_va_29.
+[variadic] printf.c:78:
+ Translating call to printf to a call to the specialized version printf_va_30.
+[variadic] printf.c:79:
+ Translating call to printf to a call to the specialized version printf_va_31.
+[variadic] printf.c:80:
+ Translating call to printf to a call to the specialized version printf_va_32.
[eva] Analyzing a complete application starting at main
[eva] using specification for function printf_va_1
[eva] using specification for function printf_va_2
@@ -128,6 +136,10 @@
Ignoring.
[eva] using specification for function printf_va_27
[eva] using specification for function printf_va_28
+[eva] using specification for function printf_va_29
+[eva] using specification for function printf_va_30
+[eva] using specification for function printf_va_31
+[eva] using specification for function printf_va_32
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_initial_stdout.__fc_FILE_id ∈ {1}
@@ -607,6 +619,60 @@ int printf_va_27(char const * restrict format, int param0, char *param1);
*/
int printf_va_28(char const * restrict format, char *param0);
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param1),
+ (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param1, param0;
+ */
+int printf_va_29(char const * restrict format, int param0, int param1);
+
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param0;
+ */
+int printf_va_30(char const * restrict format, int param0);
+
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param1),
+ (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param1, param0;
+ */
+int printf_va_31(char const * restrict format, int param0, void *param1);
+
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param0;
+ */
+int printf_va_32(char const * restrict format, void *param0);
+
int main(void)
{
int __retres;
@@ -664,6 +730,10 @@ int main(void)
char hashes[4] = {(char)'#', (char)'#', (char)'#', (char)'#'};
printf("%.*s",4,hashes); /* printf_va_27 */
printf("%.4s",hashes); /* printf_va_28 */
+ printf("%*c",4,'#'); /* printf_va_29 */
+ printf("%4c",'#'); /* printf_va_30 */
+ printf("%*p",20,(void *)string); /* printf_va_31 */
+ printf("%20p",(void *)string); /* printf_va_32 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
index 3b3929047d11a5d489a49ad7de293a5586bc3721..114680f3b2c15b14a2349dffbbf158f28c2745b2 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
@@ -20,16 +20,19 @@
Translating call to scanf to a call to the specialized version scanf_va_1.
[variadic] scanf.c:15:
Translating call to scanf to a call to the specialized version scanf_va_2.
-[variadic] scanf.c:23: Warning:
+[variadic] scanf.c:17:
+ Translating call to scanf to a call to the specialized version scanf_va_3.
+[variadic] scanf.c:25: Warning:
Unable to find type intmax_t in the source code which should be used in this call:
no specification will be generated.
Note that due to cleanup, the type may have been defined in the original code but not used anywhere.
Did you include <stdint.h> ?
-[variadic] scanf.c:23:
+[variadic] scanf.c:25:
Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] using specification for function scanf_va_1
[eva] using specification for function scanf_va_2
+[eva] using specification for function scanf_va_3
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
c[0] ∈ [--..--]
@@ -87,6 +90,23 @@ int scanf_va_1(char const * restrict format, char *param0, char *param1,
*/
int scanf_va_2(char const * restrict format, wchar_t *param0);
+/*@ requires \valid(param0);
+ requires valid_read_string(format);
+ ensures \initialized(param0);
+ assigns \result, __fc_stdin->__fc_FILE_data, *param0;
+ assigns \result
+ \from (indirect: __fc_stdin->__fc_FILE_id),
+ (indirect: __fc_stdin->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdin->__fc_FILE_data
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int scanf_va_3(char const * restrict format, char *param0);
+
int main(void)
{
int __retres;
@@ -95,6 +115,7 @@ int main(void)
wchar_t wc;
scanf("Hello %*10le %% %10s %[^]world] %d !",c,c,& i); /* scanf_va_1 */
scanf("%lc",& wc); /* scanf_va_2 */
+ scanf("%1c",c); /* scanf_va_3 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
index 44221e5bb220b87e06bf9640fb09e6404e660fd3..b9054e59855e5ae39fa5be8b102f0db362b083c8 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
@@ -20,11 +20,14 @@
Translating call to scanf to a call to the specialized version scanf_va_1.
[variadic] scanf.c:15:
Translating call to scanf to a call to the specialized version scanf_va_2.
-[variadic] scanf.c:23:
+[variadic] scanf.c:17:
Translating call to scanf to a call to the specialized version scanf_va_3.
+[variadic] scanf.c:25:
+ Translating call to scanf to a call to the specialized version scanf_va_4.
[eva] Analyzing a complete application starting at main
[eva] using specification for function scanf_va_1
[eva] using specification for function scanf_va_2
+[eva] using specification for function scanf_va_3
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
c[0] ∈ [--..--]
@@ -83,6 +86,23 @@ int scanf_va_1(char const * restrict format, char *param0, char *param1,
*/
int scanf_va_2(char const * restrict format, wchar_t *param0);
+/*@ requires \valid(param0);
+ requires valid_read_string(format);
+ ensures \initialized(param0);
+ assigns \result, __fc_stdin->__fc_FILE_data, *param0;
+ assigns \result
+ \from (indirect: __fc_stdin->__fc_FILE_id),
+ (indirect: __fc_stdin->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdin->__fc_FILE_data
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int scanf_va_3(char const * restrict format, char *param0);
+
int main(void)
{
int __retres;
@@ -91,6 +111,7 @@ int main(void)
wchar_t wc;
scanf("Hello %*10le %% %10s %[^]world] %d !",c,c,& i); /* scanf_va_1 */
scanf("%lc",& wc); /* scanf_va_2 */
+ scanf("%1c",c); /* scanf_va_3 */
__retres = 0;
return __retres;
}
@@ -110,12 +131,12 @@ int main(void)
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_3(char const * restrict format, intmax_t *param0);
+int scanf_va_4(char const * restrict format, intmax_t *param0);
void warn_about_intmax_t(void)
{
int i;
- scanf("%jd",(intmax_t *)(& i)); /* scanf_va_3 */
+ scanf("%jd",(intmax_t *)(& i)); /* scanf_va_4 */
return;
}
diff --git a/src/plugins/variadic/tests/known/printf.c b/src/plugins/variadic/tests/known/printf.c
index 40fab6d3a0315cb72f91b901d9f25b2776840251..f86aee3a7b487465287fab3aac024251c32427db 100644
--- a/src/plugins/variadic/tests/known/printf.c
+++ b/src/plugins/variadic/tests/known/printf.c
@@ -73,4 +73,9 @@ int main()
char hashes[4] = "####"; // no terminator
printf("%.*s", 4, hashes); // ok
printf("%.4s", hashes); // ok
+
+ printf("%*c", 4, '#'); // ok
+ printf("%4c", '#'); // ok
+ printf("%*p", 20, (void*)string); // ok
+ printf("%20p", (void*)string); // ok
}
diff --git a/src/plugins/variadic/tests/known/scanf.c b/src/plugins/variadic/tests/known/scanf.c
index 8943f82294f5e5a0788c4afae166afa62b3e5f13..1103ba84422d3415da2cc72802a0a247cc1112b0 100644
--- a/src/plugins/variadic/tests/known/scanf.c
+++ b/src/plugins/variadic/tests/known/scanf.c
@@ -13,6 +13,8 @@ int main(){
wchar_t wc;
scanf("%lc", &wc);
+
+ scanf("%1c", c);
}
#ifdef INCLUDE_STDINT
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index cef88c1792d677a1e561e2d333f8dc87b706ce1d..1df501071d74944707e32f4d67be6823641387b8 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -559,7 +559,8 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
| AVariant(term, Some rel) ->
let vrel = mk_variant_relation_property kf stmt ca term rel in
let vrel = variant_as_inv ~loc:term.term_loc vrel in
- { l with loop_invariants = vrel :: l.loop_invariants }
+ { l with loop_terminates = None ;
+ loop_invariants = vrel :: l.loop_invariants }
| AAssigns(_,WritesAny) ->
let asgn = WpPropId.mk_loop_any_assigns_info stmt in
{ l with loop_assigns = asgn :: l.loop_assigns }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index c46c9b16648666e10a5d4cd3f7ce7900788baab0..aa2050b9a6681883284ee7219136c47957e6f710 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -7,20 +7,25 @@
[kernel:annot:missing-spec] terminates_formulae.i:41: Warning:
Neither code nor explicit exits for function call_param,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] terminates_formulae.i:97: Warning:
+[kernel:annot:missing-spec] terminates_formulae.i:71: Warning:
+ Neither code nor specification for function with_call,
+ generating default exits, assigns and terminates. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] terminates_formulae.i:109: Warning:
Neither code nor explicit exits for function local_init_P,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:84: Warning:
+[wp:hypothesis] terminates_formulae.i:96: Warning:
'Rel' relation must be well-founded
[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [Valid] Goal general_variant_exits (Cfg) (Unreachable)
[wp] [Valid] Goal general_variant_terminates (Cfg) (Trivial)
+[wp:hypothesis] terminates_formulae.i:76: Warning:
+ 'Rel' relation must be well-founded
[wp] [Valid] Goal no_variant_exits (Cfg) (Unreachable)
[wp] [Valid] Goal variant_exits (Cfg) (Unreachable)
[wp] [Valid] Goal variant_terminates (Cfg) (Trivial)
-[wp] terminates_formulae.i:91: Warning:
+[wp] terminates_formulae.i:103: Warning:
Missing decreases clause on recursive function no_decreases, call must be unreachable
------------------------------------------------------------
Function base_call
@@ -106,7 +111,7 @@ Prove: true.
Function decreases
------------------------------------------------------------
-Goal Termination-condition (file terminates_formulae.i, line 77) in 'decreases':
+Goal Termination-condition (file terminates_formulae.i, line 89) in 'decreases':
Prove: true.
------------------------------------------------------------
@@ -117,7 +122,7 @@ Prove: true.
------------------------------------------------------------
Goal Recursion variant:
-Call decreases at line 80
+Call decreases at line 92
Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
@@ -126,7 +131,7 @@ Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
Function general_decreases
------------------------------------------------------------
-Goal Termination-condition (file terminates_formulae.i, line 83) in 'general_decreases':
+Goal Termination-condition (file terminates_formulae.i, line 95) in 'general_decreases':
Prove: true.
------------------------------------------------------------
@@ -137,7 +142,7 @@ Prove: true.
------------------------------------------------------------
Goal Recursion variant:
-Call decreases at line 86
+Call decreases at line 98
Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
Prove: P_Rel(n, to_uint32(n - 1)).
@@ -155,13 +160,37 @@ Goal Follows relation Loop variant at loop (file terminates_formulae.i, line 68)
Assume { Type: is_uint32(x). (* Goal *) When: P_Q. (* Then *) Have: 0 < x. }
Prove: P_Rel(x, to_uint32(x - 1)).
+------------------------------------------------------------
+------------------------------------------------------------
+ Function general_variant_call
+------------------------------------------------------------
+
+Goal Termination-condition (file terminates_formulae.i, line 73) in 'general_variant_call':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Exit-condition (generated) in 'general_variant_call':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file terminates_formulae.i, line 75):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Follows relation Loop variant at loop (file terminates_formulae.i, line 77):
+Assume { Type: is_uint32(x). (* Goal *) When: P_Q. (* Then *) Have: 0 < x. }
+Prove: P_Rel(x, to_uint32(x - 1)).
+
------------------------------------------------------------
------------------------------------------------------------
Function local_init_call
------------------------------------------------------------
-Goal Termination-condition (file terminates_formulae.i, line 99) in 'local_init_call':
-Call terminates at line 101
+Goal Termination-condition (file terminates_formulae.i, line 111) in 'local_init_call':
+Call terminates at line 113
Assume { (* Heap *) Type: is_sint32(a). (* Goal *) When: P_Q. }
Prove: P_P(a).
@@ -175,13 +204,13 @@ Prove: true.
Function no_decreases
------------------------------------------------------------
-Goal Termination-condition (file terminates_formulae.i, line 89) in 'no_decreases' (1/2):
+Goal Termination-condition (file terminates_formulae.i, line 101) in 'no_decreases' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Termination-condition (file terminates_formulae.i, line 89) in 'no_decreases' (2/2):
-Call terminates (missing decreases) at line 91
+Goal Termination-condition (file terminates_formulae.i, line 101) in 'no_decreases' (2/2):
+Call terminates (missing decreases) at line 103
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
Prove: !P_Q.
@@ -195,13 +224,13 @@ Prove: true.
Function no_variant
------------------------------------------------------------
-Goal Termination-condition (file terminates_formulae.i, line 71) in 'no_variant':
-Loop termination at line 74
+Goal Termination-condition (file terminates_formulae.i, line 83) in 'no_variant':
+Loop termination at line 86
Prove: !P_Q.
------------------------------------------------------------
-Goal Loop assigns (file terminates_formulae.i, line 73):
+Goal Loop assigns (file terminates_formulae.i, line 85):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index a038c7f3b038b44a135b9aeefde84db24f4b6cba..22b0bc6bbb8e520bfb54ee225af079e8870c955a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -7,22 +7,27 @@
[kernel:annot:missing-spec] terminates_formulae.i:41: Warning:
Neither code nor explicit exits for function call_param,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] terminates_formulae.i:97: Warning:
+[kernel:annot:missing-spec] terminates_formulae.i:71: Warning:
+ Neither code nor specification for function with_call,
+ generating default exits, assigns and terminates. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] terminates_formulae.i:109: Warning:
Neither code nor explicit exits for function local_init_P,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:84: Warning:
+[wp:hypothesis] terminates_formulae.i:96: Warning:
'Rel' relation must be well-founded
[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [Valid] Goal general_variant_exits (Cfg) (Unreachable)
[wp] [Valid] Goal general_variant_terminates (Cfg) (Trivial)
+[wp:hypothesis] terminates_formulae.i:76: Warning:
+ 'Rel' relation must be well-founded
[wp] [Valid] Goal no_variant_exits (Cfg) (Unreachable)
[wp] [Valid] Goal variant_exits (Cfg) (Unreachable)
[wp] [Valid] Goal variant_terminates (Cfg) (Trivial)
-[wp] terminates_formulae.i:91: Warning:
+[wp] terminates_formulae.i:103: Warning:
Missing decreases clause on recursive function no_decreases, call must be unreachable
-[wp] 28 goals scheduled
+[wp] 32 goals scheduled
[wp] [Unsuccess] typed_base_call_terminates (Alt-Ergo) (Cached)
[wp] [Valid] typed_base_call_exits (Qed)
[wp] [Valid] typed_call_same_terminates (Qed)
@@ -38,6 +43,10 @@
[wp] [Valid] typed_variant_loop_variant_positive (Qed)
[wp] [Valid] typed_general_variant_loop_assigns (Qed)
[wp] [Valid] typed_general_variant_loop_variant_relation (Alt-Ergo) (Cached)
+[wp] [Valid] typed_general_variant_call_terminates (Qed)
+[wp] [Valid] typed_general_variant_call_exits (Qed)
+[wp] [Valid] typed_general_variant_call_loop_assigns (Qed)
+[wp] [Valid] typed_general_variant_call_loop_variant_relation (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_no_variant_terminates (Alt-Ergo) (Cached)
[wp] [Valid] typed_no_variant_loop_assigns (Qed)
[wp] [Valid] typed_decreases_terminates (Qed)
@@ -51,11 +60,11 @@
[wp] [Valid] typed_no_decreases_exits (Qed)
[wp] [Unsuccess] typed_local_init_call_terminates (Alt-Ergo) (Cached)
[wp] [Valid] typed_local_init_call_exits (Qed)
-[wp] Proved goals: 27 / 33
+[wp] Proved goals: 31 / 37
Terminating: 2
Unreachable: 3
- Qed: 18
- Alt-Ergo: 4
+ Qed: 21
+ Alt-Ergo: 5
Unsuccess: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -66,6 +75,7 @@
call_param_change 1 - 2 50.0%
variant 2 1 3 100%
general_variant 1 1 2 100%
+ general_variant_call 3 1 4 100%
no_variant 1 - 2 50.0%
decreases 2 1 3 100%
general_decreases 2 1 3 100%
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_formulae.i b/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
index fb8079e4da7d2e18927deb879f13cdb08592f9b0..a4ca1dfabe98f4662b090294fa954af269e1bf37 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
+++ b/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
@@ -68,6 +68,18 @@ void general_variant(unsigned x) {
while (x > 0) x --;
}
+void with_call(void);
+
+//@ terminates Q ;
+void general_variant_call(unsigned x) {
+ /*@ loop assigns x ;
+ loop variant x for Rel; */
+ while (x > 0){
+ with_call();
+ x --;
+ }
+}
+
//@ terminates Q ;
void no_variant(void){
//@ loop assigns i ;
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 42f5dbd8c9e577b60e0897201d64343d212072e5..797055f81dffa3ddfba8b968fa68c8fdfff8742e 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -68,7 +68,8 @@
"typing:implicit-function-declaration", "typing:implicit-int",
"typing:incompatible-pointer-types",
"typing:incompatible-types-call", "typing:inconsistent-specifier",
- "typing:int-conversion", "typing:merge-conversion", "typing:no-proto"
+ "typing:int-conversion", "typing:merge-conversion",
+ "typing:no-proto", "unknown-attribute"
],
"disabled": [
"CERT:EXP:10", "acsl-float-compare", "c11", "file:not-found",
diff --git a/tests/spec/oracle/declspec.res.oracle b/tests/spec/oracle/declspec.res.oracle
index 0c39acb7ee9274d719c0a6485cb188a4ee19c80b..66d927c775cf46b83de750222c4bf863c02e7c31 100644
--- a/tests/spec/oracle/declspec.res.oracle
+++ b/tests/spec/oracle/declspec.res.oracle
@@ -9,7 +9,7 @@
void f(char const * __attribute__((__whatever__)) a,
char * __attribute__((__p__)) b)
{
- /*@ assert p((char *)b); */ ;
+ /*@ assert p(b); */ ;
return;
}
diff --git a/tests/syntax/oracle/array_formals.res.oracle b/tests/syntax/oracle/array_formals.res.oracle
index 11d5e49bbb72f5e451601757eaa698a7bf91c2ac..2e2ce2b7c0c968555ebfacdea42223256a49de31 100644
--- a/tests/syntax/oracle/array_formals.res.oracle
+++ b/tests/syntax/oracle/array_formals.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing array_formals.i (no preprocessing)
+[kernel:unknown-attribute] array_formals.i:7: Warning: Unknown attribute: test
/* Generated by Frama-C */
typedef int ( __attribute__((__test__)) arr)[2];
int f(int a[2])
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle
index d47e7ccfd11e49ed64f6de8d7b1c80aa08d47661..792500d3b81add493063e651e09eed8a040541bd 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.0.res.oracle
@@ -1,8 +1,46 @@
[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
+[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
+ Unknown attribute: tret1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
+ Unknown attribute: f1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
+ Unknown attribute: arg1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
+ Unknown attribute: tret2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
+ Unknown attribute: f2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
+ Unknown attribute: arg2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
+ Unknown attribute: tret3
+[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
+ Unknown attribute: arg3
[kernel] attributes-declarations-definitions.c:12: Warning:
found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
+[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
+ Unknown attribute: tret4
+[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
+ Unknown attribute: f4
+[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
+ Unknown attribute: arg4
[kernel] attributes-declarations-definitions.c:21: Warning:
found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
+[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
+ Unknown attribute: tret5
+[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
+ Unknown attribute: f5
+[kernel:unknown-attribute] attributes-declarations-definitions.c:25: Warning:
+ Unknown attribute: a1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:33: Warning:
+ Unknown attribute: a2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
+ Unknown attribute: p1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
+ Unknown attribute: p2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:56: Warning:
+ Unknown attribute: _n
+[kernel:unknown-attribute] attributes-declarations-definitions.c:58: Warning:
+ Unknown attribute: e_
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
@@ -19,18 +57,14 @@ int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3)
{
- int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
- __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
- return __retres;
+ return p3;
}
aint g(int __attribute__((__a2__)) i3);
aint g(int __attribute__((__a2__)) i3)
{
- aint __retres;
- __retres = (aint)i3;
- return __retres;
+ return i3;
}
iptr h(iptr volatile ip2);
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle
index 0b83c35f45ab5fb43425845f8807646ed441895c..42b10c3a1cd7a4fd93316eaea4bc15b6d6cd8fdd 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.1.res.oracle
@@ -1,8 +1,46 @@
[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
+[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
+ Unknown attribute: tret1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
+ Unknown attribute: f1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
+ Unknown attribute: arg1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
+ Unknown attribute: tret2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
+ Unknown attribute: f2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
+ Unknown attribute: arg2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
+ Unknown attribute: tret3
+[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
+ Unknown attribute: arg3
[kernel] attributes-declarations-definitions.c:12: Warning:
found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
+[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
+ Unknown attribute: tret4
+[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
+ Unknown attribute: f4
+[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
+ Unknown attribute: arg4
[kernel] attributes-declarations-definitions.c:21: Warning:
found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
+[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
+ Unknown attribute: tret5
+[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
+ Unknown attribute: f5
+[kernel:unknown-attribute] attributes-declarations-definitions.c:25: Warning:
+ Unknown attribute: a1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:33: Warning:
+ Unknown attribute: a2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
+ Unknown attribute: p1
+[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
+ Unknown attribute: p2
+[kernel:unknown-attribute] attributes-declarations-definitions.c:56: Warning:
+ Unknown attribute: _n
+[kernel:unknown-attribute] attributes-declarations-definitions.c:58: Warning:
+ Unknown attribute: e_
[kernel] attributes-declarations-definitions.c:62: User Error:
unsupported attribute: vector_size
[kernel] User Error: stopping on file "attributes-declarations-definitions.c" that has errors. Add
diff --git a/tests/syntax/oracle/inline_calls.0.res.oracle b/tests/syntax/oracle/inline_calls.0.res.oracle
index 18da0e0c968c55fdbf22e7452c0f5d4c758bee6f..850888712b55f3e969b9a097ca2f69a2ba259cfc 100644
--- a/tests/syntax/oracle/inline_calls.0.res.oracle
+++ b/tests/syntax/oracle/inline_calls.0.res.oracle
@@ -23,7 +23,8 @@ int g(void)
if (v) {
int tmp;
{
- /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
+ /* __blockattribute__(__fc_inlined__("f")) */
+ int __retres_5;
__retres_5 = 2;
tmp = __retres_5;
}
@@ -33,7 +34,8 @@ int g(void)
else {
int tmp_0;
{
- /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */int __retres_6;
+ /* __blockattribute__(__fc_inlined__("in_f__fc_inline")) */
+ int __retres_6;
__retres_6 = 3;
tmp_0 = __retres_6;
}
@@ -47,11 +49,13 @@ int h(void)
{
int tmp;
{
- /* __blockattribute__(____fc_inlined__("g")) */int __retres;
+ /* __blockattribute__(__fc_inlined__("g")) */
+ int __retres;
if (v) {
int tmp_3;
{
- /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
+ /* __blockattribute__(__fc_inlined__("f")) */
+ int __retres_5;
__retres_5 = 2;
tmp_3 = __retres_5;
}
@@ -61,7 +65,7 @@ int h(void)
else {
int tmp_0;
{
- /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */
+ /* __blockattribute__(__fc_inlined__("in_f__fc_inline")) */
int __retres_6;
__retres_6 = 3;
tmp_0 = __retres_6;
@@ -91,8 +95,9 @@ int rec(int x_0)
goto return_label;
}
{
- /* __blockattribute__(____fc_inlined__("rec")) */int __retres_7;
- int tmp_6;
+ /* __blockattribute__(__fc_inlined__("rec")) */
+ int __retres_7;
+ int tmp_6;
int x_0_5 = x_0 - 1;
if (x_0_5 < 0) {
__retres_7 = x_0_5;
@@ -117,7 +122,8 @@ int f1(int a)
if (nondet) {
int __inline_tmp;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5 = 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */
+ int a_5 = 1;
if (nondet) g1(4);
__inline_tmp = a_5;
}
@@ -126,12 +132,14 @@ int f1(int a)
if (nondet) {
int __inline_tmp_6;
{
- /* __blockattribute__(____fc_inlined__("f1")) */int __retres_9;
+ /* __blockattribute__(__fc_inlined__("f1")) */
+ int __retres_9;
int a_8 = 2;
if (nondet) {
int __inline_tmp_10;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5_11 = 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */
+ int a_5_11 = 1;
if (nondet) g1(4);
__inline_tmp_10 = a_5_11;
}
@@ -156,7 +164,8 @@ int g1(int a)
if (nondet) {
int __inline_tmp;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_4 = 4;
+ /* __blockattribute__(__fc_inlined__("g1")) */
+ int a_4 = 4;
if (nondet) {
int __inline_tmp_5;
g1(4);
@@ -174,23 +183,26 @@ int main(void)
int __inline_tmp;
int tmp_1;
{
- /* __blockattribute__(____fc_inlined__("i")) */int __retres;
+ /* __blockattribute__(__fc_inlined__("i")) */
+ int __retres;
/*@ assert i: \true; */ ;
__retres = 0;
__inline_tmp = __retres;
}
int local_init = __inline_tmp;
{
- /* __blockattribute__(____fc_inlined__("rec")) */int __retres_10;
- int tmp;
+ /* __blockattribute__(__fc_inlined__("rec")) */
+ int __retres_10;
+ int tmp;
int x_0 = local_init;
if (x_0 < 0) {
__retres_10 = x_0;
goto return_label;
}
{
- /* __blockattribute__(____fc_inlined__("rec")) */int __retres_7;
- int tmp_6;
+ /* __blockattribute__(__fc_inlined__("rec")) */
+ int __retres_7;
+ int tmp_6;
int x_0_5 = x_0 - 1;
if (x_0_5 < 0) {
__retres_7 = x_0_5;
@@ -205,12 +217,14 @@ int main(void)
}
int t = __inline_tmp_8;
{
- /* __blockattribute__(____fc_inlined__("f1")) */int __retres_13;
+ /* __blockattribute__(__fc_inlined__("f1")) */
+ int __retres_13;
int a = 2;
if (nondet) {
int __inline_tmp_14;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5 = 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */
+ int a_5 = 1;
if (nondet) g1(4);
__inline_tmp_14 = a_5;
}
@@ -219,13 +233,14 @@ int main(void)
if (nondet) {
int __inline_tmp_6;
{
- /* __blockattribute__(____fc_inlined__("f1")) */int __retres_9;
+ /* __blockattribute__(__fc_inlined__("f1")) */
+ int __retres_9;
int a_8 = 2;
if (nondet) {
int __inline_tmp_10;
{
- /* __blockattribute__(____fc_inlined__("g1")) */int a_5_11 =
- 1;
+ /* __blockattribute__(__fc_inlined__("g1")) */
+ int a_5_11 = 1;
if (nondet) g1(4);
__inline_tmp_10 = a_5_11;
}
@@ -245,13 +260,16 @@ int main(void)
__inline_tmp_11 = __retres_13;
}
{
- /* __blockattribute__(____fc_inlined__("h")) */int tmp_15;
+ /* __blockattribute__(__fc_inlined__("h")) */
+ int tmp_15;
{
- /* __blockattribute__(____fc_inlined__("g")) */int __retres_16;
+ /* __blockattribute__(__fc_inlined__("g")) */
+ int __retres_16;
if (v) {
int tmp_3;
{
- /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
+ /* __blockattribute__(__fc_inlined__("f")) */
+ int __retres_5;
__retres_5 = 2;
tmp_3 = __retres_5;
}
@@ -261,7 +279,7 @@ int main(void)
else {
int tmp_0;
{
- /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */
+ /* __blockattribute__(__fc_inlined__("in_f__fc_inline")) */
int __retres_6;
__retres_6 = 3;
tmp_0 = __retres_6;
@@ -289,7 +307,8 @@ int call_with_static(void)
{
int tmp;
{
- /* __blockattribute__(____fc_inlined__("with_static")) */with_static_count ++;
+ /* __blockattribute__(__fc_inlined__("with_static")) */
+ with_static_count ++;
tmp = with_static_count;
}
return tmp;
@@ -305,8 +324,8 @@ void builtin_acsl(void)
void call_builtin_acsl(void)
{
{
- /* __blockattribute__(____fc_inlined__("builtin_acsl")) */float g_0 =
- 0.f;
+ /* __blockattribute__(__fc_inlined__("builtin_acsl")) */
+ float g_0 = 0.f;
/*@ assert ¬\is_NaN(g_0); */ ;
;
}
@@ -322,9 +341,8 @@ void f_slevel(void)
void call_f_slevel(void)
{
{
- /* __blockattribute__(____fc_inlined__("f_slevel")) *//*@
- \eva::slevel 0; */
- ;
+ /* __blockattribute__(__fc_inlined__("f_slevel")) */
+ /*@ \eva::slevel 0; */ ;
;
}
return;
@@ -341,7 +359,8 @@ void post_decl(void);
void middle_decl(void)
{
{
- /* __blockattribute__(____fc_inlined__("pre_decl")) */x ++;
+ /* __blockattribute__(__fc_inlined__("pre_decl")) */
+ x ++;
y ++;
post_decl();
;
diff --git a/tests/syntax/oracle/osx_attribute.res.oracle b/tests/syntax/oracle/osx_attribute.res.oracle
index 0f3d989cd41c02e56b329c4a5f530751358dfbf8..d798db731f67b077fe519ba03a2c6cd13b274563 100644
--- a/tests/syntax/oracle/osx_attribute.res.oracle
+++ b/tests/syntax/oracle/osx_attribute.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing osx_attribute.i (no preprocessing)
+[kernel:unknown-attribute] osx_attribute.i:1: Warning:
+ Unknown attribute: availability
/* Generated by Frama-C */
void f(void) __attribute__((__availability__(macos,introduced=10.4,deprecated=10.6,obsoleted=10.7)));
diff --git a/tests/value/oracle/const_typedef.res.oracle b/tests/value/oracle/const_typedef.res.oracle
index ff88e007c15aa42a5ab6064ac1a68abbab1726bd..08036b1ec9ea59f2ae52cd2081d3774a9f9a032a 100644
--- a/tests/value/oracle/const_typedef.res.oracle
+++ b/tests/value/oracle/const_typedef.res.oracle
@@ -1,4 +1,9 @@
[kernel] Parsing const_typedef.i (no preprocessing)
+[kernel:unknown-attribute] const_typedef.i:9: Warning: Unknown attribute: BLA
+[kernel:unknown-attribute] const_typedef.i:10: Warning: Unknown attribute: BLA
+[kernel:unknown-attribute] const_typedef.i:11: Warning: Unknown attribute: BLA
+[kernel:unknown-attribute] const_typedef.i:12: Warning: Unknown attribute: BLA
+[kernel:unknown-attribute] const_typedef.i:19: Warning: Unknown attribute: BLA
/* Generated by Frama-C */
typedef int INT[3][3];
typedef int INT3[2][7];
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index 8af4494c8c1d3f713fd45c9f8d299c4a2593d442..1ebd46de9fa932b0224854b1a5a41b036281e4d0 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -1,4 +1,12 @@
[kernel] Parsing period.c (with preprocessing)
+[kernel:unknown-attribute] period.c:4: Warning:
+ Unknown attribute: Frama_C_periodic
+[kernel:unknown-attribute] period.c:13: Warning:
+ Unknown attribute: Frama_C_periodic
+[kernel:unknown-attribute] period.c:14: Warning:
+ Unknown attribute: Frama_C_periodic
+[kernel:unknown-attribute] period.c:15: Warning:
+ Unknown attribute: Frama_C_periodic
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/oracle_equality/period.res.oracle b/tests/value/oracle_equality/period.res.oracle
index 54f6fc44b0d4c8cf5be9e39d50eb248bd42f4eeb..d63f5c7de17ca306c120bb86c38d2e4c07729652 100644
--- a/tests/value/oracle_equality/period.res.oracle
+++ b/tests/value/oracle_equality/period.res.oracle
@@ -1,10 +1,10 @@
-88,92d87
+96,100d95
< [eva:alarm] period.c:53: Warning:
< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
< [eva:garbled-mix:write] period.c:53:
< Assigning imprecise value to p because of arithmetic operation on addresses.
< [eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
-102,105d96
+110,113d104
< period.c:53: arithmetic operation on addresses
< (read in 1 statement, propagated through 1 statement) garbled mix of &
< {g}