why tabulations?

src/plugins/e-acsl/pre_analysis.ml

@@ -401,51 +401,51 @@ module rec Transfer
     in
     Dataflow.Post 
       (fun state ->
-	let state = Env.default_varinfos state in
-	let state = 
-	  if (is_first || is_last) && Misc.is_generated_kf kf then 
-	    Annotations.fold_behaviors
-	      (fun _ bhv s -> 
-		let handle_annot test f s =
-		  if test then 
-		    f (fun _ p s -> register_predicate kf p s) kf bhv.b_name s
-		  else
-		    s
-		in
-		let s = handle_annot is_first Annotations.fold_requires s in
-		let s = handle_annot is_first Annotations.fold_assumes s in
-		handle_annot 
-		  is_last 
-		  (fun f -> Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
-	      kf
-	      state
-	  else
-	    state
-	in
-	let state = 
-	  Annotations.fold_code_annot
-	    (fun _ -> register_code_annot kf) stmt state
-	in
-	let state =
-	  if stmt.ghost then
-	    let rtes = Rte.stmt kf stmt in
-	    List.fold_left
-	      (fun state a -> register_code_annot kf a state) state rtes
-	  else 
-	    state
-	in
-	let state =
-	  (* take initializers into account *)
-	  if is_first then
-	    let main, lib = Globals.entry_point () in
-	    if Kernel_function.equal kf main && not lib then 
-	      register_initializers state
-	    else
-	      state
-	  else
-	    state
-	in
-	Some state)
+        let state = Env.default_varinfos state in
+        let state = 
+          if (is_first || is_last) && Misc.is_generated_kf kf then 
+	          Annotations.fold_behaviors
+	            (fun _ bhv s -> 
+		            let handle_annot test f s =
+		              if test then 
+		                f (fun _ p s -> register_predicate kf p s) kf bhv.b_name s
+		              else
+		                s
+		            in
+		            let s = handle_annot is_first Annotations.fold_requires s in
+		            let s = handle_annot is_first Annotations.fold_assumes s in
+		            handle_annot 
+		              is_last 
+		              (fun f -> Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
+	            kf
+	            state
+	        else
+	          state
+	      in
+	      let state = 
+	        Annotations.fold_code_annot
+	          (fun _ -> register_code_annot kf) stmt state
+	      in
+	      let state =
+	        if stmt.ghost then
+	          let rtes = Rte.stmt kf stmt in
+	          List.fold_left
+	            (fun state a -> register_code_annot kf a state) state rtes
+	        else 
+	          state
+	      in
+	      let state =
+	        (* take initializers into account *)
+	        if is_first then
+	          let main, lib = Globals.entry_point () in
+	          if Kernel_function.equal kf main && not lib then 
+	            register_initializers state
+	          else
+	            state
+	        else
+	          state
+	      in
+	      Some state)
 
   (** The (backwards) transfer function for an instruction. The
       [(Cil.CurrentLoc.get ())] is set before calling this. If it returns