aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authornicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-22 15:57:21 +0200
committernicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-22 15:57:21 +0200
commit10cbe4b28ef6dc5d02c9a5d4d369484e4943a18d (patch)
treef5334c751dd40116a630ca238db02a8a35841471 /driver
parentfe557bf65ec738eaa078bc5e398ff690eb1f2b9e (diff)
downloadcompcert-kvx-10cbe4b28ef6dc5d02c9a5d4d369484e4943a18d.tar.gz
compcert-kvx-10cbe4b28ef6dc5d02c9a5d4d369484e4943a18d.zip
Changed default threshold value following tests
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 1f31bd3e..c90fdb8c 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -115,5 +115,5 @@ let option_inline_auto_threshold = ref 0
let option_profile_arcs = ref false
let option_fbranch_probabilities = ref true
let option_debug_compcert = ref 0
-let option_regpres_threshold = ref 5
+let option_regpres_threshold = ref 2
let main_function_name = ref "main"