From 55d32c9f3a91058f69f34c17c17701d0dc81874d Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Thu, 19 Jul 2018 13:33:17 +0200
Subject: Add tests for primitive floats with 'vm_compute'

Tests are updated to include VM computations and check for double
rounding.
---
 test-suite/primitive/float/coq_env_double_array.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/primitive/float/coq_env_double_array.v

(limited to 'test-suite/primitive/float/coq_env_double_array.v')

diff --git a/test-suite/primitive/float/coq_env_double_array.v b/test-suite/primitive/float/coq_env_double_array.v
new file mode 100644
index 0000000000..754ccb69aa
--- /dev/null
+++ b/test-suite/primitive/float/coq_env_double_array.v
@@ -0,0 +1,13 @@
+Require Import Floats.
+
+Goal True.
+pose (f := one).
+pose (f' := (-f)%float).
+
+(* this used to segfault when the coq_env array given to the
+   coq_interprete C function was an unboxed OCaml Double_array
+   (created by Array.map in csymtable.ml just before calling
+   eval_tcode) *)
+vm_compute in f'.
+
+Abort.
-- 
cgit v1.2.3