diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-07 13:37:20 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-07 13:37:20 +0100 |
commit | 36f52bf433614156a64358dbd71019b8d34865c5 (patch) | |
tree | 3494b9a2e94c420ba378bd2c83de07884d565f76 /cfrontend | |
parent | c91b33e36d96a51329d53bd9efa1523e567d1812 (diff) | |
download | compcert-36f52bf433614156a64358dbd71019b8d34865c5.tar.gz compcert-36f52bf433614156a64358dbd71019b8d34865c5.zip |
Improve and simplify error messages.
The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c18a6e03..c4772688 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -882,11 +882,7 @@ let rec convertExpr env e = let fun_name = !currentFunction in let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in let targs1 = convertTypArgs env [] args1 in - List.iter (fun exp -> if Cutil.is_float_type env exp.etyp then begin - error "floating point types are not supported in ais annotations" - end else if Cutil.is_volatile_variable env exp then begin - error "access to volatile variables are not supported in ais annotations" - end) args1; + AisAnnot.validate_ais_annot env !currentLocation txt args1; Ebuiltin( AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) |