diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml index f544f8b7447c908f53d4b4892868a7abfdd730e6..6bdf6e32d0d3268a1f04bbd6e233a50d43b45790 100644 --- a/src/plugins/e-acsl/src/analyses/bound_variables.ml +++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml @@ -495,6 +495,10 @@ end = struct Error.untypable msg end +(******************************************************************************) +(** Syntactical analysis *) +(******************************************************************************) + (** [extract_constraint ctxt t1 r t2] populates the quantification context [ctxt] with the constraint [t1 r t2], either adding a lower bound if [t2] is a bounded variable or adding an upper bound if [t1] is a bounded variable. diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml index 24775347413b7975db7d758f4c61ae1adcdf6b5a..dce4af58bf9d22d69fa087552a06223d74ab2865 100644 --- a/src/plugins/e-acsl/src/code_generator/env.ml +++ b/src/plugins/e-acsl/src/code_generator/env.ml @@ -445,7 +445,7 @@ let transfer ~from env = match from.env_stack, env.env_stack with type where = Before | Middle | After let pop_and_get ?(split=false) env stmt ~global_clear where = let split = split && stmt.labels = [] in - (* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split;*) + (* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split; *) let local_env, tl = top env in let clear = if global_clear then begin