diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Config.ml | 4 | ||||
| -rw-r--r-- | compiler/Driver.ml | 14 |
2 files changed, 9 insertions, 9 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 8483c879..a487f9e2 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -124,7 +124,7 @@ let always_deconstruct_adts_with_matches = ref false (** Controls whether we need to use a state to model the external world (I/O, for instance). *) -let use_state = ref true +let use_state = ref false (** Controls whether we use fuel to control termination. *) @@ -160,7 +160,7 @@ let backward_no_state_update = ref false files for the types, clauses and functions, or if we group them in one file. *) -let split_files = ref true +let split_files = ref false (** Generate the library entry point, if the crate is split between different files. diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 14668632..128ae890 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -93,9 +93,9 @@ let () = Arg.Set extract_decreases_clauses, " Use decreases clauses/termination measures for the recursive \ definitions" ); - ( "-no-state", - Arg.Clear use_state, - " Do not use state-error monads, simply use error monads" ); + ( "-state", + Arg.Set use_state, + " Use a *state*-error monads, instead of an error monads" ); ( "-use-fuel", Arg.Set use_fuel, " Use a fuel parameter to control divergence" ); @@ -106,10 +106,10 @@ let () = Arg.Set extract_template_decreases_clauses, " Generate templates for the required decreases clauses/termination \ measures, in a dedicated file. Implies -decreases-clauses" ); - ( "-no-split-files", - Arg.Clear split_files, - " Do not split the definitions between different files for types, \ - functions, etc." ); + ( "-split-files", + Arg.Set split_files, + " Split the definitions between different files for types, functions, \ + etc." ); ( "-no-check-inv", Arg.Clear check_invariants, " Deactivate the invariant sanity checks performed at every evaluation \ |