diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index 2884e402669088fbbd2694381b83baf8c5c2d5d4..8f220ac92b3275c3f07dcad56ef5160c289a86ab 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 021c5b0acb09dbd822d9cc93242bcfaa3bd62189..92f3d335f21ae0ddd5a26e469b19ea5efafee7e6 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 21b22d17866c3083cd21bc17521f049ce95f0ebe..035f8c083dd6ca7277305c4df8200447e7b937de 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 7c94e87d3ceb3f39f32c651abca2c300842dd83a..208afd355b95ebac47ccc3979e1238c582be9682 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 +}