--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2014 ---
just update the question! I have been solved this problem by changing this piece of code On 16 May 2014 03:29, David Yang <abiao.yang at gmail.com> wrote: > match lval with > | Some(Var vi, _) -> > begin > let instr = Cil_types.Set(Cil.var vi, Cil.integer ~loc 1, loc) in > let insert_stmt = Cil.mkStmt (Cil_types.Instr instr) in > insert_stmt.labels <- stmt.labels; > stmt.labels <- []; > let bloc_kind = Cil_types.Block(Cil.mkBlock [insert_stmt; stmt]) in > let new_stmt = Cil.mkStmt bloc_kind in > Cil.ChangeTo new_stmt > end > | _ -> Cil.DoChildren into: (* ===============update code ================= *) match lval with | Some(Var vi, _) -> begin let instr = Cil_types.Set(Cil.var vi, Cil.integer ~loc 1, loc) in let insert_stmt = Cil.mkStmt (Cil_types.Instr instr) in let dstmt = Cil.dummyStmt in dstmt.skind <- stmt.skind; let bloc_kind = Cil_types.Block(Cil.mkBlock [insert_stmt; dstmt]) in stmt.skind <- bloc_kind; Cil.ChangeTo stmt end | _ -> Cil.DoChildren