Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] How to transform a statement with case label by using the visitor?
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Fri, 16 May 2014 03:29:12 +0800
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>