vendors,hacl: use more generic gcc options

Tentative fix for "Illegal instruction (core dumped)" on certain
architectures du to gcc over optimization. This can possibly
introduce a performance regression.

@chambart for his gbd-foo skills
This commit is contained in:
Pietro Abate 2018-10-11 17:23:12 +02:00
parent e02ba41a65
commit 000b9af6f9
No known key found for this signature in database
GPG Key ID: 375CEF476926787B

View File

@ -1,6 +1,6 @@
let () = let () =
(* inspired by https://github.com/vbmithr/ocaml-secp256k1-internal/blob/master/config/discover.ml *) (* inspired by https://github.com/vbmithr/ocaml-secp256k1-internal/blob/master/config/discover.ml *)
let ccopts = "-Ofast -march=native -mtune=native -fwrapv -fomit-frame-pointer -funroll-loops -Wall -Werror -Wfatal-errors" in let ccopts = "-Ofast -mtune=generic -fwrapv -fomit-frame-pointer -funroll-loops -Wall -Werror -Wfatal-errors" in
(* the important bit is -DKRML_NOUINT128 which enables the verified (but slow) implementation of UInt128 in FStar.c rather than the builtin __int128 which is only available on 64-bit platforms. *) (* the important bit is -DKRML_NOUINT128 which enables the verified (but slow) implementation of UInt128 in FStar.c rather than the builtin __int128 which is only available on 64-bit platforms. *)
let ccopts32 = "-Ofast -fwrapv -fomit-frame-pointer -funroll-loops -DKRML_NOUINT128 -Wall -Werror -Wfatal-errors" in let ccopts32 = "-Ofast -fwrapv -fomit-frame-pointer -funroll-loops -DKRML_NOUINT128 -Wall -Werror -Wfatal-errors" in