From ef99c7f4d46130d96d1e2b9386d9ebfe98714ef6 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 10 Feb 2021 11:39:50 +0100
Subject: [PATCH] [eacsl] Fix generated `__e_acsl_globals_clean()`
The `__eacsl_globals_clean()` global function is only created if there
are globals variables. A `return;` statement is added at the end of the
function to satisfy Frama-C invariants.
---
.../src/code_generator/global_observer.ml | 32 +++++++-------
.../src/code_generator/global_observer.mli | 4 +-
.../e-acsl/src/code_generator/injector.ml | 32 ++++++++------
.../e-acsl/tests/bts/issue-eacsl-145.c | 12 ++++++
.../tests/bts/oracle_ci/gen_issue-eacsl-145.c | 42 +++++++++++++++++++
.../bts/oracle_ci/issue-eacsl-145.res.oracle | 39 +++++++++++++++++
.../oracle_dev/issue-eacsl-145.e-acsl.err.log | 0
7 files changed, 132 insertions(+), 29 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-145.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-145.e-acsl.err.log
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 352152f2c2a..6ee21213ec0 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -187,20 +187,24 @@ let mk_init_function () =
vi, fundec
let mk_clean_function () =
- (* Create and register [__e_acsl_globals_clean] function with definition
- for de-allocation of global variables *)
- let vi, fundec, _kf = mk_function function_clean_name in
- (* Generate delete statements and add them to the function body *)
- let stmts =
- Varinfo.Hashtbl.fold_sorted
- (fun vi _l acc ->
- if Misc.is_fc_or_compiler_builtin vi then acc
- else Smart_stmt.delete_stmt vi :: acc)
- tbl
- []
- in
- fundec.sbody.bstmts <- stmts;
- vi, fundec
+ if Varinfo.Hashtbl.length tbl = 0 then
+ None
+ else
+ (* Create and register [__e_acsl_globals_clean] function with definition
+ for de-allocation of global variables *)
+ let vi, fundec, _kf = mk_function function_clean_name in
+ (* Generate delete statements and add them to the function body *)
+ let return = Cil.mkStmt ~valid_sid:true (Return (None, Location.unknown)) in
+ let stmts =
+ Varinfo.Hashtbl.fold_sorted
+ (fun vi _l acc ->
+ if Misc.is_fc_or_compiler_builtin vi then acc
+ else Smart_stmt.delete_stmt vi :: acc)
+ tbl
+ [return]
+ in
+ fundec.sbody.bstmts <- stmts;
+ Some (vi, fundec)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.mli b/src/plugins/e-acsl/src/code_generator/global_observer.mli
index e37f39301d3..de355a0efc9 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.mli
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.mli
@@ -44,9 +44,9 @@ val mk_init_function: unit -> varinfo * fundec
(** Generate a new C function containing the observers for global variable
declarations and initializations. *)
-val mk_clean_function: unit -> varinfo * fundec
+val mk_clean_function: unit -> (varinfo * fundec) option
(** Generate a new C function containing the observers for global variable
- de-allocations. *)
+ de-allocations if there are global variables. *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index acae30bc013..f095fa81d2c 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -710,8 +710,12 @@ let inject_global_handler file main =
let vi_init, fundec_init = Global_observer.mk_init_function () in
let cil_fct_init = GFun(fundec_init, Location.unknown) in
(* Create [__e_acsl_globals_delete] function *)
- let vi_clean, fundec_clean = Global_observer.mk_clean_function () in
- let cil_fct_clean = GFun(fundec_clean, Location.unknown) in
+ let vi_and_fundec_clean_opt = Global_observer.mk_clean_function () in
+ let cil_fct_clean_opt =
+ Option.map
+ (fun (_, fundec_clean) -> GFun(fundec_clean, Location.unknown))
+ vi_and_fundec_clean_opt
+ in
match main with
| Some main ->
let mk_fct_call vi =
@@ -730,14 +734,14 @@ let inject_global_handler file main =
(* Create [__e_acsl_globals_init();] call *)
let stmt_init = mk_fct_call vi_init in
(* Create [__e_acsl_globals_delete();] call *)
- let stmt_clean =
- match fundec_clean.sbody.bstmts with
- | [] -> None
- | _ -> Some (mk_fct_call vi_clean)
+ let stmt_clean_opt =
+ Option.map
+ (fun (vi_clean, _) -> mk_fct_call vi_clean)
+ vi_and_fundec_clean_opt
in
(* Surround the content of main with the calls to
[__e_acsl_globals_init();] and [__e_acsl_globals_delete();] *)
- surround_function_with main main_fundec stmt_init stmt_clean;
+ surround_function_with main main_fundec stmt_init stmt_clean_opt;
(* Retrieve all globals except main *)
let main_vi = Globals.Functions.get_vi main in
let new_globals =
@@ -758,9 +762,10 @@ let inject_global_handler file main =
let globals_to_add = [ GFun(main_fundec, Location.unknown) ] in
(* Prepend [__e_acsl_globals_clean] if not empty *)
let globals_to_add =
- match fundec_clean.sbody.bstmts with
- | [] -> globals_to_add
- | _ -> cil_fct_clean :: globals_to_add
+ Option.fold
+ ~none:globals_to_add
+ ~some:(fun cil_fct_clean -> cil_fct_clean :: globals_to_add)
+ cil_fct_clean_opt
in
(* Prepend [__e_acsl_globals_init] *)
let globals_to_add = cil_fct_init :: globals_to_add in
@@ -782,9 +787,10 @@ let inject_global_handler file main =
Global_observer.function_init_name
Global_observer.function_clean_name;
let globals_func =
- match fundec_clean.sbody.bstmts with
- | [] -> [ cil_fct_init ]
- | _ -> [ cil_fct_init; cil_fct_clean ]
+ Option.fold
+ ~none:[ cil_fct_init ]
+ ~some:(fun cil_fct_clean -> [ cil_fct_init; cil_fct_clean ])
+ cil_fct_clean_opt
in
file.globals <- file.globals @ globals_func
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c
new file mode 100644
index 00000000000..dde2d2aed6d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c
@@ -0,0 +1,12 @@
+/* run.config_ci
+ COMMENT: frama-c/e-acsl#145, test for validity of globals_init and
+ globals_clean.
+ STDOPT: +"-verbose 1 -eva-print"
+*/
+int G = 0;
+
+int main(void) {
+ /*@ assert \valid(&G); */
+ int a = G;
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c
new file mode 100644
index 00000000000..7382aae8323
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c
@@ -0,0 +1,42 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int G = 0;
+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 *)(& G),(size_t)4);
+ __e_acsl_full_init((void *)(& G));
+ }
+ return;
+}
+
+void __e_acsl_globals_clean(void)
+{
+ __e_acsl_delete_block((void *)(& G));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& G),sizeof(int),
+ (void *)(& G),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid,"Assertion","main","\\valid(&G)",
+ "tests/bts/issue-eacsl-145.c",9);
+ }
+ /*@ assert \valid(&G); */ ;
+ int a = G;
+ __retres = 0;
+ __e_acsl_globals_clean();
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle
new file mode 100644
index 00000000000..73cc9ba6ba1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle
@@ -0,0 +1,39 @@
+[kernel] Parsing tests/bts/issue-eacsl-145.c (with preprocessing)
+[e-acsl] beginning translation.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ G ∈ {0}
+ __e_acsl_heap_allocation_size ∈ [--..--]
+ __e_acsl_heap_allocated_blocks ∈ [--..--]
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ __e_acsl_init ∈ [--..--]
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_full_init
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function __e_acsl_delete_block
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 5 functions analyzed (out of 5): 100% coverage.
+ In these functions, 27 statements reached (out of 27): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 0 invalid 1 total
+ Preconditions 1 valid 0 unknown 0 invalid 1 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-145.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-145.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab