diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-24 16:23:50 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-24 16:23:50 +0200 |
| commit | 34768a3c2ed8a2ee09786cd7e56fe3a7e7491efb (patch) | |
| tree | 9c36f87071c5b4cf7eb7b5d74059860ad6cc8524 /cfrontend/C2C.ml | |
| parent | c96c50577569c6077c42e756bbf12d31d9c82717 (diff) | |
| download | compcert-34768a3c2ed8a2ee09786cd7e56fe3a7e7491efb.tar.gz compcert-34768a3c2ed8a2ee09786cd7e56fe3a7e7491efb.zip | |
Prefix ais annotations with location.
The file and line information are now stored as comment string at
the start of each annotation.
Bug 22462
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a7ee353a..3e3ac48a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -863,9 +863,11 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> - let targs1 = convertTypArgs env [] args1 in + let file,line = !currentLocation in + let loc_string = Printf.sprintf "# file %s, line %d\n" file line in + let targs1 = convertTypArgs env [] args1 in Ebuiltin( - AST.EF_annot(P.of_int 2,coqstring_of_camlstring txt, typlist_of_typelist targs1), + 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) | _ -> error "argument 1 of '__builtin_ais_annot' must be a string literal"; |