diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index a76fdee561c4288a70fd4b3473fd29e6caf5ef14..18775a69119b68f9bba8f09368c3653ef11a193f 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -57,6 +57,7 @@
/tests/runtime/*.cm*
/tests/runtime/result/*
/tests/temporal/result/*
+/tests/special/result/*
/tests/no-main/result/*
/tests/full-mmodel/result/*
/tests/bts/result/*
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index f587123e589abdeb13e35f45c7daec5dd496b81b..013bcefbcf7da9d4fd64bfc6ed2cde4294a2bff1 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -69,6 +69,7 @@ PLUGIN_CMO:= local_config \
exit_points \
label \
env \
+ keep_status \
dup_functions \
interval \
typing \
@@ -129,7 +130,7 @@ $(EACSL_PLUGIN_DIR)/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_F
ifeq (@MAY_RUN_TESTS@,yes)
-PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main full-mmodel temporal
+PLUGIN_TESTS_DIRS := reject runtime bts gmp no-main full-mmodel temporal special
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
E_ACSL_TESTS: $(EACSL_PLUGIN_DIR)/tests/test_config
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index b080ed4c2a5a8b2c1632a6076814833e951b74ae..1fe2370039081e0179c86ab846df2a68d00d8abd 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2017/11/27] Restore behavior of option -e-acsl-valid broken
+ since Phosphorus (included).
-* E-ACSL [2017/10/25] Fix bug #2303 about unnamed formals in
annotated functions.
- E-ACSL [2017/06/10] Add --free-valid-address option to e-acsl.gcc.sh
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 9d330878ff321b82be59f130950bb863b3eb7ff5..9a74392d6f07d1c83b8aaeccf86dff4c4db1c004 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -29,7 +29,6 @@ let dkey = Options.dkey_dup
(* ********************************************************************** *)
let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
-let is_generated kf = Kernel_function.Hashtbl.mem fct_tbl kf
let actions = Queue.create ()
@@ -51,51 +50,10 @@ let reset () =
Global.reset ();
Queue.clear actions
-(* ********************************************************************** *)
-(* Duplicating property statuses *)
-(* ********************************************************************** *)
-
-let reemit = function
- | Property.IPBehavior _ | Property.IPAxiom _ | Property.IPAxiomatic _
- | Property.IPPredicate (Property.PKAssumes _, _, _, _) -> false
- | _ -> true
-
-let copy_ppt old_prj new_prj old_ppt new_ppt =
- let module P = Property_status in
- let selection = State_selection.of_list [ P.self; Emitter.self ] in
- let emit s l =
- Project.on ~selection new_prj
- (fun s ->
- let e = match l with [] -> assert false | e :: _ -> e in
- let emitter = Emitter.Usable_emitter.get e.P.emitter in
- match s with
- | P.True | P.False_and_reachable | P.Dont_know ->
- P.emit emitter ~hyps:e.P.properties new_ppt s
- | P.False_if_reachable ->
- (* in that case, the only hypothesis is "Reachable new_ppt" which must
- be automatically added by the kernel *)
- P.emit emitter ~hyps:[] new_ppt P.False_if_reachable)
- s
- in
- let copy () =
- match Project.on ~selection old_prj P.get old_ppt with
- | P.Never_tried -> ()
- | P.Best(s, l) -> emit s l
- | P.Inconsistent i ->
- emit P.True i.P.valid;
- emit P.False_and_reachable i.P.invalid
- in
- if reemit old_ppt && not (Options.Valid.get ()) then Queue.add copy actions
-
(* ********************************************************************** *)
(* Duplicating functions *)
(* ********************************************************************** *)
-let dup_spec_status old_prj kf new_kf old_spec new_spec =
- let old_ppts = Property.ip_of_spec kf Kglobal ~active:[] old_spec in
- let new_ppts = Property.ip_of_spec new_kf Kglobal ~active:[] new_spec in
- List.iter2 (copy_ppt old_prj (Project.current ())) old_ppts new_ppts
-
let dup_funspec tbl bhv spec =
(* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
let o = object
@@ -205,7 +163,7 @@ let dup_fundec loc spec bhv kf vi new_vi =
sallstmts = [];
sspec = new_spec }
-let dup_global loc old_prj spec bhv kf vi new_vi =
+let dup_global loc actions spec bhv kf vi new_vi =
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
let fundec = dup_fundec loc spec bhv kf vi new_vi in
@@ -216,8 +174,34 @@ let dup_global loc old_prj spec bhv kf vi new_vi =
Globals.Functions.register new_kf;
Globals.Functions.replace_by_definition new_spec fundec loc;
Annotations.register_funspec new_kf;
- dup_spec_status old_prj kf new_kf spec new_spec;
Options.feedback ~dkey ~level:2 "function %s" name;
+ (* remove the specs attached to the previous kf iff it is a definition:
+ it is necessary to keep stable the number of annotations in order to get
+ [Keep_status] working fine. *)
+ let kf = Cil.get_kernel_function bhv kf in
+ if Kernel_function.is_definition kf then begin
+ Queue.add
+ (fun () ->
+ let bhvs =
+ Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
+ in
+ List.iter
+ (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
+ bhvs;
+ Annotations.iter_decreases
+ (fun e _ -> Annotations.remove_decreases e kf)
+ kf;
+ Annotations.iter_terminates
+ (fun e _ -> Annotations.remove_terminates e kf)
+ kf;
+ Annotations.iter_complete
+ (fun e l -> Annotations.remove_complete e kf l)
+ kf;
+ Annotations.iter_disjoint
+ (fun e l -> Annotations.remove_disjoint e kf l)
+ kf)
+ actions
+ end;
GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
(* ********************************************************************** *)
@@ -258,22 +242,7 @@ class dup_functions_visitor prj = object (self)
| Memory_model -> before_memory_model <- Code
| Code -> ()
- method !vcode_annot a =
- Cil.JustCopyPost
- (fun a' ->
- let get_ppt kf stmt a = Property.ip_of_code_annot kf stmt a in
- let kf = Extlib.the self#current_kf in
- let stmt = Extlib.the self#current_stmt in
- List.iter2
- (fun p p' -> copy_ppt (Project.current ()) prj p p')
- (get_ppt kf stmt a)
- (get_ppt
- (Cil.get_kernel_function self#behavior kf)
- (Cil.get_stmt self#behavior stmt)
- a');
- a')
-
- method !vlogic_info_decl li =
+ method !vlogic_info_decl li =
Global.add_logic_info li;
Cil.JustCopy
@@ -338,8 +307,15 @@ if there are memory-related annotations.@]"
let spec = Annotations.funspec ~populate:false kf in
let vi_bhv = Cil.get_varinfo self#behavior vi in
let new_g, new_decl =
- Project.on prj
- (dup_global loc (Project.current ()) spec self#behavior kf vi_bhv)
+ Project.on
+ prj
+ (dup_global
+ loc
+ self#get_filling_actions
+ spec
+ self#behavior
+ kf
+ vi_bhv)
new_vi
in
(* postpone the introduction of the new function definition to the
diff --git a/src/plugins/e-acsl/dup_functions.mli b/src/plugins/e-acsl/dup_functions.mli
index 3ac1e612b3fad6cbd09c1c0dd8b7f5bffedc8534..2f2b51bf6719c0924a0617352f89bc3a4fd945c8 100644
--- a/src/plugins/e-acsl/dup_functions.mli
+++ b/src/plugins/e-acsl/dup_functions.mli
@@ -20,10 +20,7 @@
(* *)
(**************************************************************************)
-open Cil_types
-
val dup: unit -> Project.t
-val is_generated: kernel_function -> bool
(*
Local Variables:
diff --git a/src/plugins/e-acsl/keep_status.ml b/src/plugins/e-acsl/keep_status.ml
new file mode 100644
index 0000000000000000000000000000000000000000..684dc2307407b1e06d4b3f74032f5b587199f564
--- /dev/null
+++ b/src/plugins/e-acsl/keep_status.ml
@@ -0,0 +1,150 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2017 *)
+(* 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 ();
+ option_check := Options.Check.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 =
+(* 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 = Misc.get_original_name kf in
+ 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)" info.cpt
+ in
+ (* check kind consistency in order to detect more abnormal behaviors *)
+ if kind <> kind' then
+ Options.fatal "[keep_status] incorrect kind '%a' (expected: '%a')"
+ pretty_kind kind
+ pretty_kind kind';
+ keep
diff --git a/src/plugins/e-acsl/keep_status.mli b/src/plugins/e-acsl/keep_status.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5b863270be7438368297921ff200f85207a1ee7b
--- /dev/null
+++ b/src/plugins/e-acsl/keep_status.mli
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2017 *)
+(* 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 the main translation *)
+
+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. *)
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 18115a3f14ee0aca703e44510f85435f7709210d..247fb18dc5bf9c2dc14d7fc2cad0d2bd9ee49705 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/src/plugins/e-acsl/main.ml
@@ -135,7 +135,7 @@ module Resulting_projects =
(struct
let name = "E-ACSL resulting projects"
let size = 7
- let dependencies = [ Ast.self ]
+ let dependencies = Ast.self :: Options.parameter_states
end)
let () =
@@ -249,6 +249,7 @@ 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/misc.ml b/src/plugins/e-acsl/misc.ml
index 8a646f14934195fbd8486dee51f35e1ff2c797a2..a2b7839793bd136c46d6529d522d08281cd4f158 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -138,7 +138,7 @@ let is_generated_kf kf =
let name = Kernel_function.get_vi kf in
is_generated_varinfo name
-let get_orig_name kf =
+let get_original_name kf =
let name = Kernel_function.get_name kf in
strip_prefix e_acsl_gen_prefix name
@@ -164,7 +164,7 @@ let mk_e_acsl_guard ?(reverse=false) kind kf e p =
(mk_api_name "assert")
[ e;
kind_to_string loc kind;
- Cil.mkString ~loc (get_orig_name kf);
+ Cil.mkString ~loc (get_original_name kf);
Cil.mkString ~loc msg;
Cil.integer loc line ]
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 437b1b98a3e627b6c01ff337994befbbc8b7627b..e4f11509b1639aa8909758474e256c4f6d0a50c6 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -122,6 +122,10 @@ val is_generated_literal_string_varinfo: varinfo -> bool
val is_generated_kf: kernel_function -> bool
(** Same as [is_generated_varinfo] but for kernel functions *)
+val get_original_name: kernel_function -> string
+(** @return the original basename of a function for generated functions, or the
+ identify for ungenerated ones. *)
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index 726cf32f2065154ed69b84ff620c9648c0ab210d..0d0466fcba11a22d080f23ce8c43eb06ce4a1f3c 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -119,6 +119,13 @@ let version () =
end
let () = Cmdline.run_after_configuring_stage version
+let parameter_states =
+ [ Valid.self;
+ Gmp_only.self;
+ Full_mmodel.self;
+ Builtins.self;
+ Temporal_validity.self]
+
let must_visit () = Run.get () || Check.get ()
let dkey_analysis = register_category "analysis"
diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli
index bfd8342cf004a6a6de3a0d485f07e0c04c029fe9..09ec5522a344a2337edcbf04e33153d05e1fd633 100644
--- a/src/plugins/e-acsl/options.mli
+++ b/src/plugins/e-acsl/options.mli
@@ -32,6 +32,8 @@ module Project_name: Parameter_sig.String
module Builtins: Parameter_sig.String_set
module Temporal_validity: Parameter_sig.Bool
+val parameter_states: State.t list
+
val must_visit: unit -> bool
val dkey_analysis: Log.category
diff --git a/src/plugins/e-acsl/prepare_ast.ml b/src/plugins/e-acsl/prepare_ast.ml
index f67f04117572065772b9404fffd676847195177f..a0a20e405372bf19b61de04145bdf0acc0d9d411 100644
--- a/src/plugins/e-acsl/prepare_ast.ml
+++ b/src/plugins/e-acsl/prepare_ast.ml
@@ -58,7 +58,7 @@ let sufficiently_aligned attrs algn =
let require_alignment typ attrs algn =
Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
-class prepare_visitor prj = object (_)
+class prepare_visitor prj = object (self)
inherit Visitor.frama_c_copy prj
(* Add align attributes to local variables (required by temporal analysis) *)
@@ -66,32 +66,153 @@ class prepare_visitor prj = object (_)
if Temporal.is_enabled () then
Cil.DoChildrenPost (fun blk ->
List.iter (fun vi ->
- (* 4 bytes alignment is required to allow sufficient space for storage
- of 32-bit timestamps in a 1:1 shadow. *)
+ (* 4 bytes alignment is required to allow sufficient space for storage
+ of 32-bit timestamps in a 1:1 shadow. *)
if require_alignment vi.vtype vi.vattr 4; then begin
vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
end)
- blk.blocals;
- blk)
+ blk.blocals;
+ blk)
else
Cil.DoChildren
+ (* 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 a 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 _ -> ()
+
(* Move variable declared in the body of a switch statement to the outer
scope *)
- method !vstmt_aux _ =
- Cil.DoChildrenPost (fun stmt ->
- match stmt.skind with
- | Switch(_,sw_blk,_,_) ->
- let new_blk = Cil.mkBlock [ stmt ] in
- let new_stmt = Cil.mkStmt (Block new_blk) in
- new_blk.blocals <- sw_blk.blocals;
- sw_blk.blocals <- [];
- new_stmt
- | _ -> stmt)
-
- initializer
- Project.copy ~selection:(Parameter_state.get_selection ()) prj
-end
+ method !vstmt_aux init_stmt =
+ Annotations.iter_code_annot
+ (fun _ a -> self#push_pre_code_annot a)
+ init_stmt;
+ Cil.DoChildrenPost
+ (fun stmt ->
+ Annotations.iter_code_annot
+ (fun _ a -> self#push_post_code_annot a)
+ init_stmt;
+ match stmt.skind with
+ | Switch(_,sw_blk,_,_) ->
+ let new_blk = Cil.mkBlock [ stmt ] in
+ let new_stmt = Cil.mkStmt (Block new_blk) in
+ new_blk.blocals <- sw_blk.blocals;
+ sw_blk.blocals <- [];
+ new_stmt
+ | _ -> stmt)
+
+ method private is_unvariadic_function vi =
+ match Cil.unrollType vi.vtype with
+ | TFun(_, _, variadic, _) -> not variadic
+ | _ -> false
+
+ method !vglob_aux = function
+ | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
+ when self#is_unvariadic_function vi
+ && not (Misc.is_library_loc loc)
+ && not (Cil.is_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
+
+ initializer Project.copy ~selection:(Parameter_state.get_selection ()) prj
+
+ end
let prepare () =
Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
diff --git a/src/plugins/e-acsl/prepare_ast.mli b/src/plugins/e-acsl/prepare_ast.mli
index f1ad742fab66ef0efd035baa8121dd9c66fe97f0..29af15182ef7cfec6aead0718095d4c21aeb10c1 100644
--- a/src/plugins/e-acsl/prepare_ast.mli
+++ b/src/plugins/e-acsl/prepare_ast.mli
@@ -21,9 +21,10 @@
(**************************************************************************)
(** Prepare AST for E-ACSL generation.
- * So for this mudule performs the only task:
- * - Move declarations of variables declared in the bodies of switch
- * statements to upper scopes.
-*)
+
+ So for this mudule performs two tasks:
+ - move declarations of variables declared in the bodies of switch
+ statements to upper scopes;
+ - store what is necessary to translate in [Keep_status]. *)
val prepare: unit -> Project.t
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index 44f7f5d0c9ee05e8447d0a5a0a549a6385cef47b..63d40a91360f0e872180541f239014e2138af477 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,6 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
index fd4f79bbeeddfce2d1453e31edd9e45174ec8964..7ad53f43ba46316c8f4ae40bb595517ab42aee16 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
@@ -2,5 +2,7 @@
[e-acsl] warning: annotating undefined function `atoi':
the generated program may miss memory instrumentation
if there are memory-related annotations.
+FRAMAC_SHARE/libc/stdlib.h:76:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index caa221c7af4e0b90fcc074663440e0a315d67ca1..bf5e66ec057ee972ef969f95c4fdff161a156f1d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -12,16 +12,6 @@
*/
void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out);
-/*@ requires \valid(Mtmax_in);
- requires \valid(Mwmax);
- requires \valid(Mtmax_out);
-
- behavior OverEstimate_Motoring:
- assumes \true;
- ensures
- *\old(Mtmax_out) ≡
- *\old(Mtmax_in) + (5 - ((5 / 80) * *\old(Mwmax)) * 0.4);
- */
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
__e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
@@ -49,17 +39,6 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
*/
void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out);
-/*@ requires \valid(Mtmin_in);
- requires \valid(Mwmin);
- requires \valid(Mtmin_out);
-
- behavior UnderEstimate_Motoring:
- assumes \true;
- ensures
- *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85 * *\old(Mwmin)?
- *\old(Mtmin_in) ≢ 0.:
- 0.85 * *\old(Mwmin) ≢ 0.;
- */
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
__e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 15d4cac23157437357e95845df2697bc0d418868..71e2577f0495344831130a35a68205d1d722703d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -6,10 +6,6 @@
*/
int __gen_e_acsl_sorted(int *t, int n);
-/*@ behavior yes:
- assumes ∀ int i; 0 < i < n ⇒ *(t + (i - 1)) ≤ *(t + i);
- ensures \result ≡ 1;
- */
int sorted(int *t, int n)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index a42da3e57acdae4ac55af81018c081955c8454d1..7185b9bfd07b25badaf02101ba912c7bf58fb607 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -11,13 +11,6 @@ typedef int ArrayInt[5];
void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
int *AverageAccel);
-/*@ ensures
- *\old(AverageAccel) ≡
- (((((*\old(Accel))[4] + (*\old(Accel))[3]) + (*\old(Accel))[2]) +
- (*\old(Accel))[1])
- + (*\old(Accel))[0])
- / 5;
- */
void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
{
__e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index 302c3300239726a0a820d3994caa18b325329cab..9a0f79b306fb0d4ca48e5d9378ec76722cad1a18 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -3,7 +3,6 @@
/*@ requires n > 0; */
int __gen_e_acsl_fact(int n);
-/*@ requires n > 0; */
int fact(int n)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index d7ada2c7115bd789170d9402edb44f320bf154f5..c8a9cb14b211e3c564949587c33bf5668dfe4c79 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -10,10 +10,6 @@ int global_i = 0;
*/
void __gen_e_acsl_loop(void);
-/*@ requires global_i ≡ 0;
- requires \valid(global_i_ptr);
- requires global_i_ptr ≡ &global_i;
- */
void loop(void)
{
return;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index 50e175fcb044acba4e3d318107f89dc288c160a6..4ca30ec02ab347dc3f46813193f65902c9e8d7e9 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -4,7 +4,6 @@ int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);
-/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
int __gen_e_acsl_at_4;
@@ -106,7 +105,6 @@ void g(int *p, int *q)
/*@ ensures \result ≡ \old(x); */
int __gen_e_acsl_h(int x);
-/*@ ensures \result ≡ \old(x); */
int h(int x)
{
__e_acsl_store_block((void *)(& x),(size_t)4);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 5b54cad0dde4309b9fc5cd75328f89681d8810fd..2031fd1929009beb0b6d0703dee14223bc4886e6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -4,7 +4,6 @@ int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);
-/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
__e_acsl_mpz_t __gen_e_acsl_at_3;
@@ -177,7 +176,6 @@ void g(int *p, int *q)
/*@ ensures \result ≡ \old(x); */
int __gen_e_acsl_h(int x);
-/*@ ensures \result ≡ \old(x); */
int h(int x)
{
__e_acsl_store_block((void *)(& x),(size_t)4);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
index fb79cdc60f5e835b8ddd42b063bdef8dcdc1db7c..d55ebd19849aec4566b46463b0f6b2f12cfcd735 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
@@ -4,6 +4,8 @@
if there are memory-related annotations.
tests/runtime/ctype_macros.c:39:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/ctype.h:164:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/ctype.h:164:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index 9c07803917ff166930e4aaab947b1ff10ebb2196..b8b425b657a046419140f6ad0c4e03f63840bc21 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -5,7 +5,6 @@ int Y = 2;
/*@ ensures X ≡ 1; */
void __gen_e_acsl_f(void);
-/*@ ensures X ≡ 1; */
void f(void)
{
X = 1;
@@ -16,8 +15,6 @@ void f(void)
ensures Y ≡ 2; */
void __gen_e_acsl_g(void);
-/*@ ensures X ≡ 2;
- ensures Y ≡ 2; */
void g(void)
{
X = 2;
@@ -27,7 +24,6 @@ void g(void)
/*@ requires X ≡ 2; */
void __gen_e_acsl_h(void);
-/*@ requires X ≡ 2; */
void h(void)
{
X ++;
@@ -38,8 +34,6 @@ void h(void)
requires Y ≡ 2; */
void __gen_e_acsl_i(void);
-/*@ requires X ≡ 3;
- requires Y ≡ 2; */
void i(void)
{
X += Y;
@@ -57,15 +51,6 @@ void i(void)
*/
void __gen_e_acsl_j(void);
-/*@ behavior b1:
- requires X ≡ 5;
- ensures X ≡ 3;
-
- behavior b2:
- requires X ≡ 3 + Y;
- requires Y ≡ 2;
- ensures X ≡ Y + 1;
- */
void j(void)
{
X = 3;
@@ -84,16 +69,6 @@ void j(void)
*/
void __gen_e_acsl_k(void);
-/*@ behavior b1:
- assumes X ≡ 1;
- requires X ≡ 0;
-
- behavior b2:
- assumes X ≡ 3;
- assumes Y ≡ 2;
- requires X ≡ 3;
- requires X + Y ≡ 5;
- */
void k(void)
{
X += Y;
@@ -103,7 +78,6 @@ void k(void)
/*@ ensures X ≡ 5; */
int __gen_e_acsl_l(void);
-/*@ ensures X ≡ 5; */
int l(void)
{
/*@ assert Y ≡ 2; */
@@ -123,16 +97,6 @@ int l(void)
*/
void __gen_e_acsl_m(void);
-/*@ behavior b1:
- assumes X ≡ 7;
- ensures X ≡ 95;
-
- behavior b2:
- assumes X ≡ 5;
- assumes Y ≡ 2;
- ensures X ≡ 7;
- ensures X ≡ \old(X) + Y;
- */
void m(void)
{
X += Y;
@@ -152,17 +116,6 @@ void m(void)
*/
void __gen_e_acsl_n(void);
-/*@ requires X > 0;
- requires X < 10;
-
- behavior b1:
- assumes X ≡ 7;
- ensures X ≡ 8;
-
- behavior b2:
- assumes X ≡ 5;
- ensures X ≡ 98;
- */
void n(void)
{
X ++;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index 291fb0d05552c82f665cb5feb9008df5f8e35393..5a9054e4599ca792ef6b39bd44874eac89b9dd02 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -4,7 +4,6 @@ int X = 0;
/*@ ensures X ≡ 3; */
int main(void);
-/*@ ensures X ≡ 3; */
int __gen_e_acsl_main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 71d59a04e1783ac482a8725a2a34e6f0728e508a..14aa44c0aee38b3a7164c9279e72eb4ec0e13f4a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -13,16 +13,6 @@ int A[10];
*/
int __gen_e_acsl_search(int elt);
-/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i + 1];
-
- behavior exists:
- assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
- ensures \result ≡ 1;
-
- behavior not_exists:
- assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
- ensures \result ≡ 0;
- */
int search(int elt)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index e0791ac88cb29a81155f515ee9b2d1b302acc2cd..f2fa04cfb0fc425ef67bcc62838c348f123837ff 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -3,7 +3,6 @@
/*@ ensures \result ≡ (int)(\old(x) - \old(x)); */
int __gen_e_acsl_f(int x);
-/*@ ensures \result ≡ (int)(\old(x) - \old(x)); */
int f(int x)
{
x = 0;
@@ -14,7 +13,6 @@ int Y = 1;
/*@ ensures \result ≡ Y; */
int __gen_e_acsl_g(int x);
-/*@ ensures \result ≡ Y; */
int g(int x)
{
return x;
@@ -23,7 +21,6 @@ int g(int x)
/*@ ensures \result ≡ 0; */
int __gen_e_acsl_h(void);
-/*@ ensures \result ≡ 0; */
int h(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
index 535deea6a82d7ec6c5b4d05e868a04a634798c36..84e47332b50fc927bca65abef979455f04de93f7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
@@ -2,10 +2,7 @@
[e-acsl] translation done in project "e-acsl".
tests/runtime/linear_search.i:7:[value] warning: function __gen_e_acsl_search: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/linear_search.i:7:[value] warning: function search: precondition got status unknown.
tests/runtime/linear_search.i:18:[value] warning: loop invariant got status unknown.
-tests/runtime/linear_search.i:10:[value] warning: function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/runtime/linear_search.i:13:[value] warning: function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/runtime/linear_search.i:10:[value] warning: function __gen_e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/runtime/linear_search.i:13:[value] warning: function __gen_e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/runtime/linear_search.i:31:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
index dee7ed535006155a87063f244e8b989a5985ef8e..a17600f826d5e9e8a2f8a4900495fcae1b11e574 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
@@ -10,9 +10,15 @@
if there are memory-related annotations.
tests/runtime/local_goto.c:37:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
+tests/runtime/local_goto.c:37:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
tests/runtime/local_goto.c:28:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
+tests/runtime/local_goto.c:28:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
tests/runtime/local_goto.c:16:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
+tests/runtime/local_goto.c:16:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-valid.c b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
new file mode 100644
index 0000000000000000000000000000000000000000..be1694738022e2984871d08c645726b2a932739f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
@@ -0,0 +1,41 @@
+/* run.config
+ COMMENT: test option -e-acsl-no-valid
+ LOG: gen_@PTEST_NAME@.c
+ OPT: -e-acsl-prepare -val -value-verbose 0 -machdep gcc_x86_64 -then -check -e-acsl-valid -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -value-verbose 0
+ EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ special "" "--frama-c=@frama-c@"
+ LOG: gen_@PTEST_NAME@2.c
+ OPT: -e-acsl-prepare -val -value-verbose 0 -machdep gcc_x86_64 -then -check -e-acsl-no-valid -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -value-verbose 0
+*/
+
+#include <stdlib.h>
+
+/*@ requires \valid(y);
+ @ requires *x >= 0;
+ @ ensures *x == \old(*x)+1;
+ @ assigns *x \from *x,x;
+ @ behavior b1:
+ @ assumes *y == 1;
+ @ assigns \nothing;
+ @ ensures *x < 0;
+ @ behavior b2:
+ @ assumes *x == 0;
+ @ ensures *x == 1;
+ @ complete behaviors;
+ @ disjoint behaviors b1, b2;
+ @ */
+void f(int *x, int *y) {
+ /*@ requires *x >= 0;
+ @ ensures 2 >= 1;
+ @ assigns *x; */
+ { (*x)++; }
+ /*@ loop invariant 0 <= i <= 1;
+ @ loop variant 2 - i; */
+ for(int i = 0; i < 1; i++) /*@ assert 1 == 1; */ /*@ assert \valid(y); */ ;
+}
+
+int main(void) {
+ int x = 0;
+ int *y = (int *)malloc(sizeof(int));
+ f(&x, y);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
index 44e9bd786985b1ba4cae2d2237a2b982b30e91e5..274bdbe69e1a2b66be3ef24030464585c4d743f5 100644
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
@@ -1,9 +1,5 @@
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/special/builtin.i (no preprocessing)
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
index 44e9bd786985b1ba4cae2d2237a2b982b30e91e5..274bdbe69e1a2b66be3ef24030464585c4d743f5 100644
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
@@ -1,9 +1,5 @@
-[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/special/builtin.i (no preprocessing)
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.err.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..41f53a3b493062ae9708bbe2efe3c53d374afb70
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
@@ -0,0 +1,15 @@
+tests/special/e-acsl-valid.c:12:[value] warning: function f: precondition got status unknown.
+tests/special/e-acsl-valid.c:19:[value] warning: function f, behavior b1: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+[e-acsl] beginning translation.
+tests/special/e-acsl-valid.c:27:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:28:[e-acsl] warning: E-ACSL construct `variant' is not yet supported. Ignoring annotation.
+tests/special/e-acsl-valid.c:31:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:31:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:22:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.err.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..95252981ffa598a1e6178a56b390ee677d80598a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
@@ -0,0 +1,15 @@
+tests/special/e-acsl-valid.c:12:[value] warning: function f: precondition got status unknown.
+tests/special/e-acsl-valid.c:19:[value] warning: function f, behavior b1: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+[e-acsl] beginning translation.
+tests/special/e-acsl-valid.c:27:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:28:[e-acsl] warning: E-ACSL construct `variant' is not yet supported. Ignoring annotation.
+tests/special/e-acsl-valid.c:28:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:28:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:12:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/special/e-acsl-valid.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
index 61c87805321645f1e886911b11e355a704edf69d..5119fca23dca60be72f4bffe6d695bdc26b1db2c 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
@@ -1,14 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int incr(int x);
/*@ ensures \result ≡ incr(\old(i)); */
int __gen_e_acsl_f(int i);
-/*@ ensures \result ≡ incr(\old(i)); */
int f(int i)
{
- int j;
- j = i + 1;
+ int j = i + 1;
return j;
}
@@ -22,8 +21,8 @@ int incr(int x)
int main(void)
{
int __retres;
- int i;
- i = __gen_e_acsl_f(2);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int i = __gen_e_acsl_f(2);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
index aa17b64f55f75476367f21007df9ae54eb47a823..f5fefba9aecb54b313f94ea0be09eccc55497cd8 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
@@ -1,14 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int incr(int x);
/*@ ensures \result ≡ incr(\old(i)); */
int __gen_e_acsl_f(int i);
-/*@ ensures \result ≡ incr(\old(i)); */
int f(int i)
{
- int j;
- j = i + 1;
+ int j = i + 1;
return j;
}
@@ -22,8 +21,8 @@ int incr(int x)
int main(void)
{
int __retres;
- int i;
- i = __gen_e_acsl_f(2);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int i = __gen_e_acsl_f(2);
__retres = 0;
return __retres;
}
@@ -36,15 +35,15 @@ int __gen_e_acsl_f(int i)
__gen_e_acsl_at = i;
__retres = f(i);
{
- mpz_t __gen_e_acsl_result;
+ __e_acsl_mpz_t __gen_e_acsl_result;
int __gen_e_acsl_incr_app;
- mpz_t __gen_e_acsl_app;
+ __e_acsl_mpz_t __gen_e_acsl_app;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
__gen_e_acsl_incr_app = incr(__gen_e_acsl_at);
__gmpz_init_set_si(__gen_e_acsl_app,(long)__gen_e_acsl_incr_app);
- __gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_result),
- (__mpz_struct const *)(__gen_e_acsl_app));
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_app));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
(char *)"\\result == incr(\\old(i))",12);
__gmpz_clear(__gen_e_acsl_result);
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
new file mode 100644
index 0000000000000000000000000000000000000000..9ec0221d8cca64df660dad187a97436976d01596
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
@@ -0,0 +1,208 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+/*@ requires \valid(y);
+ requires *x ≥ 0;
+ ensures *\old(x) ≡ \old(*x) + 1;
+ assigns *x;
+ assigns *x \from *x, x;
+
+ behavior b1:
+ assumes *y ≡ 1;
+ ensures *\old(x) < 0;
+ assigns \nothing;
+
+ behavior b2:
+ assumes *x ≡ 0;
+ ensures *\old(x) ≡ 1;
+
+ complete behaviors b2, b1;
+ disjoint behaviors b1, b2;
+ */
+void __gen_e_acsl_f(int *x, int *y);
+
+void f(int *x, int *y)
+{
+ /*@ requires *x ≥ 0;
+ ensures 2 ≥ 1;
+ assigns *x; */
+ {
+ {
+ int __gen_e_acsl_valid_read;
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(x)",27);
+ __e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
+ (char *)"*x >= 0",27);
+ }
+ __e_acsl_initialize((void *)x,sizeof(int));
+ (*x) ++;
+ __e_acsl_assert(2 >= 1,(char *)"Postcondition",(char *)"f",
+ (char *)"2 >= 1",28);
+ }
+ {
+ int i = 0;
+ /*@ loop variant 2 - i; */
+ {
+ {
+ int __gen_e_acsl_and;
+ if (0 <= i) __gen_e_acsl_and = i <= 1; else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",(char *)"f",
+ (char *)"0 <= i <= 1",31);
+ }
+ /*@ loop invariant 0 ≤ i ≤ 1; */
+ while (i < 1) {
+ /*@ assert 1 ≡ 1; */
+ __e_acsl_assert(1 == 1,(char *)"Assertion",(char *)"f",
+ (char *)"1 == 1",33);
+ /*@ assert \valid(y); */
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),
+ (void *)y,(void *)(& y));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"f",
+ (char *)"\\valid(y)",33);
+ }
+ {
+ int __gen_e_acsl_and_2;
+ i ++;
+ if (0 <= i) __gen_e_acsl_and_2 = i <= 1;
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Invariant",(char *)"f",
+ (char *)"0 <= i <= 1",31);
+ }
+ }
+ }
+ }
+ __e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int x = 0;
+ __e_acsl_store_block((void *)(& x),(size_t)4);
+ __e_acsl_full_init((void *)(& x));
+ int *y = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_full_init((void *)(& y));
+ __gen_e_acsl_f(& x,y);
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ requires \valid(y);
+ requires *x ≥ 0;
+ ensures *\old(x) ≡ \old(*x) + 1;
+ assigns *x;
+ assigns *x \from *x, x;
+
+ behavior b1:
+ assumes *y ≡ 1;
+ ensures *\old(x) < 0;
+ assigns \nothing;
+
+ behavior b2:
+ assumes *x ≡ 0;
+ ensures *\old(x) ≡ 1;
+
+ complete behaviors b2, b1;
+ disjoint behaviors b1, b2;
+ */
+void __gen_e_acsl_f(int *x, int *y)
+{
+ long __gen_e_acsl_at_6;
+ int *__gen_e_acsl_at_5;
+ int *__gen_e_acsl_at_4;
+ int __gen_e_acsl_at_3;
+ int *__gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
+ {
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
+ (void *)(& y));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
+ (char *)"\\valid(y)",12);
+ __e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
+ (char *)"*x >= 0",13);
+ }
+ {
+ int __gen_e_acsl_valid_read_5;
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(x)",14);
+ __gen_e_acsl_at_6 = (long)*x;
+ }
+ __gen_e_acsl_at_5 = x;
+ __gen_e_acsl_at_4 = x;
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(x)",21);
+ __gen_e_acsl_at_3 = *x == 0;
+ }
+ __gen_e_acsl_at_2 = x;
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)y,sizeof(int),
+ (void *)y,(void *)(& y));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(y)",17);
+ __gen_e_acsl_at = *y == 1;
+ }
+ f(x,y);
+ {
+ int __gen_e_acsl_implies;
+ int __gen_e_acsl_implies_2;
+ if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
+ else {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
+ sizeof(int),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",
+ 19);
+ __gen_e_acsl_implies = *__gen_e_acsl_at_2 < 0;
+ }
+ __e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",(char *)"f",
+ (char *)"\\old(*y == 1) ==> *\\old(x) < 0",19);
+ if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_2 = 1;
+ else {
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
+ sizeof(int),
+ (void *)__gen_e_acsl_at_4,
+ (void *)(& __gen_e_acsl_at_4));
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_4)",
+ 22);
+ __gen_e_acsl_implies_2 = *__gen_e_acsl_at_4 == 1;
+ }
+ __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
+ (char *)"f",(char *)"\\old(*x == 0) ==> *\\old(x) == 1",
+ 22);
+ __e_acsl_assert(*__gen_e_acsl_at_5 == __gen_e_acsl_at_6 + 1L,
+ (char *)"Postcondition",(char *)"f",
+ (char *)"*\\old(x) == \\old(*x) + 1",14);
+ __e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
+ return;
+ }
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
new file mode 100644
index 0000000000000000000000000000000000000000..dd54c01842d2331d7fd1b23586089b8cc434dd17
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
@@ -0,0 +1,141 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+/*@ requires \valid(y);
+ requires *x ≥ 0;
+ ensures *\old(x) ≡ \old(*x) + 1;
+ assigns *x;
+ assigns *x \from *x, x;
+
+ behavior b1:
+ assumes *y ≡ 1;
+ ensures *\old(x) < 0;
+ assigns \nothing;
+
+ behavior b2:
+ assumes *x ≡ 0;
+ ensures *\old(x) ≡ 1;
+
+ complete behaviors b2, b1;
+ disjoint behaviors b1, b2;
+ */
+void __gen_e_acsl_f(int *x, int *y);
+
+void f(int *x, int *y)
+{
+ /*@ requires *x ≥ 0;
+ ensures 2 ≥ 1;
+ assigns *x; */
+ {
+ {
+ int __gen_e_acsl_valid_read;
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(x)",27);
+ __e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
+ (char *)"*x >= 0",27);
+ }
+ __e_acsl_initialize((void *)x,sizeof(int));
+ (*x) ++;
+ __e_acsl_assert(2 >= 1,(char *)"Postcondition",(char *)"f",
+ (char *)"2 >= 1",28);
+ }
+ {
+ int i = 0;
+ /*@ loop invariant 0 ≤ i ≤ 1;
+ loop variant 2 - i; */
+ while (i < 1) {
+ /*@ assert 1 ≡ 1; */ ;
+ /*@ assert \valid(y); */ ;
+ i ++;
+ }
+ }
+ __e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ int x = 0;
+ __e_acsl_store_block((void *)(& x),(size_t)4);
+ __e_acsl_full_init((void *)(& x));
+ int *y = malloc(sizeof(int));
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_full_init((void *)(& y));
+ __gen_e_acsl_f(& x,y);
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ requires \valid(y);
+ requires *x ≥ 0;
+ ensures *\old(x) ≡ \old(*x) + 1;
+ assigns *x;
+ assigns *x \from *x, x;
+
+ behavior b1:
+ assumes *y ≡ 1;
+ ensures *\old(x) < 0;
+ assigns \nothing;
+
+ behavior b2:
+ assumes *x ≡ 0;
+ ensures *\old(x) ≡ 1;
+
+ complete behaviors b2, b1;
+ disjoint behaviors b1, b2;
+ */
+void __gen_e_acsl_f(int *x, int *y)
+{
+ int *__gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
+ {
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
+ (void *)(& y));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
+ (char *)"\\valid(y)",12);
+ }
+ __gen_e_acsl_at_2 = x;
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)y,sizeof(int),
+ (void *)y,(void *)(& y));
+ __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(y)",17);
+ __gen_e_acsl_at = *y == 1;
+ }
+ f(x,y);
+ {
+ int __gen_e_acsl_implies;
+ if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
+ else {
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
+ sizeof(int),
+ (void *)__gen_e_acsl_at_2,
+ (void *)(& __gen_e_acsl_at_2));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"f",
+ (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",
+ 19);
+ __gen_e_acsl_implies = *__gen_e_acsl_at_2 < 0;
+ }
+ __e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",(char *)"f",
+ (char *)"\\old(*y == 1) ==> *\\old(x) < 0",19);
+ __e_acsl_delete_block((void *)(& y));
+ __e_acsl_delete_block((void *)(& x));
+ return;
+ }
+}
+
+
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
index 1adfbf4c3325a5ac415b0ba674c6c4237c8c2c29..a184f0a503377e05cd1531e6742d2b52d8c0064f 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
@@ -4,4 +4,6 @@
if there are memory-related annotations.
tests/temporal/t_malloc-asan.c:31:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
+tests/temporal/t_malloc-asan.c:31:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index caf187356b86b329a85cb8fec3cf23af87b9f4c0..4da3a698ac4b3a1ae9c60a39bc653ea01101545d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -11,8 +11,6 @@ FRAMAC_SHARE/libc/string.h:82:[e-acsl] warning: E-ACSL construct `assigns clause
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:85:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:85:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
FRAMAC_SHARE/libc/string.h:60:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:61:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:62:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
@@ -20,6 +18,4 @@ FRAMAC_SHARE/libc/string.h:62:[e-acsl] warning: E-ACSL construct `assigns clause
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:65:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:65:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 7b6b7e4dd56892b218a5fbc162064d86789566a1..f2eb5dab38c2491a5cf4cfd64951ed37a11dd063 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -866,7 +866,10 @@ let term_to_exp typ t =
(* ************************************************************************** *)
(* [translate_*] translates a given ACSL annotation into the corresponding C
- statement (if any) for runtime assertion checking *)
+ 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] *)
(* ************************************************************************** *)
let assumes_predicate bhv =
@@ -881,26 +884,14 @@ let assumes_predicate bhv =
let original_project_ref = ref Project_skeleton.dummy
let set_original_project p = original_project_ref := p
-let must_translate ppt =
- let selection =
- State_selection.of_list [ Property_status.self; Options.Valid.self ]
- in
- Project.on ~selection
- !original_project_ref
- (fun ppt ->
- match Property_status.get ppt with
- | Property_status.Best(Property_status.True, _) -> Options.Valid.get ()
- | _ -> true)
- ppt
-
-let translate_preconditions kf kinstr env behaviors =
+let translate_preconditions kf env behaviors =
let env = Env.set_annotation_kind env Misc.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 must_translate (Property.ip_of_requires kf kinstr b p) then
+ if Keep_status.must_translate kf Keep_status.K_Requires then
let loc = p.ip_content.pred_loc in
let p =
Logic_const.pimplies
@@ -918,24 +909,25 @@ let translate_preconditions kf kinstr env behaviors =
in
List.fold_left do_behavior env behaviors
-let translate_postconditions kf kinstr env behaviors =
+let translate_postconditions kf env behaviors =
let env = Env.set_annotation_kind env Misc.Postcondition in
- (* generate one guard by postcondition of each behavior *)
+ (* 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
+ then not_yet env "assigns clause in behavior";
+ (* ignore b.b_extended since we never translate them *)
+ env)
+ env
+ in
let assumes_pred = assumes_predicate b in
List.fold_left
- (fun env (t, p as post) ->
- if must_translate (Property.ip_of_ensures kf kinstr b post) then
- let env =
- handle_error
- (fun env ->
- if b.b_assigns <> WritesAny then
- not_yet env "assigns clause in behavior";
- if b.b_extended <> [] then
- not_yet env "grammar extensions in behavior";
- env)
- env
- in
+ (fun env (t, p) ->
+ if Keep_status.must_translate kf Keep_status.K_Ensures then
let do_it env =
match t with
| Normal ->
@@ -956,57 +948,62 @@ let translate_postconditions kf kinstr env behaviors =
env
b.b_post_cond
in
- List.fold_left do_behavior env behaviors
+ (* fix ordering of behaviors' iterations *)
+ let bhvs =
+ List.sort (fun b1 b2 -> String.compare b1.b_name b2.b_name) behaviors
+ in
+ List.fold_left do_behavior env bhvs
-let translate_pre_spec kf kinstr env spec =
+let translate_pre_spec kf 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 v ->
- if must_translate (Property.ip_of_decreases kf kinstr v) then
- not_yet env "variant clause"))
+ (fun _ ->
+ if Keep_status.must_translate kf Keep_status.K_Decreases then
+ not_yet env "variant clause"))
spec.spec_variant;
+ (* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
unsupported
(Extlib.may
- (fun t ->
- if must_translate (Property.ip_of_terminates kf kinstr t) then
- not_yet env "terminates clause"))
+ (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 l ->
- if must_translate (Property.ip_of_complete kf kinstr ~active:[] l)
- then not_yet env "complete behaviors"))
+ (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 l ->
- if must_translate (Property.ip_of_disjoint kf kinstr ~active:[] l)
- then not_yet env "disjoint behaviors"))
+ (fun _ ->
+ if Keep_status.must_translate kf Keep_status.K_Disjoint then
+ not_yet env "disjoint behaviors"))
l);
env
in
let env = convert_unsupported_clauses env in
handle_error
- (fun env -> translate_preconditions kf kinstr env spec.spec_behavior)
+ (fun env -> translate_preconditions kf env spec.spec_behavior)
env
-let translate_post_spec kf kinstr env spec =
+let translate_post_spec kf env spec =
handle_error
- (fun env -> translate_postconditions kf kinstr env spec.spec_behavior)
+ (fun env -> translate_postconditions kf env spec.spec_behavior)
env
-let translate_pre_code_annotation kf stmt env annot =
+let translate_pre_code_annotation kf env annot =
let convert env = match annot.annot_content with
| AAssert(l, p) ->
- if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+ if Keep_status.must_translate kf Keep_status.K_Assert then
let env = Env.set_annotation_kind env Misc.Assertion in
if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
@@ -1016,9 +1013,9 @@ let translate_pre_code_annotation kf stmt env annot =
| AStmtSpec(l, spec) ->
if l <> [] then
not_yet env "@[statement contract applied only on some behaviors@]";
- translate_pre_spec kf (Kstmt stmt) env spec ;
+ translate_pre_spec kf env spec ;
| AInvariant(l, loop_invariant, p) ->
- if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+ if Keep_status.must_translate kf Keep_status.K_Invariant then
let env = Env.set_annotation_kind env Misc.Invariant in
if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
@@ -1027,15 +1024,16 @@ let translate_pre_code_annotation kf stmt env annot =
else
env
| AVariant _ ->
- if must_translate (Property.ip_of_code_annot_single kf stmt annot)
+ if Keep_status.must_translate kf Keep_status.K_Variant
then not_yet env "variant"
else env
| AAssigns _ ->
- if must_translate (Property.ip_of_code_annot_single kf stmt annot)
+ (* TODO: it is not a precondition *)
+ if Keep_status.must_translate kf Keep_status.K_Assigns
then not_yet env "assigns"
else env
| AAllocation _ ->
- if must_translate (Property.ip_of_code_annot_single kf stmt annot)
+ if Keep_status.must_translate kf Keep_status.K_Allocation
then not_yet env "allocation"
else env
| APragma _ -> not_yet env "pragma"
@@ -1043,9 +1041,9 @@ let translate_pre_code_annotation kf stmt env annot =
in
handle_error convert env
-let translate_post_code_annotation kf stmt env annot =
+let translate_post_code_annotation kf env annot =
let convert env = match annot.annot_content with
- | AStmtSpec(_, spec) -> translate_post_spec kf (Kstmt stmt) env spec
+ | AStmtSpec(_, spec) -> translate_post_spec kf env spec
| AAssert _
| AInvariant _
| AVariant _
diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli
index 56a484dccc2fc13ec73dc4c4a618b320720879d0..9fa04a7600d3e8095a601ef0fcd224f8efb547dc 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/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 -> 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 -> stmt -> Env.t -> code_annotation -> Env.t
-val translate_post_code_annotation:
- kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
+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_code_annotation:
+ kernel_function -> Env.t -> code_annotation -> Env.t
+val translate_post_code_annotation:
+ kernel_function -> Env.t -> code_annotation -> Env.t
val translate_named_predicate:
kernel_function -> Env.t -> predicate -> Env.t
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index b8582fe2960e7529af5195f5d15b11ee09b6e87e..c475f5398ba460fc68eb60321f3d0e6640c71ca3 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -552,10 +552,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
env
in
(* translate the precondition of the function *)
- if Dup_functions.is_generated (Extlib.the self#current_kf) then
- Project.on prj (Translate.translate_pre_spec kf Kglobal env) !funspec
- else
- env
+ Project.on prj (Translate.translate_pre_spec kf env) !funspec
else
env
in
@@ -569,10 +566,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Cil.visitCilCodeAnnotation (self :> Cil.cilVisitor) old_a
in
let env =
- Project.on
- prj
- (Translate.translate_pre_code_annotation kf stmt env)
- a
+ Project.on prj (Translate.translate_pre_code_annotation kf env) a
in
env, a :: new_annots)
(Cil.get_original_stmt self#behavior stmt)
@@ -619,8 +613,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Project.on
prj
(List.fold_right
- (fun a env ->
- Translate.translate_post_code_annotation kf stmt env a)
+ (fun a env -> Translate.translate_post_code_annotation kf env a)
new_annots)
env
in
@@ -640,13 +633,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let env = mk_post_env env in
(* also handle the postcondition of the function and clear the env *)
let env =
- if Dup_functions.is_generated (Extlib.the self#current_kf) then
- Project.on
- prj
- (Translate.translate_post_spec kf Kglobal env)
- !funspec
- else
- env
+ Project.on prj (Translate.translate_post_spec kf env) !funspec
in
(* de-allocating memory previously allocating by the kf *)
(* JS: should be done in the new project? *)
@@ -848,8 +835,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
initializer
Misc.reset ();
Literal_strings.reset ();
+ Keep_status.before_translation ();
self#reset_env ();
Translate.set_original_project (Project.current ())
+
end
let do_visit ?(prj=Project.current ()) generate =