aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 16:28:00 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 16:28:00 +0200
commit96165dbec88ab4c951d99e64e51f5c55a1244137 (patch)
tree86110cecc1b97e39f2f8e5d58e228dd1dd10a1c5 /driver
parentda923568ad5085654b8db034310c4db50848e16e (diff)
downloadcompcert-kvx-96165dbec88ab4c951d99e64e51f5c55a1244137.tar.gz
compcert-kvx-96165dbec88ab4c951d99e64e51f5c55a1244137.zip
fixed a bug in support libraries; reload profiling info
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Driver.ml1
2 files changed, 1 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 87c8d9c8..600c3371 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -84,4 +84,3 @@ let option_all_loads_nontrap = ref false
let option_inline_auto_threshold = ref 0
let option_profile_arcs = ref false
-
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 909ef0d5..7fbcb025 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -328,6 +328,7 @@ let cmdline_actions =
_Regexp "-O[123]$", Unit (set_all optimization_options);
Exact "-Os", Set option_Osize;
Exact "-Obranchless", Set option_Obranchless;
+ Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s);
Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n);
Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
Exact "-fsmall-const", Integer(fun n -> option_small_const := n);