error3.JPG (139,548 bytes) 2010-06-14 15:57

frama_c_journal.ml (2,543 bytes) 2010-06-14 15:57

(* Frama-C journal generated at 16:49 the 14/06/2010 *)

exception Unreachable
exception Exception of string

(* Run the user commands *)
let run () =
  File.init_from_cmdline ();
  let p_interactive = Project.create "interactive" in
  Project.set_current ~on:true p_interactive;
  Parameters.Files.set [ "D:\\main.c" ];
  File.init_from_cmdline ();
  Project.set_current ~on:true (Project.from_unique_name "default");
  Project.set_current p_interactive;
  !Db.Slicing.Project.set_project None;
  !Db.Metrics.compute ();
  Parameters.Dynamic.Bool.set "-jessie" true;
  Parameters.Dynamic.Bool.set "-jessie-adhoc-normalization" false;
  Parameters.Dynamic.Bool.set "-val" true;
  !Db.Value.compute ();
  begin try
    (* exception Log.AbortFatal("jessie") raised on:Applying dynamic
                                                      functions
                                                      "run_analysis" of type
                                                      unit -> unit *)
    Dynamic.get ~plugin:"Jessie" "run_analysis" (Type.func Type.unit Type.unit)
      ();
    raise Unreachable
  with
  | Unreachable as exn -> raise exn
  | exn (* Log.AbortFatal("jessie") *) ->
    (* continuing: *)
    !Db.Slicing.Project.set_project None;
    !Db.Value.compute ();
    begin try
      (* exception Log.AbortFatal("jessie") raised on:Applying dynamic
                                                        functions
                                                        "run_analysis" of
                                                        type unit -> unit *)
      Dynamic.get ~plugin:"Jessie" "run_analysis" (Type.func Type.unit Type.unit)
        ();
      raise Unreachable
    with
    | Unreachable as exn -> raise exn
    | exn (* Log.AbortFatal("jessie") *) ->
      (* continuing: *) !Db.Slicing.Project.set_project None; ()
    end
  end

(* Main *)
let main () =
  Journal.keep_file "frama_c_journal.ml";
  try run ()
  with
  | Unreachable -> Kernel.fatal "Journal reachs an assumed dead code" 
  | Exception s -> Kernel.log "Journal re-raised the exception %S" s
  | exn ->
    Kernel.fatal
      "Journal raised an unexpected exception: %s"
      (Printexc.to_string exn)

(* Registering *)
let main : unit -> unit =
  Dynamic.register
    ~plugin:"Frama_c_journal"
    "main"
    (Type.func Type.unit Type.unit)
    ~journalize:false
    main

(* Hooking *)
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()

main.c (239 bytes) 2010-06-14 15:58

int i, t[10];

int main(void)
{
	unsigned int j;
	j=suma(1,2);
	for(i=0;i<20;i++)
		t[i]=i+1;
	return 0;
}

int suma(int i, int j)
{
	if(i==0 && j==0)
		return 0;
	else
		return i+j;
}

void f(void)
{
	return 1;
}