From 36f52bf433614156a64358dbd71019b8d34865c5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 7 Mar 2018 13:37:20 +0100 Subject: 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. --- cfrontend/C2C.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'cfrontend') 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) -- cgit