diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index f4c318a3f636251c9efc7a27e51920348fe06877..34c3eedf2810292cd710f11a00fb73a8fa03c704 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -28,6 +28,48 @@ module Dataflow = Dataflow2
let dkey = Options.Dkey.mtracking
module Error = Error.Make(struct let phase = dkey end)
+(* Some pointers (stdin, stdout, stderr, &errno) are special in the sense that
+ they need not be allocated, initialized, and in that they are not freeable,
+ and that some of them are statically known to be writeable/read-only.
+ There is no need to monitor the corresponding memory regions. *)
+module SpecialPointers = struct
+ type spec = {pointer : bool; freeable : bool; writeable : bool; initialized : bool}
+
+ let specs = [
+ "errno", {pointer = false; freeable = false; writeable = true; initialized = true};
+ "stdin", {pointer = true; freeable = false; writeable = false; initialized = true};
+ "stdout", {pointer = true; freeable = false; writeable = true; initialized = true};
+ "stderr", {pointer = true; freeable = false; writeable = true; initialized = true}
+ ]
+
+ let tbl = Varinfo.Hashtbl.create 5
+
+ let initialize () =
+ let add_builtin (name, spec) =
+ let name = if Kernel.FramaCStdLib.get () then "__fc_" ^ name else name in
+ let vi_o = Globals.Syntactic_search.find_in_scope name Global in
+ Option.iter (fun vi -> Varinfo.Hashtbl.add tbl vi spec) vi_o
+ in List.iter add_builtin specs
+
+ let clear () = Varinfo.Hashtbl.clear tbl
+
+ let mem = Varinfo.Hashtbl.mem tbl
+
+ let find_opt = Varinfo.Hashtbl.find_opt tbl
+
+ let pointer_of_term t =
+ let filter_opt f = function
+ | None -> None
+ | Some x -> if f x then Some x else None
+ in
+ match t.term_node with
+ | TLval (TVar {lv_origin = Some v}, TNoOffset) ->
+ filter_opt (fun spec -> spec.pointer) (find_opt v)
+ | TAddrOf (TVar {lv_origin = Some v}, TNoOffset) ->
+ filter_opt (fun spec -> not @@ spec.pointer) (find_opt v)
+ | _ -> None
+end
+
let must_never_monitor vi =
(* E-ACSL, please do not monitor yourself! *)
Rtl.Symbols.mem_vi vi.vname
@@ -42,6 +84,8 @@ let must_never_monitor vi =
||
(* function pointers are not yet supported. *)
Cil.isFunctionType vi.vtype
+ ||
+ SpecialPointers.mem vi
(* ********************************************************************** *)
(* Backward dataflow analysis to compute a sound over-approximation of what
@@ -163,6 +207,7 @@ end
let reset () =
Options.feedback ~dkey ~level:2 "clearing environment.";
+ SpecialPointers.clear ();
Env.clear ()
module rec Transfer
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.mli b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
index d66ae805534b9ba2d4cc9803273df12f9b31b239..b4bd046673882e068d8286104f3ebe49d0d7deb3 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.mli
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.mli
@@ -25,6 +25,14 @@ open Cil_types
(** Compute a sound over-approximation of what left-values must be tracked by
the memory model library *)
+module SpecialPointers : sig
+ type spec = {pointer : bool; freeable : bool; writeable : bool; initialized : bool}
+ val initialize : unit -> unit
+
+ (* is this one of stdin/stdout/stderr/&errno? If so, return spec *)
+ val pointer_of_term : term -> spec option
+end
+
val reset: unit -> unit
(** Must be called to redo the analysis *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index a1fe17a9c9f8d6ed658fcfb018a7419b815b4186..018742d7921846ce388ccbaf369140289f01fd5e 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -74,6 +74,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let loc = p.pred_loc in
let logic_env = Env.Logic_env.get env in
Current_loc.set loc;
+ let of_bool = function true -> Cil.one ~loc | false -> Cil.zero ~loc in
match p.pred_content with
| Pfalse -> Cil.zero ~loc, adata, env
| Ptrue -> Cil.one ~loc, adata, env
@@ -216,21 +217,29 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
Translate_ats.to_exp ~loc ~adata kf env (PoT_pred p) label
| Pvalid_read(BuiltinLabel Here, t) as pc
| (Pvalid(BuiltinLabel Here, t) as pc) ->
- let call_valid ~adata t p =
- let name = match pc with
- | Pvalid _ -> "valid"
- | Pvalid_read _ -> "valid_read"
- | _ -> assert false
- in
- let e, adata, env =
- Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
- in
- let adata = Assert.register_pred ~loc env p e adata in
- e, adata, env
- in
- (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
- now convert this right-most valid. *)
- call_valid ~adata t p
+ begin
+ match pc, Memory_tracking.SpecialPointers.pointer_of_term t with
+ (* static resolution: \valid(stdout) ≡ 1; \valid(stdin) ≡ 0; etc. *)
+ | Pvalid _, Some spec -> of_bool spec.writeable, adata, env
+ (* static resolution: \valid_read(stdin) ≡ 1; \valid_read(&errno) ≡ 1; etc. *)
+ | Pvalid_read _, Some _spec -> of_bool true, adata, env
+ | _ ->
+ let call_valid ~adata t p =
+ let name = match pc with
+ | Pvalid _ -> "valid"
+ | Pvalid_read _ -> "valid_read"
+ | _ -> assert false
+ in
+ let e, adata, env =
+ Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
+ in
+ let adata = Assert.register_pred ~loc env p e adata in
+ e, adata, env
+ in
+ (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
+ now convert this right-most valid. *)
+ call_valid ~adata t p
+ end
| Pvalid _ -> Env.not_yet env "labeled \\valid"
| Pvalid_read _ -> Env.not_yet env "labeled \\valid_read"
| Pseparated tlist ->
@@ -267,38 +276,46 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pinitialized(BuiltinLabel Here, t) ->
- let e, adata, env =
- (match t.term_node with
- (* optimisation when we know that the initialisation is ok *)
- | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, adata, env
- | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
- when
- vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
- Cil.one ~loc, adata, env
- | _ ->
- let e, adata, env =
- Memory_translate.call_with_size
- ~adata
- ~loc
- kf
- "initialized"
- Cil.intType
- env
- [ t ]
- p
- in
- let adata = Assert.register_pred ~loc env p e adata in
- e, adata, env)
- in
- e, adata, env
+ begin
+ match Memory_tracking.SpecialPointers.pointer_of_term t with
+ (* static resolutions: \initialized(stdout) ≡ 1; etc. *)
+ | Some spec -> of_bool spec.initialized, adata, env
+ | None ->
+ match t.term_node with
+ (* optimisation when we know that the initialisation is ok *)
+ | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, adata, env
+ | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
+ when
+ vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
+ Cil.one ~loc, adata, env
+ | _ ->
+ let e, adata, env =
+ Memory_translate.call_with_size
+ ~adata
+ ~loc
+ kf
+ "initialized"
+ Cil.intType
+ env
+ [ t ]
+ p
+ in
+ let adata = Assert.register_pred ~loc env p e adata in
+ e, adata, env
+ end
| Pinitialized _ -> Env.not_yet env "labeled \\initialized"
| Pallocable _ -> Env.not_yet env "\\allocate"
- | Pfreeable(BuiltinLabel Here, t) ->
- let e, adata, env =
- Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
- in
- let adata = Assert.register_pred ~loc env p e adata in
- e, adata, env
+ | Pfreeable(BuiltinLabel Here, t) -> begin
+ match Memory_tracking.SpecialPointers.pointer_of_term t with
+ (* static resolutions: \freeable(stdout) ≡ 0; etc. *)
+ | Some spec -> of_bool spec.freeable, adata, env
+ | None ->
+ let e, adata, env =
+ Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
+ in
+ let adata = Assert.register_pred ~loc env p e adata in
+ e, adata, env
+ end
| Pfreeable _ -> Env.not_yet env "labeled \\freeable"
| Pfresh _ -> Env.not_yet env "\\fresh"
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index a4e5e85d31f4fcf406c56278beb2757a7f0e9eb1..8cbd69646da818e9f9622157211b90e1b91c5167 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -49,6 +49,7 @@ let generate_code =
(* preparation of the AST does not concern the E-ACSL RTL:
do it first *)
Prepare_ast.prepare ();
+ Memory_tracking.SpecialPointers.initialize ();
Rtl.link rtl_prj;
(* the E-ACSL type system ensures the soundness of the generated
arithmetic operations. Therefore, deactivate the corresponding
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index 6726aca133c0489dd71bb29ae3d6510298ad409b..0b015a34965af1b60854b2680b95718c1bb533c1 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -1683,10 +1683,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_fopen));
__e_acsl_store_block((void *)(__fc_fopen),128UL);
__e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdout),8UL);
- __e_acsl_full_init((void *)(& stdout));
- __e_acsl_store_block((void *)(& stdin),8UL);
- __e_acsl_full_init((void *)(& stdin));
__e_acsl_store_block((void *)(& __fc_interrupted),4UL);
__e_acsl_full_init((void *)(& __fc_interrupted));
__e_acsl_store_block((void *)(& __fc_p_time_tm),8UL);
@@ -1703,8 +1699,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_sigaction));
__e_acsl_store_block((void *)(sigaction),2080UL);
__e_acsl_full_init((void *)(& sigaction));
- __e_acsl_store_block((void *)(& errno),4UL);
- __e_acsl_full_init((void *)(& errno));
}
return;
}
@@ -1729,8 +1723,6 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(__fc_tmpnam));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& stdin));
__e_acsl_delete_block((void *)(& __fc_interrupted));
__e_acsl_delete_block((void *)(& __fc_p_time_tm));
__e_acsl_delete_block((void *)(& __fc_time_tm));
@@ -1739,7 +1731,6 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& __fc_time));
__e_acsl_delete_block((void *)(& __fc_p_sigaction));
__e_acsl_delete_block((void *)(sigaction));
- __e_acsl_delete_block((void *)(& errno));
return;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 680fcfdaecb6ecc4c123bc0ae24a8f484bf77d7e..038e1ab49bf714a185ab8ca15229e8be3d610bd8 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -1365,10 +1365,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_fopen));
__e_acsl_store_block((void *)(__fc_fopen),128UL);
__e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdout),8UL);
- __e_acsl_full_init((void *)(& stdout));
- __e_acsl_store_block((void *)(& stdin),8UL);
- __e_acsl_full_init((void *)(& stdin));
__e_acsl_store_block((void *)(& __fc_interrupted),4UL);
__e_acsl_full_init((void *)(& __fc_interrupted));
__e_acsl_store_block((void *)(& __fc_p_time_tm),8UL);
@@ -1385,8 +1381,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_sigaction));
__e_acsl_store_block((void *)(sigaction),2080UL);
__e_acsl_full_init((void *)(& sigaction));
- __e_acsl_store_block((void *)(& errno),4UL);
- __e_acsl_full_init((void *)(& errno));
}
return;
}
@@ -1411,8 +1405,6 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(__fc_tmpnam));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& stdin));
__e_acsl_delete_block((void *)(& __fc_interrupted));
__e_acsl_delete_block((void *)(& __fc_p_time_tm));
__e_acsl_delete_block((void *)(& __fc_time_tm));
@@ -1421,7 +1413,6 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& __fc_time));
__e_acsl_delete_block((void *)(& __fc_p_sigaction));
__e_acsl_delete_block((void *)(sigaction));
- __e_acsl_delete_block((void *)(& errno));
return;
}
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
index e1865e3750f8492648ae105f11bf4ee9a467b7e3..6713347b1c7fa5b3986d3b51d485eb65c798ccd3 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
@@ -51,155 +51,77 @@ void *thread_start(void *arg)
void *__retres;
__e_acsl_store_block((void *)(& __retres),8UL);
{
- int __gen_e_acsl_valid;
- int __gen_e_acsl_and;
__e_acsl_store_block((void *)(& arg),8UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __gen_e_acsl_valid = __e_acsl_valid((void *)stdout,sizeof(FILE),
- (void *)stdout,(void *)(& stdout));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"__fc_stdout",
- (void *)stdout);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"sizeof(FILE)",
- 0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "\\valid(__fc_stdout)",0,__gen_e_acsl_valid);
- if (__gen_e_acsl_valid) {
- int __gen_e_acsl_initialized;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)stdout,
- sizeof(FILE));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"__fc_stdout",
- (void *)stdout);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "\\initialized(__fc_stdout)",0,
- __gen_e_acsl_initialized);
- __gen_e_acsl_and = __gen_e_acsl_initialized;
- }
- else __gen_e_acsl_and = 0;
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
__gen_e_acsl_assert_data.pred_txt = "\\valid(__fc_stdout) && \\initialized(__fc_stdout)";
__gen_e_acsl_assert_data.file = "threads_safe_locations.c";
__gen_e_acsl_assert_data.fct = "thread_start";
__gen_e_acsl_assert_data.line = 6;
- __e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_assert(1,& __gen_e_acsl_assert_data);
}
/*@ assert \valid(__fc_stdout) && \initialized(__fc_stdout); */ ;
{
- int __gen_e_acsl_valid_2;
- int __gen_e_acsl_and_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stderr,sizeof(FILE),
- (void *)stderr,(void *)(& stderr));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"__fc_stderr",
- (void *)stderr);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "\\valid(__fc_stderr)",0,
- __gen_e_acsl_valid_2);
- if (__gen_e_acsl_valid_2) {
- int __gen_e_acsl_initialized_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)stderr,
- sizeof(FILE));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
- "__fc_stderr",(void *)stderr);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "\\initialized(__fc_stderr)",0,
- __gen_e_acsl_initialized_2);
- __gen_e_acsl_and_2 = __gen_e_acsl_initialized_2;
- }
- else __gen_e_acsl_and_2 = 0;
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "\\valid(__fc_stderr) && \\initialized(__fc_stderr)";
__gen_e_acsl_assert_data_2.file = "threads_safe_locations.c";
__gen_e_acsl_assert_data_2.fct = "thread_start";
__gen_e_acsl_assert_data_2.line = 7;
- __e_acsl_assert(__gen_e_acsl_and_2,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(1,& __gen_e_acsl_assert_data_2);
}
/*@ assert \valid(__fc_stderr) && \initialized(__fc_stderr); */ ;
{
- int __gen_e_acsl_valid_read;
- int __gen_e_acsl_and_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)stdin,sizeof(FILE),
- (void *)stdin,
- (void *)(& stdin));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdin",
- (void *)stdin);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "\\valid_read(__fc_stdin)",0,
- __gen_e_acsl_valid_read);
- if (__gen_e_acsl_valid_read) {
- int __gen_e_acsl_initialized_3;
- __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)stdin,
- sizeof(FILE));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdin",
- (void *)stdin);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "\\initialized(__fc_stdin)",0,
- __gen_e_acsl_initialized_3);
- __gen_e_acsl_and_3 = __gen_e_acsl_initialized_3;
- }
- else __gen_e_acsl_and_3 = 0;
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
__gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(__fc_stdin) && \\initialized(__fc_stdin)";
__gen_e_acsl_assert_data_3.file = "threads_safe_locations.c";
__gen_e_acsl_assert_data_3.fct = "thread_start";
__gen_e_acsl_assert_data_3.line = 8;
- __e_acsl_assert(__gen_e_acsl_and_3,& __gen_e_acsl_assert_data_3);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert(1,& __gen_e_acsl_assert_data_3);
}
/*@ assert \valid_read(__fc_stdin) && \initialized(__fc_stdin); */ ;
int *addrof_errno = & errno;
__e_acsl_store_block((void *)(& addrof_errno),8UL);
__e_acsl_full_init((void *)(& addrof_errno));
{
- int __gen_e_acsl_initialized_4;
- int __gen_e_acsl_and_4;
- int __gen_e_acsl_and_5;
+ int __gen_e_acsl_initialized;
+ int __gen_e_acsl_and;
+ int __gen_e_acsl_and_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& addrof_errno),
- sizeof(int *));
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& addrof_errno),
+ sizeof(int *));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
"&addrof_errno",(void *)(& addrof_errno));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int *)",0,sizeof(int *));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
"\\initialized(&addrof_errno)",0,
- __gen_e_acsl_initialized_4);
- if (__gen_e_acsl_initialized_4) {
- int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)addrof_errno,sizeof(int),
- (void *)addrof_errno,
- (void *)(& addrof_errno));
+ __gen_e_acsl_initialized);
+ if (__gen_e_acsl_initialized) {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)addrof_errno,sizeof(int),
+ (void *)addrof_errno,
+ (void *)(& addrof_errno));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
"addrof_errno",(void *)addrof_errno);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
"sizeof(int)",0,sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
"\\valid(addrof_errno)",0,
- __gen_e_acsl_valid_3);
- __gen_e_acsl_and_4 = __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid);
+ __gen_e_acsl_and = __gen_e_acsl_valid;
}
- else __gen_e_acsl_and_4 = 0;
- if (__gen_e_acsl_and_4) {
- int __gen_e_acsl_initialized_5;
- __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)addrof_errno,
+ else __gen_e_acsl_and = 0;
+ if (__gen_e_acsl_and) {
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)addrof_errno,
sizeof(int));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
"addrof_errno",(void *)addrof_errno);
@@ -207,17 +129,17 @@ void *thread_start(void *arg)
"sizeof(int)",0,sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
"\\initialized(addrof_errno)",0,
- __gen_e_acsl_initialized_5);
- __gen_e_acsl_and_5 = __gen_e_acsl_initialized_5;
+ __gen_e_acsl_initialized_2);
+ __gen_e_acsl_and_2 = __gen_e_acsl_initialized_2;
}
- else __gen_e_acsl_and_5 = 0;
+ else __gen_e_acsl_and_2 = 0;
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Assertion";
__gen_e_acsl_assert_data_4.pred_txt = "\\valid(addrof_errno) && \\initialized(addrof_errno)";
__gen_e_acsl_assert_data_4.file = "threads_safe_locations.c";
__gen_e_acsl_assert_data_4.fct = "thread_start";
__gen_e_acsl_assert_data_4.line = 10;
- __e_acsl_assert(__gen_e_acsl_and_5,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_and_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
/*@ assert \valid(addrof_errno) && \initialized(addrof_errno); */ ;
@@ -493,12 +415,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_fopen));
__e_acsl_store_block((void *)(__fc_fopen),128UL);
__e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stdout),8UL);
- __e_acsl_full_init((void *)(& stdout));
- __e_acsl_store_block((void *)(& stdin),8UL);
- __e_acsl_full_init((void *)(& stdin));
- __e_acsl_store_block((void *)(& stderr),8UL);
- __e_acsl_full_init((void *)(& stderr));
__e_acsl_store_block((void *)(& __fc_interrupted),4UL);
__e_acsl_full_init((void *)(& __fc_interrupted));
__e_acsl_store_block((void *)(& __fc_p_time_tm),8UL);
@@ -515,8 +431,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_sigaction));
__e_acsl_store_block((void *)(sigaction),2080UL);
__e_acsl_full_init((void *)(& sigaction));
- __e_acsl_store_block((void *)(& errno),4UL);
- __e_acsl_full_init((void *)(& errno));
}
return;
}
@@ -527,9 +441,6 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(__fc_tmpnam));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& stderr));
__e_acsl_delete_block((void *)(& __fc_interrupted));
__e_acsl_delete_block((void *)(& __fc_p_time_tm));
__e_acsl_delete_block((void *)(& __fc_time_tm));
@@ -538,7 +449,6 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& __fc_time));
__e_acsl_delete_block((void *)(& __fc_p_sigaction));
__e_acsl_delete_block((void *)(sigaction));
- __e_acsl_delete_block((void *)(& errno));
return;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
index 7541386aef45bf1ad4008d0a5323371adb062bba..81dd33d16813be56c8e3b47f9c2e9a8209f2522c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
@@ -10,28 +10,10 @@
#include "time.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __e_acsl_store_block((void *)(& errno),4UL);
- __e_acsl_full_init((void *)(& errno));
- }
- return;
-}
-
-void __e_acsl_globals_clean(void)
-{
- __e_acsl_delete_block((void *)(& errno));
- return;
-}
-
int main(int argc, char const **argv)
{
int __retres;
__e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
- __e_acsl_globals_init();
int *p = & errno;
__e_acsl_store_block((void *)(& p),8UL);
__e_acsl_full_init((void *)(& p));
@@ -72,7 +54,6 @@ int main(int argc, char const **argv)
/*@ assert \valid(p); */ ;
__retres = 0;
__e_acsl_delete_block((void *)(& p));
- __e_acsl_globals_clean();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
index 07f3bc147ab6946873b871aee042604f92bf743e..e5024cc5bf4e059efe502608899188d5aebc3b28 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
@@ -8,104 +8,46 @@
#include "time.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __e_acsl_store_block((void *)(& stdout),8UL);
- __e_acsl_full_init((void *)(& stdout));
- __e_acsl_store_block((void *)(& stdin),8UL);
- __e_acsl_full_init((void *)(& stdin));
- __e_acsl_store_block((void *)(& stderr),8UL);
- __e_acsl_full_init((void *)(& stderr));
- }
- return;
-}
-
-void __e_acsl_globals_clean(void)
-{
- __e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& stderr));
- return;
-}
-
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_globals_init();
{
- int __gen_e_acsl_valid;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __gen_e_acsl_valid = __e_acsl_valid((void *)stderr,sizeof(FILE),
- (void *)stderr,(void *)(& stderr));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"__fc_stderr",
- (void *)stderr);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"sizeof(FILE)",
- 0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "\\valid(__fc_stderr)",0,__gen_e_acsl_valid);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
__gen_e_acsl_assert_data.pred_txt = "\\valid(__fc_stderr)";
__gen_e_acsl_assert_data.file = "stdout.c";
__gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 8;
- __e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_assert(1,& __gen_e_acsl_assert_data);
}
/*@ assert \valid(__fc_stderr); */ ;
{
- int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)stdin,sizeof(FILE),
- (void *)stdin,
- (void *)(& stdin));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"__fc_stdin",
- (void *)stdin);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "\\valid_read(__fc_stdin)",0,
- __gen_e_acsl_valid_read);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__fc_stdin)";
__gen_e_acsl_assert_data_2.file = "stdout.c";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 9;
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(1,& __gen_e_acsl_assert_data_2);
}
/*@ assert \valid_read(__fc_stdin); */ ;
{
- int __gen_e_acsl_valid_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdout,sizeof(FILE),
- (void *)stdout,(void *)(& stdout));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdout",
- (void *)stdout);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
- "sizeof(FILE)",0,sizeof(FILE));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "\\valid(__fc_stdout)",0,
- __gen_e_acsl_valid_2);
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
__gen_e_acsl_assert_data_3.pred_txt = "\\valid(__fc_stdout)";
__gen_e_acsl_assert_data_3.file = "stdout.c";
__gen_e_acsl_assert_data_3.fct = "main";
__gen_e_acsl_assert_data_3.line = 10;
- __e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert(1,& __gen_e_acsl_assert_data_3);
}
/*@ assert \valid(__fc_stdout); */ ;
__retres = 0;
- __e_acsl_globals_clean();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
index dc148d6a1b66770b41ccef0bdb51409a401a3914..db5643b8380fabd98a67a8220d18ef355e345d85 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
@@ -1,29 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] stdout.c:8: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] stdout.c:8: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] stdout.c:8: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] stdout.c:8: Warning: assertion got status unknown.
-[eva:alarm] stdout.c:9: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] stdout.c:9: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] stdout.c:9: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] stdout.c:9: Warning: assertion got status unknown.
-[eva:alarm] stdout.c:10: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] stdout.c:10: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] stdout.c:10: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] stdout.c:10: Warning: assertion got status unknown.