From 992434d9f842d784f686b523f6ef02ca4bb0aaa5 Mon Sep 17 00:00:00 2001 From: Thibaut Benjamin <thibaut.benjamin@cea.fr> Date: Mon, 26 Jul 2021 10:37:41 +0200 Subject: [PATCH] [e-acsl] typographic corrections --- src/plugins/e-acsl/src/analyses/bound_variables.ml | 4 ++++ src/plugins/e-acsl/src/code_generator/env.ml | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml index f544f8b7447..6bdf6e32d0d 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 24775347413..dce4af58bf9 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 -- GitLab