diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 2eb4d2d1a7e4bbed5ecd0e46bc13c11dd1d9cc77..9d8eb9a550327225c832ef0d6707923cd868bd76 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -57,7 +57,6 @@ SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# project initializer
SRC_PROJECT_INITIALIZER:= \
- keep_status \
rtl \
prepare_ast
SRC_PROJECT_INITIALIZER:=\
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index c01f07f6269eda6dbe4441a0a0fae86977361871..3722be14ad4101f2cb7097d414683c0ca0065ed3 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -232,7 +232,7 @@ let add_new_block_in_stmt env kf stmt =
in
let mk_post_env env stmt =
Annotations.fold_code_annot
- (fun _ a env -> Translate.translate_post_code_annotation kf env a)
+ (fun _ a env -> Translate.translate_post_code_annotation kf stmt env a)
stmt
env
in
@@ -252,7 +252,7 @@ let add_new_block_in_stmt env kf stmt =
let env = mk_post_env env stmt in
(* also handle the postcondition of the function and clear the
env *)
- Translate.translate_post_spec kf env (Annotations.funspec kf)
+ Translate.translate_post_spec kf Kglobal env (Annotations.funspec kf)
else
env
in
@@ -450,7 +450,7 @@ and inject_in_stmt env kf stmt =
(* translate the precondition of the function *)
if Functions.check kf then
let funspec = Annotations.funspec kf in
- Translate.translate_pre_spec kf env funspec
+ Translate.translate_pre_spec kf Kglobal env funspec
else env
else
env
@@ -459,7 +459,7 @@ and inject_in_stmt env kf stmt =
let env =
if Functions.check kf then
Annotations.fold_code_annot
- (fun _ a env -> Translate.translate_pre_code_annotation kf env a)
+ (fun _ a env -> Translate.translate_pre_code_annotation kf stmt env a)
stmt
env
else
@@ -862,7 +862,6 @@ let inject () =
Options.feedback ~level:2
"injecting annotations as code in project %a"
Project.pretty (Project.current ());
- Keep_status.before_translation ();
Misc.reorder_ast ();
Gmp_types.init ();
let ast = Ast.get () in
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index b9dfc2390c42fb5519843333f0fb83f8b0bc2c0d..f3cb0dc8de11b567298a59bd2167bfc9d7ee6e00 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1135,12 +1135,27 @@ let term_to_exp typ t =
(* ************************************************************************** *)
(* [translate_*] translates a given ACSL annotation into the corresponding C
- statement (if any) for runtime assertion checking.
-
- IMPORTANT: the order of translation of pre-/post-spec must be consistent with
- the pushes done in [Keep_status] *)
+ statement (if any) for runtime assertion checking. *)
(* ************************************************************************** *)
+let must_translate ppt =
+ Options.Valid.get ()
+ || match Property_status.get ppt with
+ | Never_tried
+ | Inconsistent _
+ | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
+ true
+ | Best (True, _) ->
+ (* [TODO] generating code for "valid under hypotheses" properties could be
+ useful for some use cases (in particular, when E-ACSL does not stop on
+ the very first error).
+ ==> introduce a new option or modify the behavior of -e-acsl-valid *)
+ false
+
+let must_translate_opt = function
+ | None -> false
+ | Some ppt -> must_translate ppt
+
let assumes_predicate bhv =
List.fold_left
(fun acc p ->
@@ -1151,14 +1166,14 @@ let assumes_predicate bhv =
Logic_const.ptrue
bhv.b_assumes
-let translate_preconditions kf env behaviors =
+let translate_preconditions kf kinstr env behaviors =
let env = Env.set_annotation_kind env Constructor.Precondition in
let do_behavior env b =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
let do_it env =
- if Keep_status.must_translate kf Keep_status.K_Requires then
+ if must_translate (Property.ip_of_requires kf kinstr b p) then
let loc = p.ip_content.pred_loc in
let p =
Logic_const.pimplies
@@ -1176,16 +1191,16 @@ let translate_preconditions kf env behaviors =
in
List.fold_left do_behavior env behaviors
-let translate_postconditions kf env behaviors =
+let translate_postconditions kf kinstr env behaviors =
let env = Env.set_annotation_kind env Constructor.Postcondition in
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
let env =
handle_error
(fun env ->
- (* test ordering does matter for keeping statuses consistent *)
- if b.b_assigns <> WritesAny
- && Keep_status.must_translate kf Keep_status.K_Assigns
+ let active = [] in (* TODO: 'for' behaviors *)
+ let ppt = Property.ip_assigns_of_behavior kf kinstr ~active b in
+ if b.b_assigns <> WritesAny && must_translate_opt ppt
then not_yet env "assigns clause in behavior";
(* ignore b.b_extended since we never translate them *)
env)
@@ -1193,8 +1208,8 @@ let translate_postconditions kf env behaviors =
in
let assumes_pred = assumes_predicate b in
List.fold_left
- (fun env (t, p) ->
- if Keep_status.must_translate kf Keep_status.K_Ensures then
+ (fun env ((t, p) as tp) ->
+ if must_translate (Property.ip_of_ensures kf kinstr b tp) then
let do_it env =
match t with
| Normal ->
@@ -1221,56 +1236,53 @@ let translate_postconditions kf env behaviors =
in
List.fold_left do_behavior env bhvs
-let translate_pre_spec kf env spec =
+let translate_pre_spec kf kinstr env spec =
let unsupported f x = ignore (handle_error (fun env -> f x; env) env) in
let convert_unsupported_clauses env =
unsupported
- (Extlib.may
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Decreases then
- not_yet env "variant clause"))
- spec.spec_variant;
+ (fun spec ->
+ let ppt = Property.ip_decreases_of_spec kf kinstr spec in
+ if must_translate_opt ppt then not_yet env "variant clause")
+ spec;
(* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
unsupported
- (Extlib.may
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Terminates then
- not_yet env "terminates clause"))
- spec.spec_terminates;
- (match spec.spec_complete_behaviors with
- | [] -> ()
- | l ->
- unsupported
- (List.iter
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Complete then
- not_yet env "complete behaviors"))
- l);
- (match spec.spec_disjoint_behaviors with
- | [] -> ()
- | l ->
- unsupported
- (List.iter
- (fun _ ->
- if Keep_status.must_translate kf Keep_status.K_Disjoint then
- not_yet env "disjoint behaviors"))
- l);
+ (fun spec ->
+ let ppt = Property.ip_terminates_of_spec kf kinstr spec in
+ if must_translate_opt ppt then not_yet env "terminates clause")
+ spec;
+ let active = [] in (* TODO: 'for' behaviors *)
+ let ppts = Property.ip_complete_of_spec kf kinstr ~active spec in
+ unsupported
+ (fun ppts ->
+ List.iter
+ (fun ppt ->
+ if must_translate ppt then not_yet env "complete behaviors")
+ ppts)
+ ppts;
+ let ppts = Property.ip_disjoint_of_spec kf kinstr ~active spec in
+ unsupported
+ (fun ppts ->
+ List.iter
+ (fun ppt ->
+ if must_translate ppt then not_yet env "disjoint behaviors")
+ ppts)
+ ppts;
env
in
let env = convert_unsupported_clauses env in
handle_error
- (fun env -> translate_preconditions kf env spec.spec_behavior)
+ (fun env -> translate_preconditions kf kinstr env spec.spec_behavior)
env
-let translate_post_spec kf env spec =
+let translate_post_spec kf kinstr env spec =
handle_error
- (fun env -> translate_postconditions kf env spec.spec_behavior)
+ (fun env -> translate_postconditions kf kinstr env spec.spec_behavior)
env
-let translate_pre_code_annotation kf env annot =
+let translate_pre_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
| AAssert(l, _, p) ->
- if Keep_status.must_translate kf Keep_status.K_Assert then
+ if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Constructor.Assertion in
if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
@@ -1280,9 +1292,9 @@ let translate_pre_code_annotation kf env annot =
| AStmtSpec(l, spec) ->
if l <> [] then
not_yet env "@[statement contract applied only on some behaviors@]";
- translate_pre_spec kf env spec ;
+ translate_pre_spec kf (Kstmt stmt) env spec ;
| AInvariant(l, loop_invariant, p) ->
- if Keep_status.must_translate kf Keep_status.K_Invariant then
+ if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Constructor.Invariant in
if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
@@ -1291,26 +1303,30 @@ let translate_pre_code_annotation kf env annot =
else
env
| AVariant _ ->
- if Keep_status.must_translate kf Keep_status.K_Variant
+ if must_translate (Property.ip_of_code_annot_single kf stmt annot)
then not_yet env "variant"
else env
| AAssigns _ ->
(* TODO: it is not a precondition *)
- if Keep_status.must_translate kf Keep_status.K_Assigns
- then not_yet env "assigns"
- else env
+ let ppts = Property.ip_of_code_annot kf stmt annot in
+ List.iter
+ (fun ppt -> if must_translate ppt then not_yet env "assigns")
+ ppts;
+ env
| AAllocation _ ->
- if Keep_status.must_translate kf Keep_status.K_Allocation
- then not_yet env "allocation"
- else env
+ let ppts = Property.ip_of_code_annot kf stmt annot in
+ List.iter
+ (fun ppt -> if must_translate ppt then not_yet env "allocation")
+ ppts;
+ env
| APragma _ -> not_yet env "pragma"
| AExtended _ -> env (* never translate extensions. *)
in
handle_error convert env
-let translate_post_code_annotation kf env annot =
+let translate_post_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
- | AStmtSpec(_, spec) -> translate_post_spec kf env spec
+ | AStmtSpec(_, spec) -> translate_post_spec kf (Kstmt stmt) env spec
| AAssert _
| AInvariant _
| AVariant _
diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate.mli
index b38599d54403b537afbb1dec5277430e3b4d0a6c..64a83c76113bbe3e29142f4d4d6981e74ae81d00 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate.mli
@@ -26,12 +26,12 @@ open Cil_types
statement (if any) for runtime assertion checking. This C statements are
part of the resulting environment. *)
-val translate_pre_spec: kernel_function -> Env.t -> funspec -> Env.t
-val translate_post_spec: kernel_function -> Env.t -> funspec -> Env.t
+val translate_pre_spec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
+val translate_post_spec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
val translate_pre_code_annotation:
- kernel_function -> Env.t -> code_annotation -> Env.t
+ kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
val translate_post_code_annotation:
- kernel_function -> Env.t -> code_annotation -> Env.t
+ kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
val translate_named_predicate:
kernel_function -> Env.t -> predicate -> Env.t
@@ -50,6 +50,6 @@ val predicate_to_exp: kernel_function -> predicate -> exp
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index caa37aa4bce1354fdd41bc79c6d12f0015e2054f..6e52696fb1c02572af20e9e2a565da814b1b7f86 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -168,7 +168,6 @@ let change_printer =
end
let main () =
- Keep_status.clear ();
if Options.Run.get () then begin
change_printer ();
ignore (generate_code (Options.Project_name.get ()));
diff --git a/src/plugins/e-acsl/src/project_initializer/keep_status.ml b/src/plugins/e-acsl/src/project_initializer/keep_status.ml
deleted file mode 100644
index aa933b5f1a417c43b94d5cb68d8a19fb5330adc8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.ml
+++ /dev/null
@@ -1,161 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* E-ACSL needs to access to the property status of every property (in
- particular for the option -e-acsl-valid). However, the necessary elements for
- building a property are copied/modified several times from the original
- project to the final project and the property statuses are destroyed when
- creating the intermediate projects; so there is no easy way to access to
- property statuses from the final project.
-
- This module aims at solving this issue by providing an access to property
- statuses from the final project. To work properly, it requires to visit every
- property during the final visit in the very same order than during the AST
- preparation visit. Indeed, for each function, it associates to each
- property an unique integer corresponding to its visit ordering. *)
-
-(* the kind is only used for a few additional consistency checks between [push]
- and [must_translate]*)
-type kind =
- | K_Assert
- | K_Invariant
- | K_Variant
- | K_StmtSpec
- | K_Allocation
- | K_Assigns
- | K_Decreases
- | K_Terminates
- | K_Complete
- | K_Disjoint
- | K_Requires
- | K_Ensures
-
-let _pretty_kind fmt k =
- Format.fprintf fmt "%s"
- (match k with
- | K_Assert -> "assert"
- | K_Invariant -> "invariant"
- | K_Variant -> "variant"
- | K_StmtSpec -> "stmtspec"
- | K_Allocation -> "allocation"
- | K_Assigns -> "assigns"
- | K_Decreases -> "decreases"
- | K_Terminates -> "terminates"
- | K_Complete -> "complete"
- | K_Disjoint -> "disjoint"
- | K_Requires -> "requires"
- | K_Ensures -> "ensures")
-
-(* information attached to every kernel_function containing an annotation *)
-type kf_info =
- { mutable cpt: int
- (* counter building the relationship between [push] and [must_translate] *);
- mutable statuses: (kind * bool) Datatype.Int.Map.t
- (* map associating a property as an integer to its kind and status
- ([true] = proved) *) }
-
-(* statuses for each function represented by its name (because the [kf] itself
- changes from a project to another). *)
-let keep_status
- : kf_info Datatype.String.Hashtbl.t
- = Datatype.String.Hashtbl.create 17
-
-(* will contain the value of a few options from the original project
- in order to safely use them from the final project. *)
-let option_valid = ref false
-let option_check = ref false
-
-let clear () =
- Datatype.String.Hashtbl.clear keep_status;
- option_valid := Options.Valid.get ()
-
-let push kf kind ppt =
- (* Options.feedback "PUSHING %a for %a"
- pretty_kind kind
- Kernel_function.pretty kf;*)
- (* no registration when -e-acsl-check or -e-acsl-valid *)
- if not (!option_check || !option_valid) then
- let keep =
- let open Property_status in
- match get ppt with
- | Never_tried
- | Inconsistent _
- | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
- true
- | Best (True, _) ->
- false
- in
- let status = kind, keep in
- let name = Kernel_function.get_name kf in
- try
- let info = Datatype.String.Hashtbl.find keep_status name in
- info.cpt <- info.cpt + 1;
- info.statuses <- Datatype.Int.Map.add info.cpt status info.statuses
- with Not_found ->
- let info = { cpt = 1; statuses = Datatype.Int.Map.singleton 1 status } in
- Datatype.String.Hashtbl.add keep_status name info
-
-let before_translation () =
- (* reset all counters *)
- Datatype.String.Hashtbl.iter (fun _ info -> info.cpt <- 0) keep_status
-
-let must_translate _kf _kind = true
- (* Options.feedback "GETTING %a for %a"
- pretty_kind kind
- Kernel_function.pretty kf;*)
-(* !option_check
- ||
- !option_valid
- ||
- (* function contracts have been moved from the original function to its
- duplicate by [Dup_function] but they are still associated to the original
- function here *)
- let name = Functions.RTL.get_original_name kf in
- try
- let info =
- try Datatype.String.Hashtbl.find keep_status name
- with Not_found ->
- Options.fatal "[keep_status] unbound function" Datatype.String.pretty kf
- in
- info.cpt <- info.cpt + 1;
- let kind', keep =
- try Datatype.Int.Map.find info.cpt info.statuses
- with Not_found ->
- Options.fatal "[keep_status] unbound annotation (id %d)@ in function %a"
- info.cpt
- Kernel_function.pretty kf
- in
- (* check kind consistency in order to detect more abnormal behaviors *)
- if kind <> kind' then
- Options.fatal
- "[keep_status] incorrect kind '%a' (expected: '%a')@ in function %a"
- pretty_kind kind
- pretty_kind kind'
- Kernel_function.pretty kf;
- keep
- with Not_found -> true
-*)
-(*
-Local Variables:
-compile-command: "make -C ../../../../.."
-End:
-*)
diff --git a/src/plugins/e-acsl/src/project_initializer/keep_status.mli b/src/plugins/e-acsl/src/project_initializer/keep_status.mli
deleted file mode 100644
index 455662756b7abdf51f79185ee20d09bf03fddd8a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/project_initializer/keep_status.mli
+++ /dev/null
@@ -1,60 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Make the property statuses of the initial project accessible when
- doing the main translation *)
-
-type kind =
- | K_Assert
- | K_Invariant
- | K_Variant
- | K_StmtSpec
- | K_Allocation
- | K_Assigns
- | K_Decreases
- | K_Terminates (* TODO: should be removed: not part of the E-ACSL subset *)
- | K_Complete
- | K_Disjoint
- | K_Requires
- | K_Ensures
-
-val clear: unit -> unit
-(** to be called before any program transformation *)
-
-val push: Kernel_function.t -> kind -> Property.t -> unit
-(** store the given property of the given kind for the given function *)
-
-val before_translation: unit -> unit
-(** to be called just before injecting the code *)
-
-val must_translate: Kernel_function.t -> kind -> bool
-(** To be called just before transforming a property of the given kind for the
- given function.
- VERY IMPORTANT: the property of the n-th call to this function exactly
- correspond to the n-th pushed property (see {!push}).
- @return true if and only if the translation must occur. *)
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 57458a5688878cb8930006420b56b818aa7905d5..f5e31c7949f347cb4d850ad9ceed30c119dbe2e4 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -345,103 +345,6 @@ class prepare_visitor = object (self)
| TFun(_, _, variadic, _) -> variadic
| _ -> true
- (* IMPORTANT: for keeping property statuses, we must preserve the ordering of
- translation, see function [Translate.translate_pre_spec] and
- [Translate.translate_post_spec]: be careful when modifying it. *)
-
- method private push_pre_spec s =
- let kf = Extlib.the self#current_kf in
- let kinstr = self#current_kinstr in
- let open Keep_status in
- Extlib.may
- (fun v -> push kf K_Decreases (Property.ip_of_decreases kf kinstr v))
- s.spec_variant;
- Extlib.may
- (fun t -> push kf K_Terminates (Property.ip_of_terminates kf kinstr t))
- s.spec_terminates;
- List.iter
- (fun l ->
- push kf K_Complete (Property.ip_of_complete kf kinstr ~active:[] l))
- s.spec_complete_behaviors;
- List.iter
- (fun l ->
- push kf K_Disjoint (Property.ip_of_disjoint kf kinstr ~active:[] l))
- s.spec_disjoint_behaviors;
- List.iter
- (fun b ->
- List.iter
- (fun p -> push kf K_Requires (Property.ip_of_requires kf kinstr b p))
- b.b_requires)
- s.spec_behavior
-
- method private push_post_spec spec =
- let do_behavior b =
- let kf = Extlib.the self#current_kf in
- let ki = match self#current_stmt with
- | None -> Kglobal
- | Some stmt -> Kstmt stmt
- in
- let open Keep_status in
- Extlib.may
- (push kf K_Assigns)
- (Property.ip_of_assigns
- kf
- ki
- (Property.Id_contract (Datatype.String.Set.empty (* TODO *), b))
- b.b_assigns);
- List.iter
- (fun p -> push kf K_Ensures (Property.ip_of_ensures kf ki b p))
- b.b_post_cond
- in
- (* fix ordering of behaviors' iterations *)
- let bhvs =
- List.sort
- (fun b1 b2 -> String.compare b1.b_name b2.b_name)
- spec.spec_behavior
- in
- List.iter do_behavior bhvs
-
- method private push_pre_code_annot a =
- let kf = Extlib.the self#current_kf in
- let stmt = Extlib.the self#current_stmt in
- let push_single k a =
- Keep_status.push kf k (Property.ip_of_code_annot_single kf stmt a)
- in
- let open Keep_status in
- match a.annot_content with
- | AAssert _ -> push_single K_Assert a
- | AStmtSpec(_ (* TODO *), s) -> self#push_pre_spec s
- | AInvariant _ -> push_single K_Invariant a
- | AVariant v ->
- push kf K_Variant (Property.ip_of_decreases kf (Kstmt stmt) v)
- | AAssigns _ ->
- (* TODO: should be a postcondition, but considered as an unhandled
- precondition in translate.ml right now; and we need to preserve the
- same ordering *)
- Extlib.may
- (push kf K_Assigns)
- (Property.ip_assigns_of_code_annot kf (Kstmt stmt) a)
- | AAllocation(_ (* TODO *), alloc) ->
- Extlib.may
- (push kf K_Allocation)
- (Property.ip_of_allocation kf (Kstmt stmt) (Property.Id_loop a) alloc)
- | APragma _ ->
- (* not yet translated *)
- ()
- | AExtended _ ->
- (* never translate extensions *)
- ()
-
- method private push_post_code_annot a = match a.annot_content with
- | AStmtSpec(_ (* TODO *), s) -> self#push_post_spec s
- | AAssert _
- | AInvariant _
- | AVariant _
- | AAssigns _
- | AAllocation _
- | APragma _
- | AExtended _ -> ()
-
(* ---------------------------------------------------------------------- *)
(* visitor's method overloading *)
(* ---------------------------------------------------------------------- *)
@@ -487,17 +390,6 @@ class prepare_visitor = object (self)
else
Cil.DoChildren
- method !vstmt_aux stmt =
- Annotations.iter_code_annot
- (fun _ a -> self#push_pre_code_annot a)
- stmt;
- Cil.DoChildrenPost
- (fun _ ->
- Annotations.iter_code_annot
- (fun _ a -> self#push_post_code_annot a)
- stmt;
- stmt)
-
method !vfunc fundec =
Cil.DoChildrenPost
(fun _ ->
@@ -557,9 +449,6 @@ class prepare_visitor = object (self)
Printer.pp_varinfo vi
| GFun _ -> ()
| _ -> assert false);
- let spec = Annotations.funspec ~populate:false kf in
- self#push_pre_spec spec;
- self#push_post_spec spec;
let tmp = vi.vname in
if tmp = "main" then begin
(* the new function becomes the new main: *)
@@ -580,7 +469,7 @@ class prepare_visitor = object (self)
dup_global
loc
self#get_filling_actions
- spec
+ (Annotations.funspec ~populate:false kf)
self#behavior
sound_verdict_vi
kf
@@ -599,19 +488,6 @@ class prepare_visitor = object (self)
when Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi ->
Cil.DoChildren
- | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when not (self#is_variadic_function vi)
- ->
- assert (* handled by the 2 cases above *)
- (not (Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi));
- let kf = Extlib.the self#current_kf in
- let s = Annotations.funspec ~populate:false kf in
- Cil.DoChildrenPost
- (fun f ->
- self#push_pre_spec s;
- self#push_post_spec s;
- f)
-
| _ ->
Cil.DoChildren
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index 5237a7d39d59ca87564a0f4d6329972f641c9f42..65ea62daf1854443f8523737c7f519d9e18e9dd6 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -25,7 +25,6 @@
More precisely, this module performs the following tasks:
- generating a new definition for functions with contract;
- removing term sharing;
- - storing what is necessary to translate in [Keep_status];
- in case of temporal validity checks, adding the attribute "aligned" to
variables that are not sufficiently aligned. *)