diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-10-11 17:43:59 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-10-11 17:43:59 +0200 |
| commit | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (patch) | |
| tree | 6119d963ce34b56386f79693972e8ce86d9c0e87 /cfrontend/PrintCsyntax.ml | |
| parent | 659b735ed2dbefcbe8bcb2ec2123b66019ddaf14 (diff) | |
| download | compcert-kvx-7a6bb90048db7a254e959b1e3c308bac5fe6c418.tar.gz compcert-kvx-7a6bb90048db7a254e959b1e3c308bac5fe6c418.zip | |
Use Coq strings instead of idents to name external and builtin functions.
The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example:
* in $ARCH/Machregs.v to define the register conventions for builtin functions;
* in the VST program logic from Princeton to treat thread primitives specially.
So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq.
This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index d890c820..ce912a8c 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -258,12 +258,12 @@ let rec expr p (prec, e) = exprlist (true, args) | Ebuiltin(EF_annot(txt, _), _, args, _) -> fprintf p "__builtin_annot@[<hov 1>(%S%a)@]" - (extern_atom txt) exprlist (false, args) + (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]" - (extern_atom txt) exprlist (false, args) + (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> - fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args) + fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob | Ebuiltin(_, _, args, _) -> @@ -282,7 +282,7 @@ and exprlist p (first, rl) = exprlist p (false, rl) and extended_asm p txt res args clob = - fprintf p "asm volatile (@[<hv 0>%S" (extern_atom txt); + fprintf p "asm volatile (@[<hv 0>%S" (camlstring_of_coqstring txt); fprintf p "@ :"; begin match res with | None -> () |