diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-08 09:46:31 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-08 09:46:31 +0000 |
| commit | f687301c3616c83d4e8d6f23404671f85253520d (patch) | |
| tree | 9d2a1711dd2bc3591579dfa9b8d107ee6c58d7a1 /driver/Driver.ml | |
| parent | 8e5f68c1a6d921a46bb817fe0a82fca1c3494dde (diff) | |
| download | compcert-f687301c3616c83d4e8d6f23404671f85253520d.tar.gz compcert-f687301c3616c83d4e8d6f23404671f85253520d.zip | |
Better treatment of volatile accesses in the reference interpreter.
Suppressed option -randvol.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2092 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index ca703fdc..85f60791 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); |