Remove My_unix module

[Halbaroth]

The purpose of My_unix was to provide dummy implementations for some Unix system calls in Javascript mode. These dummy implementations were actually dead code because we use a Dune feature to provide them through the stanza (javascript_files ...). This PR removes the useless module and inline and clean its code in Options.Time.

[bclement-ocp]

Is this also true for My_zip then?

[Halbaroth]

Strangely, the feature seems to work with native format. You can try it with:

node _build/default/src/bin/js/main_text_js.bc.js tests/misc/unzip.ae.zip

But the feature is broken with the SMT format. We got an infinity loop:

node _build/default/src/bin/js/main_text_js.bc.js tests/misc/unzip.smt2.zip

Notice that the file in unzip.smt2.zip is not the translation of the one in unzip.ae.zip. I also try with a very simple file:

(set-logic ALL)
(declare-const x Int)
(assert (= x x))
(check-sat)

It works with alt-ergo --frontend legacy but it goes into an infinity loop with node.

Still, we provide four dummy implementations related with camlzip:

// Camlzip primitives
//Provides: camlzip_inflateEnd
function  camlzip_inflateEnd () {
  return BLOCK(0, 0, 0, 0)
}
//Provides: camlzip_inflateInit
function camlzip_inflateInit () {
  return BLOCK(0, 0, 0, 0)
}
//Provides: camlzip_inflate_bytecode
function camlzip_inflate_bytecode () {
  return BLOCK(0, 0, 0, 0)
}
//Provides: camlzip_update_crc32
function camlzip_update_crc32 () {
  return BLOCK(0, 0, 0, 0)
}

If I remove these dummy implementations, Alt-Ergo with Node still works on the ae file but I got the following message on smt2 file:

Fatal error: exception Failure("camlzip_inflateInit not implemented")

I believe it works on some native files by sheer luck and we should disable this feature in js mode.