aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 17:02:45 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-08 17:02:45 +0200
commitc3f5f3dbd088091e3fab9f357b01693932d148f8 (patch)
treefee361b1e1cc616a1b9c412ae5cec7c9467dcf32 /driver/Driver.ml
parent96165dbec88ab4c951d99e64e51f5c55a1244137 (diff)
downloadcompcert-kvx-c3f5f3dbd088091e3fab9f357b01693932d148f8.tar.gz
compcert-kvx-c3f5f3dbd088091e3fab9f357b01693932d148f8.zip
reloading and exploiting seems to work
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 7fbcb025..29fbaa7c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -222,8 +222,10 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
-falign-functions <n> Set alignment (in bytes) of function entry points
-falign-branch-targets <n> Set alignment (in bytes) of branch targets
-falign-cond-branches <n> Set alignment (in bytes) of conditional branches
- -fcommon Put uninitialized globals in the common section [on].
+ -fcommon Put uninitialized globals in the common section [on]
-fprofile-arcs Profile branches [off].
+ -fprofile-use= filename Use profiling information in filename
+ -fbranch-probabilities Use profiling information (if available) for branches [on]
|} ^
target_help ^
toolchain_help ^