[eacsl] Do not reverse lscope list in Lscope.get_all

src/plugins/e-acsl/src/analyses/lscope.ml

@@ -33,7 +33,7 @@ let is_empty = function [] -> true | _ :: _ -> false
 
 let add lscope_var t = lscope_var :: t
 
-let get_all t = List.rev t
+let get_all t = t
 
 let exists lv t =
   let is_lv = function

src/plugins/e-acsl/src/analyses/lscope.mli

@@ -41,8 +41,9 @@ val add: lscope_var -> t -> t
 
 val get_all: t -> lscope_var list
 (* Return the list of [lscope_var] of the given logic scope.
-   The first element is the first [lscope_var] that was added to [t], the
-   second element is the second [lscope_var] that was added to [t], an so on. *)
+   The first element is the last [lscope_var] that was added to [t], the
+   second element is the second to last [lscope_var] that was added to [t], and
+   so on. *)
 
 val is_used: t -> pred_or_term -> bool
 (* [is_used lscope pot] returns [true] iff [pot] uses a variable from

src/plugins/e-acsl/src/code_generator/at_with_lscope.ml

@@ -236,6 +236,7 @@ let put_block_at_label env kf block label =
 let to_exp ~loc kf env pot label =
   let term_to_exp = !term_to_exp_ref in
   let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
+  let lscope_vars = List.rev lscope_vars in
   let sizes_and_shifts =
     sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
   in
@@ -349,6 +350,7 @@ let to_exp ~loc kf env pot label =
   in
   (* Storing loops *)
   let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
+  let lscope_vars = List.rev lscope_vars in
   let env = Env.push env in
   let storing_loops_stmts, env =
     Loops.mk_nested_loops ~loc mk_innermost_block kf env lscope_vars