1 files changed, 48 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v
index 87ebea00..cf5a1255 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -244,6 +244,18 @@ Definition intuoffloat (v: val) : option val :=
   | _ => None
   end.
 
+Definition intoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vint (Float.to_int_ne f)
+  | _ => None
+  end.
+
+Definition intuoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vint (Float.to_intu_ne f)
+  | _ => None
+  end.
+
 Definition floatofint (v: val) : option val :=
   match v with
   | Vint n => Some (Vfloat (Float.of_int n))
@@ -268,6 +280,18 @@ Definition intuofsingle (v: val) : option val :=
   | _ => None
   end.
 
+Definition intofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vint (Float32.to_int_ne f)
+  | _ => None
+  end.
+
+Definition intuofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vint (Float32.to_intu_ne f)
+  | _ => None
+  end.
+
 Definition singleofint (v: val) : option val :=
   match v with
   | Vint n => Some (Vsingle (Float32.of_int n))
@@ -623,6 +647,30 @@ Definition longuofsingle (v: val) : option val :=
   | _ => None
   end.
 
+Definition longoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vlong (Float.to_long_ne f)
+  | _ => None
+  end.
+
+Definition longuoffloat_ne (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vlong (Float.to_longu_ne f)
+  | _ => None
+  end.
+
+Definition longofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vlong (Float32.to_long_ne f)
+  | _ => None
+  end.
+
+Definition longuofsingle_ne (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vlong (Float32.to_longu_ne f)
+  | _ => None
+  end.
+
 Definition floatoflong (v: val) : option val :=
   match v with
   | Vlong n => Some (Vfloat (Float.of_long n))