diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 9c4a3b5306acdf51c56a02afc958a2132237bf28..31065775b513da7b9bb861c01a9eeef1b47b9101 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1113,13 +1113,15 @@ module LogicalOperators =
let () = Parameter_customize.set_group normalisation
let () = Parameter_customize.do_not_reset_on_copy ()
module Enums =
- P.Empty_string
+ P.String
(struct
let option_name = "-enums"
let arg_name = "repr"
+ let default = "gcc-enums"
let help =
"use <repr> to decide how enumerated types should be represented. \
- -enums help gives the list of available representations"
+ -enums help gives the list of available representations (default: "
+ ^ default ^ ")"
end)
let enum_reprs = ["gcc-enums"; "gcc-short-enums"; "int";]
let () = Enums.set_possible_values ("help"::enum_reprs)
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index af4fefa77c6ff1afd14bbe039b0a338210481b10..d5b98d5d1d192291de971216ec7783223cba3101 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -72,21 +72,35 @@ let is_extended_integer_type t =
| TNamed (ti, _) -> List.mem ti.tname extended_integer_typenames
| _ -> false
+let integral_rep ikind =
+ Cil.bitsSizeOfInt ikind, Cil.isSigned ikind
+
+let expose t =
+ Cil.type_remove_attributes_for_c_cast (Cil.unrollType t)
+
+(* From most permissive to least permissive *)
+type castability = Strict (* strictly allowed by the C standard *)
+ | Tolerated (* tolerated in practice *)
+ | NonPortable (* non-portable minor deviation *)
+ | NonStrict (* only allowed in non-strict mode *)
+ | Never (* never allowed *)
+
let can_cast given expected =
- let integral_rep ikind =
- Cil.bitsSizeOfInt ikind, Cil.isSigned ikind
- and expose t =
- Cil.type_remove_attributes_for_c_cast (Cil.unrollType t)
- in
match expose given, expose expected with
+ | t1, t2 when Cil_datatype.Typ.equal t1 t2 -> Strict
| (TInt (i1,a1) | TEnum({ekind=i1},a1)),
- (TInt (i2,a2) | TEnum({ekind=i2},a2))
- when not (Strict.get ()) || is_extended_integer_type given ->
- integral_rep i1 = integral_rep i2 &&
- Cil_datatype.Attributes.equal a1 a2
- | TPtr _, TPtr _ -> true
- | exposed_given, exposed_expected ->
- Cil_datatype.Typ.equal exposed_given exposed_expected
+ (TInt (i2,a2) | TEnum({ekind=i2},a2)) ->
+ if integral_rep i1 <> integral_rep i2 ||
+ not (Cil_datatype.Attributes.equal a1 a2) then
+ Never
+ else if is_extended_integer_type given then
+ Tolerated
+ else if i1 = i2 then
+ NonPortable
+ else
+ NonStrict
+ | TPtr _, TPtr _ -> Strict
+ | _, _ -> Never
let does_fit exp typ =
match Cil.constFoldToInt exp, Cil.unrollType typ with
@@ -105,12 +119,22 @@ let pretty_typ fmt t =
(* cast the i-th argument exp to paramtyp *)
let cast_arg i paramtyp exp =
let argtyp = Cil.typeOf exp in
- if not (can_cast argtyp paramtyp) && not (does_fit exp paramtyp) then
- Self.warning ~current:true
- "Incorrect type for argument %d. \
- The argument will be cast from %a to %a."
- (i + 1)
- pretty_typ argtyp pretty_typ paramtyp;
+ if not (does_fit exp paramtyp) then
+ begin match can_cast argtyp paramtyp with
+ | Strict | Tolerated -> ()
+ | (NonPortable | NonStrict) when not (Strict.get ()) -> ()
+ | NonPortable ->
+ Self.warning ~current:true
+ "Possible portability issues with enum type for argument %d \
+ (use -variadic-no-strict to avoid this warning)."
+ (i + 1)
+ | NonStrict | Never ->
+ Self.warning ~current:true
+ "Incorrect type for argument %d. \
+ The argument will be cast from %a to %a."
+ (i + 1)
+ pretty_typ argtyp pretty_typ paramtyp
+ end;
Cil.mkCast ~force:false ~e:exp ~newt:paramtyp
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 0bb2cd97335e2418ef8ddedeb6cfdbf5ae09c1f9..39f1ae9b900ea71a6413863dd6ced0e450a76c99 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -69,7 +69,11 @@
[variadic] tests/known/printf_wrong_types.c:35:
Translating call to printf to a call to the specialized version printf_va_15.
[variadic] tests/known/printf_wrong_types.c:35: Warning:
- Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to unsigned int.
+ Possible portability issues with enum type for argument 2 (use -variadic-no-strict to avoid this warning).
+[variadic] tests/known/printf_wrong_types.c:36:
+ Translating call to printf to a call to the specialized version printf_va_16.
+[variadic] tests/known/printf_wrong_types.c:36: Warning:
+ Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to int.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -298,6 +302,19 @@ int printf_va_14(char const * __restrict format, int param0);
*/
int printf_va_15(char const * __restrict format, unsigned int param0);
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ 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_16(char const * __restrict format, int param0);
+
int main(void)
{
int __retres;
@@ -325,6 +342,7 @@ int main(void)
printf_va_14("%d",(int)string);
RC rc = OK;
printf_va_15("%u",rc);
+ printf_va_16("%d",(int)rc);
__retres = 0;
return __retres;
}
@@ -386,6 +404,7 @@ int main(void)
printf("%d",string);
RC rc = OK;
printf("%u",rc);
+ printf("%d",rc);
__retres = 0;
return __retres;
}
@@ -453,6 +472,10 @@ int main(void)
Incorrect type for argument 2. The argument will be cast from char * to int.
[variadic] tests/known/printf_wrong_types.c:35:
Translating call to printf to a call to the specialized version printf_va_15.
+[variadic] tests/known/printf_wrong_types.c:36:
+ Translating call to printf to a call to the specialized version printf_va_16.
+[variadic] tests/known/printf_wrong_types.c:36: Warning:
+ Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to int.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -681,6 +704,19 @@ int printf_va_14(char const * __restrict format, int param0);
*/
int printf_va_15(char const * __restrict format, unsigned int param0);
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ 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_16(char const * __restrict format, int param0);
+
int main(void)
{
int __retres;
@@ -708,6 +744,7 @@ int main(void)
printf_va_14("%d",(int)string);
RC rc = OK;
printf_va_15("%u",rc);
+ printf_va_16("%d",(int)rc);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/printf_wrong_types.c b/src/plugins/variadic/tests/known/printf_wrong_types.c
index 7b6cdd80e4476bbd983e69f8d3f75d826f34f13a..85cfc9279a4d54d6d5856eb61003896518f8c424 100644
--- a/src/plugins/variadic/tests/known/printf_wrong_types.c
+++ b/src/plugins/variadic/tests/known/printf_wrong_types.c
@@ -32,5 +32,6 @@ int main(){
typedef enum { OK, ERROR } RC;
RC rc = OK;
- printf("%u", rc); // Wrong type (in strict mode)
+ printf("%u", rc); // Correct type with '-enums gcc-enums'
+ printf("%d", rc); // Wrong type (in strict mode)
}