From 456d98a810d67f73c5626a9eb6e4f26d2ee507c4 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 2 Apr 2024 22:28:27 +0200
Subject: [PATCH] [e-acsl] statically determine some predicates for special
pointers
For the special pointers stdin, stdout, stderr, and &errno the results
of \pvalid, \pinitialized, \freeable are statically known, so we return
the result directly instead of generating calls to the runtime functions.
This complements the implementation of the same semantics in the runtime
libraries in the previous commit. As the runtime implementation is
sufficient, this commit is an optimisation.
We currently do not optimise logic functions such as \block_length,
\offset, \base_addr, but we do not expect too many occurrences of terms
such as \base_addr(*(&stdin + 9)).
---
.../e-acsl/src/analyses/memory_tracking.ml | 45 ++++++
.../e-acsl/src/analyses/memory_tracking.mli | 8 +
.../code_generator/translate_predicates.ml | 107 ++++++++------
src/plugins/e-acsl/src/main.ml | 1 +
.../concurrency/oracle/gen_parallel_threads.c | 9 --
.../concurrency/oracle/gen_threads_debug.c | 9 --
.../oracle/gen_threads_safe_locations.c | 138 +++---------------
.../e-acsl/tests/memory/oracle/gen_errno.c | 19 ---
.../e-acsl/tests/memory/oracle/gen_stdout.c | 64 +-------
.../tests/memory/oracle/stdout.res.oracle | 24 ---
10 files changed, 143 insertions(+), 281 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index f4c318a3f63..34c3eedf281 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 d66ae805534..b4bd0466738 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 a1fe17a9c9f..018742d7921 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 a4e5e85d31f..8cbd69646da 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 6726aca133c..0b015a34965 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 680fcfdaecb..038e1ab49bf 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 e1865e3750f..6713347b1c7 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 7541386aef4..81dd33d1681 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 07f3bc147ab..e5024cc5bf4 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 dc148d6a1b6..db5643b8380 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.
--
GitLab