diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 13 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 8 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 |
3 files changed, 15 insertions, 14 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd281374..9b31dfdb 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -769,7 +769,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, typlist_of_typelist targs1), + EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; @@ -781,7 +781,7 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ), + Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> @@ -822,7 +822,7 @@ let rec convertExpr env e = let sg = signature_of_type targs tres {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(intern_string "printf", sg), + Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) | C.ECall(fn, args) -> @@ -877,7 +877,7 @@ let convertAsm loc env txt outputs inputs clobber = let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(intern_string txt', + Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput cc_default, clobber'), tinputs, @@ -1085,14 +1085,15 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in + let id'' = coqstring_of_camlstring id.name in let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.functions - then EF_builtin(id', sg) - else EF_external(id', sg) in + then EF_builtin(id'', sg) + else EF_external(id'', sg) in (id', Gfun(External(ef, args, res, cconv))) (** Initializers *) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 16d5823b..938454c5 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -391,7 +391,7 @@ Qed. (** External calls *) Variable do_external_function: - ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). + string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_external_function_sound: forall id sg ge vargs m t vres m' w w', @@ -405,7 +405,7 @@ Hypothesis do_external_function_complete: do_external_function id sg ge w vargs m = Some(w', t, vres, m'). Variable do_inline_assembly: - ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). + string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_inline_assembly_sound: forall txt sg ge vargs m t vres m' w w', @@ -513,12 +513,12 @@ Definition do_ef_memcpy (sz al: Z) | _ => None end. -Definition do_ef_annot (text: ident) (targs: list typ) +Definition do_ef_annot (text: string) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := do args <- list_eventval_of_val vargs targs; Some(w, Event_annot text args :: E0, Vundef, m). -Definition do_ef_annot_val (text: ident) (targ: typ) +Definition do_ef_annot_val (text: string) (targ: typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | varg :: nil => 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 -> () |