diff options
Diffstat (limited to 'common/Builtins0.v')
| -rw-r--r-- | common/Builtins0.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/common/Builtins0.v b/common/Builtins0.v index a3215545..f72febf8 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -337,7 +337,7 @@ Inductive standard_builtin : Type := | BI_addl | BI_subl | BI_mull - | BI_expect +(* | BI_expect *) | BI_i16_bswap | BI_i32_bswap | BI_i64_bswap @@ -370,7 +370,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_addl", BI_addl) :: ("__builtin_subl", BI_subl) :: ("__builtin_mull", BI_mull) - :: ("__builtin_expect", BI_expect) +(* :: ("__builtin_expect", BI_expect) *) :: ("__builtin_bswap16", BI_i16_bswap) :: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap) @@ -405,8 +405,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_mull => mksignature (Tint :: Tint :: nil) Tlong cc_default - | BI_expect => - mksignature (Tlong :: Tlong :: nil) Tlong cc_default +(* | BI_expect => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default *) | BI_i32_bswap => mksignature (Tint :: nil) Tint cc_default | BI_i64_bswap => @@ -437,8 +437,8 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _ | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _ - | BI_expect => - mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x) +(* | BI_expect => + mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x) *) | BI_i16_bswap => mkbuiltin_n1t Tint Tint (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n))))) |