summaryrefslogtreecommitdiff
path: root/compiler/Config.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Config.ml')
-rw-r--r--compiler/Config.ml18
1 files changed, 15 insertions, 3 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 7c3ce538..3e882365 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -30,7 +30,10 @@ let backend = ref FStar
(** {1 Interpreter} *)
-(** Check that invariants are maintained whenever we execute a statement *)
+(** Check that invariants are maintained whenever we execute a statement
+
+ TODO: rename to sanity_checks.
+ *)
let check_invariants = ref true
(** Expand all symbolic values containing borrows upon introduction - allows
@@ -72,6 +75,17 @@ let allow_bottom_below_borrow = true
*)
let return_unit_end_abs_with_no_loans = true
+(** The maximum number of iterations we can do to find a loop fixed point.
+
+ This is mostly for sanity: we should always find a fixed point in a
+ reasonable number of iterations. If we fail to do so, it is likely a bug: we
+ thus use this bound to detect a loop, fail and report the case to the
+ user.
+ *)
+let loop_fixed_point_max_num_iters = 100
+
+(** {1 Translation} *)
+
(** Forbids using field projectors for structures.
If we don't use field projectors, whenever we symbolically expand a structure
@@ -103,8 +117,6 @@ let dont_use_field_projectors = ref false
let always_deconstruct_adts_with_matches = ref false
-(** {1 Translation} *)
-
(** Controls whether we need to use a state to model the external world
(I/O, for instance).
*)