diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-03-06 09:59:23 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-06 09:59:23 +0100 |
| commit | 7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f (patch) | |
| tree | 550a1a180c7296a125f6f8e5813460e2c078127b /cparser/Diagnostics.ml | |
| parent | 086c6686ec93cdaf7b6433cffdc4d8403a06f8b6 (diff) | |
| download | compcert-kvx-7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f.tar.gz compcert-kvx-7ca7e64ab06d0d4deb6b3b48593f4955cf5c3c5f.zip | |
Reactivated and improved ais annotations.
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
Diffstat (limited to 'cparser/Diagnostics.ml')
| -rw-r--r-- | cparser/Diagnostics.ml | 8 |
1 files changed, 7 insertions, 1 deletions
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; |