diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-09 09:50:35 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-09 09:50:35 +0100 |
commit | d50509fb3a74cae6c5851eeff2b54fba5cfd425c (patch) | |
tree | 2ba6ca7322b66fb24b87fe2c09a20176568781a3 /backend/AisAnnot.ml | |
parent | 5063ae307001dcddbfcc60e7abda04cf98bffeb4 (diff) | |
download | compcert-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
Diffstat (limited to 'backend/AisAnnot.ml')
-rw-r--r-- | backend/AisAnnot.ml | 10 |
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); |