aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-12-14 14:44:25 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-12-14 14:44:25 +0100
commit41ed905f57ec62162aac5be5bd5551b7b753e88d (patch)
treede865e0f9093c03fc764f2194a7f4476c160256f /cparser
parent680444f180c750078a77b0591cd5c19e632612d6 (diff)
downloadcompcert-41ed905f57ec62162aac5be5bd5551b7b753e88d.tar.gz
compcert-41ed905f57ec62162aac5be5bd5551b7b753e88d.zip
Added warning for inline asm in sdump. Bug 20593
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Cerrors.ml6
-rw-r--r--cparser/Cerrors.mli1
2 files changed, 7 insertions, 0 deletions
diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml
index 562d8e89..612980f1 100644
--- a/cparser/Cerrors.ml
+++ b/cparser/Cerrors.ml
@@ -71,6 +71,7 @@ type warning_type =
| Literal_range
| Unknown_pragmas
| CompCert_conformance
+ | Inline_asm_sdump
let active_warnings: warning_type list ref = ref [
Unnamed;
@@ -89,6 +90,7 @@ let active_warnings: warning_type list ref = ref [
Invalid_noreturn;
Return_type;
Literal_range;
+ Inline_asm_sdump;
]
let error_warnings: warning_type list ref = ref []
@@ -113,6 +115,7 @@ let string_of_warning = function
| Literal_range -> "literal-range"
| Unknown_pragmas -> "unknown-pragmas"
| CompCert_conformance -> "compcert-conformance"
+ | Inline_asm_sdump -> "inline-asm-sdump"
let activate_warning w () =
if not (List.mem w !active_warnings) then
@@ -151,6 +154,7 @@ let wall () =
Literal_range;
Unknown_pragmas;
CompCert_conformance;
+ Inline_asm_sdump;
]
let werror () =
@@ -173,6 +177,7 @@ let werror () =
Return_type;
Literal_range;
Unknown_pragmas;
+ Inline_asm_sdump;
]
@@ -294,6 +299,7 @@ let warning_options =
error_option Literal_range @
error_option Unknown_pragmas @
error_option CompCert_conformance @
+ error_option Inline_asm_sdump @
[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/Cerrors.mli b/cparser/Cerrors.mli
index 56894c87..8501cfa0 100644
--- a/cparser/Cerrors.mli
+++ b/cparser/Cerrors.mli
@@ -44,6 +44,7 @@ type warning_type =
| Literal_range (** literal ranges *)
| Unknown_pragmas (** unknown/unsupported pragma *)
| CompCert_conformance (** features that are not part of the CompCert C core language *)
+ | Inline_asm_sdump (** inline assembler used in combination of sdump *)
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