From fc34351a0c18baecd1cc707007bcd53aa24ff413 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 24 Mar 2014 10:44:27 +0100
Subject: [PATCH] why tabulations?
---
src/plugins/e-acsl/pre_analysis.ml | 90 +++++++++++++++---------------
1 file changed, 45 insertions(+), 45 deletions(-)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 614de29f79a..637c6f76480 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/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
--
GitLab