diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-20 14:54:48 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-20 14:54:48 +0100 |
| commit | 9f2ca1049957004161834090a697cd4118e2fb08 (patch) | |
| tree | 48fbe0560962ea0a748cfa15edcbc63fa56bd252 /extraction | |
| parent | 28d7ff1fef9a47206114773d38e04361dc49820b (diff) | |
| download | compcert-kvx-9f2ca1049957004161834090a697cd4118e2fb08.tar.gz compcert-kvx-9f2ca1049957004161834090a697cd4118e2fb08.zip | |
Protect against redefinition of the __i64_xxx helper library functions.
This is achieved by declaring these functions in C2C.ml, then
re-checking their declarations in the global environment during
the Selection pass.
In passing, the "hf" parameter for SelectLong functions was removed
and replaced by fixed identifiers corresponding to the actual names
of the helper functions.
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..94ac6f52 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -57,12 +57,6 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant SelectLong.get_helper => - "fun ge s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". -Extract Constant SelectLong.get_builtin => - "fun s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) |