--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to transform a statement with case label by using the visitor?



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>