diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Cutil.ml | 10 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 4 | ||||
| -rw-r--r-- | cparser/Diagnostics.ml | 8 | ||||
| -rw-r--r-- | cparser/Diagnostics.mli | 1 | ||||
| -rw-r--r-- | cparser/Parse.ml | 2 | ||||
| -rw-r--r-- | cparser/Rename.ml | 2 |
6 files changed, 24 insertions, 3 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 71c253f8..30037049 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -707,6 +707,11 @@ let is_integer_type env t = | TEnum(_, _) -> true | _ -> false +let is_float_type env t = + match unroll env t with + | TFloat (_, _) -> true + | _ -> false + let is_arith_type env t = match unroll env t with | TInt(_, _) -> true @@ -1207,3 +1212,8 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } + +let is_volatile_variable env exp = + match exp.edesc with + | EVar x -> List.mem AVolatile (attributes_of_type env exp.etyp) + | _ -> false diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 79975dcf..87a69f12 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -141,6 +141,8 @@ val is_void_type : Env.t -> typ -> bool (* Is type [void]? *) val is_integer_type : Env.t -> typ -> bool (* Is type integer? *) +val is_float_type : Env.t -> typ -> bool + (* Is type float *) val is_arith_type : Env.t -> typ -> bool (* Is type integer or float? *) val is_pointer_type : Env.t -> typ -> bool @@ -239,6 +241,8 @@ val field_of_arrow_access: Env.t -> typ -> string -> field (* Return the field info for a [x->field] access *) val valid_array_size: Env.t -> typ -> int64 -> bool (* Test whether the array size fits in half of the address space *) +val is_volatile_variable: Env.t -> exp -> bool + (* Test whether the expression is an access to a volatile variable *) (* Constructors *) diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index fbdc9297..e3258a38 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -90,6 +90,7 @@ type warning_type = | Inline_asm_sdump | Unused_variable | Unused_parameter + | Wrong_ais_parameter (* List of active warnings *) let active_warnings: warning_type list ref = ref [ @@ -110,6 +111,7 @@ let active_warnings: warning_type list ref = ref [ Return_type; Literal_range; Inline_asm_sdump; + Wrong_ais_parameter; ] (* List of errors treated as warning *) @@ -139,6 +141,7 @@ let string_of_warning = function | Inline_asm_sdump -> "inline-asm-sdump" | Unused_variable -> "unused-variable" | Unused_parameter -> "unused-parameter" + | Wrong_ais_parameter -> "wrong-ais-parameter" (* Activate the given warning *) let activate_warning w () = @@ -184,7 +187,8 @@ let wall () = CompCert_conformance; Inline_asm_sdump; Unused_variable; - Unused_parameter + Unused_parameter; + Wrong_ais_parameter; ] let wnothing () = @@ -214,6 +218,7 @@ let werror () = CompCert_conformance; Inline_asm_sdump; Unused_variable; + Wrong_ais_parameter; ] (* Generate the warning key for the message *) @@ -390,6 +395,7 @@ let warning_options = error_option Inline_asm_sdump @ error_option Unused_variable @ error_option Unused_parameter @ + error_option Wrong_ais_parameter @ [Exact ("-Wfatal-errors"), Set error_fatal; Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) Exact ("-fno-diagnostics-color"), Unset color_diagnostics; diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index 82edd9fa..648d537b 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -47,6 +47,7 @@ type warning_type = | Inline_asm_sdump (** inline assembler used in combination of sdump *) | Unused_variable (** unused local variables *) | Unused_parameter (** unused function parameter *) + | Wrong_ais_parameter (** wrong parameter type for ais replacement *) val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 8143954b..b2c83698 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -69,7 +69,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing" + Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing" | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index cdb5751e..d63fa47d 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -84,7 +84,7 @@ let ident env id = IdentMap.find id env.re_id with Not_found -> Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound" - id.name id.stamp + id.name id.stamp let rec typ env = function | TPtr(ty, a) -> TPtr(typ env ty, a) |