--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on May 2014 ---
Dear all, I am writing a script to insert a statement into the case statement. But I failed to correctly transform the code for value anaysis. i want to transform a case statement from : case 0: result = f1(a); to: case 0: result = 1; result = f1(a); I know this code transform has no semantic meanings to this piece of code. What I am focus on is how to transform the statement with case labels. the command line I used for loading the script is: --------------------command------------------------ frama-c -load-script transform_case.ml case_func.c Attached please find the file "transform_case.ml" and the file "case_func.c" /* ------------------------ content of case_func.c -------------- */ int main (int arg) { int result; char* a; int b; switch(argz) { case 0: result = f1(a); default: result = -1; } return result; } (* ---------------- content of transform_case.ml --------------------- *) open Cil open Cil_types class transform_case_call_stmt prj = object (self) inherit Visitor.frama_c_copy prj method vstmt_aux stmt = if (List.exists Cil.is_case_label stmt.labels) then begin match stmt.skind with | Instr (Call(lval, _, _, loc)) -> begin 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 end | _ -> Cil.DoChildren end else Cil.DoChildren end;; module Computed = State_builder.False_ref( struct let name = "transform" let dependencies = [] let kind = `Internal end ) let main () = if not (Computed.get()) then begin Computed.set true; Ast.compute (); Format.printf "Before transfering:\n%a" Printer.pp_file (Ast.get ()); let vis = new transform_case_call_stmt in let prj = File.create_project_from_visitor "transfer" vis in Project.set_current prj; Format.printf "\n\nAfter transfering:\n%a" Printer.pp_file (Ast.get ()); Globals.set_entry_point "main" true; !Db.Value.compute (); end; ;; let () = Db.Main.extend main -------------- next part -------------- A non-text attachment was scrubbed... Name: case_func.c Type: text/x-csrc Size: 230 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140516/98861f81/attachment.c> -------------- next part -------------- A non-text attachment was scrubbed... Name: transform_case.ml Type: application/octet-stream Size: 1554 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140516/98861f81/attachment.obj>