From a26e5ceb93d9fc99fcbb887bed1d8b59c0129cda Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 2 Dec 2019 17:49:53 +0100
Subject: [PATCH] [e-acsl:archi] add missing valid_sid:true
---
src/plugins/e-acsl/src/code_generator/injector.ml | 2 +-
src/plugins/e-acsl/src/code_generator/translate.ml | 4 ++--
src/plugins/e-acsl/src/project_initializer/prepare_ast.ml | 4 ++--
src/plugins/e-acsl/tests/memory/ranges_in_builtins.c | 2 +-
4 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 2884e402669..8f220ac92b3 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -168,7 +168,7 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
in
let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
if not (may_safely_ignore lv) && must_model then
- let before = Cil.mkStmt stmt.skind in
+ let before = Cil.mkStmt ~valid_sid:true stmt.skind in
let new_stmt =
(* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 021c5b0acb0..92f3d335f21 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -677,7 +677,7 @@ and env_of_li li kf env loc =
let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
- Cil.mkStmtOneInstr (Set (Cil.var vi, e, loc))
+ Cil.mkStmtOneInstr ~valid_sid:true (Set (Cil.var vi, e, loc))
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
| Typing.Rational ->
@@ -1138,6 +1138,6 @@ let translate_post_code_annotation kf env annot =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 21b22d17866..035f8c083dd 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -183,7 +183,7 @@ class prepare_visitor prj = object (self)
match stmt.skind with
| Switch(_,sw_blk,_,_) ->
let new_blk = Cil.mkBlock [ stmt ] in
- let new_stmt = Cil.mkStmt (Block new_blk) in
+ let new_stmt = Cil.mkStmt ~valid_sid:true (Block new_blk) in
new_blk.blocals <- sw_blk.blocals;
sw_blk.blocals <- [];
new_stmt
@@ -222,6 +222,6 @@ let prepare () =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
index 7c94e87d3ce..208afd355b9 100644
--- a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
@@ -70,4 +70,4 @@ int main(void) {
char c = 'w';
f(&c, 5);
-}
\ No newline at end of file
+}
--
GitLab