diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:44:00 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:44:00 +0100 |
| commit | 82be9309276a2de2cff6ab96ef7f7b74bb34ffbb (patch) | |
| tree | 8fd1a4ebd992c7accd7c6f51874f0f1beaa3ac3a /mppa_k1c | |
| parent | 4437accc3ce393a7dbeda34b51f3507ba6c4f47f (diff) | |
| download | compcert-kvx-82be9309276a2de2cff6ab96ef7f7b74bb34ffbb.tar.gz compcert-kvx-82be9309276a2de2cff6ab96ef7f7b74bb34ffbb.zip | |
during merge; still some typing issues
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Builtins1.v | 12 | ||||
| -rw-r--r-- | mppa_k1c/Conventions1.v | 3 |
2 files changed, 9 insertions, 6 deletions
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v index 6186961f..3b5cd419 100644 --- a/mppa_k1c/Builtins1.v +++ b/mppa_k1c/Builtins1.v @@ -43,18 +43,18 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with | BI_fmin | BI_fmax => - mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fminf | BI_fmaxf => - mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default | BI_fabsf => - mksignature (Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: nil) Tsingle cc_default | BI_fma => - mksignature (Tfloat :: Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => - mksignature (Tsingle :: Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.min | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 9e9bae6f..ac2117d0 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -415,3 +415,6 @@ Lemma loc_arguments_main: Proof. reflexivity. Qed. + + +Definition return_value_needs_normalization (t: rettype) : bool := false. |