From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Thu, 19 Jul 2018 13:33:17 +0200
Subject: Add primitive floats to 'vm_compute'

* This commit add float instructions to the VM, their encoding in bytecode
  and the interpretation of primitive float values after the reduction.

* The flag '-std=c99' could be added to the C compiler flags to ensure
  that float computation strictly follows the norm (ie. i387 80-bits
  format is not used as an optimization).

  Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
  because the latter would disable GNU asm used in the VM.
---
 kernel/genOpcodeFiles.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'kernel/genOpcodeFiles.ml')

diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index a8a4ffce9c..7deffd030b 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -137,6 +137,18 @@ let opcodes =
     "CHECKTAIL0INT63";
     "ISINT";
     "AREINT2";
+    "CHECKOPPFLOAT";
+    "CHECKABSFLOAT";
+    "CHECKCOMPAREFLOAT";
+    "CHECKADDFLOAT";
+    "CHECKSUBFLOAT";
+    "CHECKMULFLOAT";
+    "CHECKDIVFLOAT";
+    "CHECKSQRTFLOAT";
+    "CHECKFLOATOFINT63";
+    "CHECKFLOATNORMFRMANTISSA";
+    "CHECKFRSHIFTEXP";
+    "CHECKLDSHIFTEXP";
     "STOP"
   |]
 
-- 
cgit v1.2.3