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.

1 files changed, 1 insertions, 1 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 990f207d..fad13c9f 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -377,7 +377,7 @@ let expand_instruction instr =
   | Pbuiltin (ef,args,res) ->
      begin match ef with
 	   | EF_builtin (name,sg) ->
-	      expand_builtin_inline (extern_atom name) args res
+	      expand_builtin_inline (camlstring_of_coqstring name) args res
 	   | EF_vload chunk ->
 	      expand_builtin_vload chunk args res
 	   | EF_vstore chunk ->