diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 19:28:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 19:28:03 +0100 |
| commit | 50ea35fceb52c5f66ccbc4f709df3a3471b12647 (patch) | |
| tree | cbbe994acd0e7e50c8a0302c5b62c84b0e753709 /backend/Selection.v | |
| parent | 202050c6240a11c94cc8b6ab599022fee7bd2471 (diff) | |
| download | compcert-kvx-50ea35fceb52c5f66ccbc4f709df3a3471b12647.tar.gz compcert-kvx-50ea35fceb52c5f66ccbc4f709df3a3471b12647.zip | |
added helper functions but strange
idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 4520cb0c..fc9315dc 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -391,11 +391,16 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := do i64_sar <- lookup_helper globs "__compcert_i64_sar" sig_li_l ; do i64_umulh <- lookup_helper globs "__compcert_i64_umulh" sig_ll_l ; do i64_smulh <- lookup_helper globs "__compcert_i64_smulh" sig_ll_l ; + do i32_sdiv <- lookup_helper globs "__compcert_i32_sdiv" sig_ii_i ; + do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ; + do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ; + do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod i64_shl i64_shr i64_sar - i64_umulh i64_smulh). + i64_umulh i64_smulh + i32_sdiv i32_udiv i32_smod i32_umod). (** Conversion of programs. *) |