diff options
Diffstat (limited to 'kvx/Builtins1.v')
| -rw-r--r-- | kvx/Builtins1.v | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index a0473d07..e3e4f95d 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -16,7 +16,7 @@ (** Platform-specific built-in functions *) Require Import String Coqlib. -Require Import AST Integers Floats Values ExtFloats. +Require Import AST Integers Floats Values ExtFloats ExtValues. Require Import Builtins0. Inductive platform_builtin : Type := @@ -31,7 +31,9 @@ Inductive platform_builtin : Type := | BI_fp_udiv32 | BI_fp_udiv64 | BI_fp_umod32 -| BI_fp_umod64. +| BI_fp_umod64 +| BI_abs +| BI_absl. Local Open Scope string_scope. @@ -48,6 +50,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fp_udiv64", BI_fp_udiv64) :: ("__builtin_fp_umod32", BI_fp_umod32) :: ("__builtin_fp_umod64", BI_fp_umod64) + :: ("__builtin_abs", BI_abs) + :: ("__builtin_absl", BI_absl) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -70,6 +74,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tint :: Tint :: nil) Tint cc_default | BI_fp_umod64 => mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_abs => + mksignature (Tint :: nil) Tint cc_default + | BI_absl => + mksignature (Tlong :: nil) Tlong cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -98,4 +106,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl (fun n1 n2 => if Int64.eq n2 Int64.zero then None else Some (Int64.modu n1 n2)) + | BI_abs => mkbuiltin_n1t Tint Tint ExtValues.int_abs + | BI_absl => mkbuiltin_n1t Tlong Tlong ExtValues.long_abs end. |