summaryrefslogtreecommitdiff
path: root/driver/Driver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index ca703fd..85f6079 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -421,7 +421,6 @@ Interpreter mode:
-trace Have the interpreter produce a detailed trace of reductions
-random Randomize execution order
-all Simulate all possible execution orders
- -randvol Return random results for reading volatile variables
"
let language_support_options = [
@@ -463,7 +462,6 @@ let cmdline_actions =
"-trace$", Self (fun _ -> Interp.trace := 2);
"-random$", Self (fun _ -> Interp.mode := Interp.Random);
"-all$", Self (fun _ -> Interp.mode := Interp.All);
- "-randvol$", Self (fun _ -> Interp.random_volatiles := true);
".*\\.c$", Self (fun s ->
let objfile = process_c_file s in
linker_options := objfile :: !linker_options);