Prefixed runtime functions.

The runtime functions are prefixed with compcert in order to
avoid potential clashes with runtime/builtin functions of other
compilers.
Bug 22062

1 files changed, 30 insertions, 30 deletions

diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index fd1fdebd..f1e8b590 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -32,45 +32,45 @@ Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (
   external_call (EF_builtin name sg) ge vargs m E0 vres m.
 
 Axiom i64_helpers_correct :
-    (forall x z, Val.longoffloat x = Some z -> external_implements "__i64_dtos" sig_f_l (x::nil) z)
- /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__i64_dtou" sig_f_l (x::nil) z)
- /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__i64_stod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__i64_utod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__i64_stof" sig_l_s (x::nil) z)
- /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__i64_utof" sig_l_s (x::nil) z)
+    (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z)
+ /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z)
+ /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z)
+ /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z)
+ /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z)
+ /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z)
  /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x))
  /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y))
  /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y))
  /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y))
- /\ (forall x y z, Val.divls x y = Some z -> external_implements "__i64_sdiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__i64_udiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modls x y = Some z -> external_implements "__i64_smod" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__i64_umod" sig_ll_l (x::y::nil) z)
- /\ (forall x y, external_implements "__i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
- /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
- /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y))
- /\ (forall x y, external_implements "__i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y))
- /\ (forall x y, external_implements "__i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)).
+ /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z)
+ /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
+ /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
+ /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y))
+ /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y))
+ /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)).
 
 Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
   (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))).
 
 Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop :=
-     helper_declared p i64_dtos "__i64_dtos" sig_f_l
-  /\ helper_declared p i64_dtou "__i64_dtou" sig_f_l
-  /\ helper_declared p i64_stod "__i64_stod" sig_l_f
-  /\ helper_declared p i64_utod "__i64_utod" sig_l_f
-  /\ helper_declared p i64_stof "__i64_stof" sig_l_s
-  /\ helper_declared p i64_utof "__i64_utof" sig_l_s
-  /\ helper_declared p i64_sdiv "__i64_sdiv" sig_ll_l
-  /\ helper_declared p i64_udiv "__i64_udiv" sig_ll_l
-  /\ helper_declared p i64_smod "__i64_smod" sig_ll_l
-  /\ helper_declared p i64_umod "__i64_umod" sig_ll_l
-  /\ helper_declared p i64_shl "__i64_shl" sig_li_l
-  /\ helper_declared p i64_shr "__i64_shr" sig_li_l
-  /\ helper_declared p i64_sar "__i64_sar" sig_li_l
-  /\ helper_declared p i64_umulh "__i64_umulh" sig_ll_l
-  /\ helper_declared p i64_smulh "__i64_smulh" sig_ll_l.
+     helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l
+  /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l
+  /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f
+  /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f
+  /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s
+  /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s
+  /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l
+  /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l
+  /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l
+  /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l
+  /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l
+  /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l
+  /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l
+  /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l
+  /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l.
 
 (** * Correctness of the instruction selection functions for 64-bit operators *)