Commit a26e5ceb authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] add missing valid_sid:true

parent e847477b
...@@ -168,7 +168,7 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf = ...@@ -168,7 +168,7 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
in in
let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
if not (may_safely_ignore lv) && must_model then 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 = let new_stmt =
(* bitfields are not yet supported ==> no initializer. (* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *) a [not_yet] will be raised in [Translate]. *)
......
...@@ -677,7 +677,7 @@ and env_of_li li kf env loc = ...@@ -677,7 +677,7 @@ and env_of_li li kf env loc =
let e, env = term_to_exp kf env t in let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with let stmt = match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) -> | 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 -> | Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e Gmp.init_set ~loc (Cil.var vi) vi_e e
| Typing.Rational -> | Typing.Rational ->
...@@ -1138,6 +1138,6 @@ let translate_post_code_annotation kf env annot = ...@@ -1138,6 +1138,6 @@ let translate_post_code_annotation kf env annot =
(* (*
Local Variables: Local Variables:
compile-command: "make -C ../.." compile-command: "make -C ../../../../.."
End: End:
*) *)
...@@ -183,7 +183,7 @@ class prepare_visitor prj = object (self) ...@@ -183,7 +183,7 @@ class prepare_visitor prj = object (self)
match stmt.skind with match stmt.skind with
| Switch(_,sw_blk,_,_) -> | Switch(_,sw_blk,_,_) ->
let new_blk = Cil.mkBlock [ stmt ] in 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; new_blk.blocals <- sw_blk.blocals;
sw_blk.blocals <- []; sw_blk.blocals <- [];
new_stmt new_stmt
...@@ -222,6 +222,6 @@ let prepare () = ...@@ -222,6 +222,6 @@ let prepare () =
(* (*
Local Variables: Local Variables:
compile-command: "make -C ../.." compile-command: "make -C ../../../../.."
End: End:
*) *)
...@@ -70,4 +70,4 @@ int main(void) { ...@@ -70,4 +70,4 @@ int main(void) {
char c = 'w'; char c = 'w';
f(&c, 5); f(&c, 5);
} }
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment