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 (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);
  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:
frama-c -load-script case_func.c

Attached please find the file "" 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 --------------------- *)
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)) ->
        match lval with
        | Some(Var vi, _) ->
          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
        | _ -> Cil.DoChildren
      | _ -> Cil.DoChildren
    end else Cil.DoChildren


module Computed =
    let name = "transform"
    let dependencies = []
    let kind = `Internal

let main () =
  if not (Computed.get()) then
    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 ();

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: <>
-------------- next part --------------
A non-text attachment was scrubbed...
Type: application/octet-stream
Size: 1554 bytes
Desc: not available
URL: <>