aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-03-09 09:50:35 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-03-09 09:50:35 +0100
commitd50509fb3a74cae6c5851eeff2b54fba5cfd425c (patch)
tree2ba6ca7322b66fb24b87fe2c09a20176568781a3
parent5063ae307001dcddbfcc60e7abda04cf98bffeb4 (diff)
downloadcompcert-d50509fb3a74cae6c5851eeff2b54fba5cfd425c.tar.gz
compcert-d50509fb3a74cae6c5851eeff2b54fba5cfd425c.zip
Do not use default printer for variable names.
Printing variable names with the default expression printer results in newlines in the outputed error message. Bug 23169
-rw-r--r--backend/AisAnnot.ml10
1 files changed, 8 insertions, 2 deletions
diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
index 27005561..c5fade24 100644
--- a/backend/AisAnnot.ml
+++ b/backend/AisAnnot.ml
@@ -188,8 +188,14 @@ let validate_ais_annot env loc txt args =
Array.set used_params (n-1) true;
if Cutil.is_float_type env arg.C.etyp then
error loc "floating point types for parameter '%s' are not supported in ais annotations" s
- else if Cutil.is_volatile_variable env arg then
- error loc "access to volatile variable '%a' for parameter '%s' is not supported in ais annotations" Cprint.exp (0,arg) s
+ else if Cutil.is_volatile_variable env arg then begin
+ let arg =
+ match arg.C.edesc with
+ | C.EVar id -> id.C.name
+ | _ -> assert false
+ in
+ error loc "access to volatile variable '%s' for parameter '%s' is not supported in ais annotations" arg s
+ end
with _ ->
error loc "unknown parameter '%s'" s
in List.iter fragment (Str.full_split re_ais_annot_param txt);