|
(* Frama-C journal generated at 17:22 the 18/07/2018 *)
|
|
|
|
exception Unreachable
|
|
exception Exception of string
|
|
|
|
(* Run the user commands *)
|
|
let run () =
|
|
Dynamic.Parameter.Bool.set "-findlib" false;
|
|
Dynamic.Parameter.Bool.set "-autoload-plugins" false;
|
|
Dynamic.Parameter.String.set "-load-module" "@default,Crude_slicer.cmxs";
|
|
Dynamic.Parameter.Bool.set "-crude_slicer" true;
|
|
Dynamic.Parameter.Bool.set "-recognize_wrecked_container_of" false;
|
|
Dynamic.Parameter.Bool.set "-summaries" false;
|
|
Dynamic.Parameter.Bool.set "-assert_stratification" false;
|
|
Dynamic.Parameter.Bool.set "-print" true;
|
|
Dynamic.Parameter.String.set "-ocode" "/home/u1364447/Desktop/slice_gcc.c";
|
|
Dynamic.Parameter.Bool.set "-collapse-call-cast" false;
|
|
Dynamic.Parameter.String.set ""
|
|
"/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c";
|
|
File.init_from_cmdline ();
|
|
File.pretty_ast ();
|
|
Project.set_keep_current false;
|
|
()
|
|
|
|
(* Main *)
|
|
let main () =
|
|
Journal.keep_file "./.frama-c/frama_c_journal.ml";
|
|
try run ()
|
|
with
|
|
| Unreachable -> Kernel.fatal "Journal reaches 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.ml"
|
|
"main"
|
|
(Datatype.func Datatype.unit Datatype.unit)
|
|
~journalize:false
|
|
main
|
|
|
|
(* Hooking *)
|
|
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
|