--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on August 2011 ---
Hello, Le 17/08/2011 16:29, Daniel Sheridan a ?crit : > I am working on a plugin which eliminates branches of code under certain > circumstances. Using a combination of constant propagation and spare > code analysis, I end up with code of the form > > if (1) { > ... > } > > which is technically correct, but would be more useful if it were > simplified. I notice that saving the code to disk and loading it in to > Frama-C is enough to eliminate the unnecessary "if". If I well understand what you are saying, you pretty print the generated code into a C file by using options "-print" and "-ocode", then you re-execute Frama-c on this file. Is it correct? > Is it possible to access this simplification step from a plugin, or do I > need to write my own visitor-based implementation of it? In the next Frama-C version, there will be a function File.create_rebuilt_project_from_visitor which will do the job [*]. Thus you can write for instance the following script: === a.ml === let main () = (* propagates constants and put the resulting AST into project [p] *) let p = !Db.Constant_Propagation.get Datatype.String.Set.empty ~cast_intro:false in Project.on p (fun () -> (* print on stdout the unsimplified AST of constant propagation *) File.pretty_ast (); (* simplify the AST of project [p] and put the resulting AST in project [prj] *) let prj = File.create_rebuilt_project_from_visitor "p" (new Visitor.frama_c_copy) in (* print on stdout the simplified AST *) File.pretty_ast ~prj ()) () let () = Db.Main.extend main ============ and run it in the following file: === a.c === int main(void) { int x = 0; if (x == 0) x = 1; else x = 2; return 0; } ============ $ frama-c -load-script a.ml a.c <snip information lines> /* Generated by Frama-C */ // that is the unsimplified AST int main(void) { int __retres; int x; x = 0; if (1) { x = 1; } else { x = 2; } __retres = 0; return (__retres); } /* Generated by Frama-C */ // that is the simplified AST int main(void) { int __retres; int x; x = 0; x = 1; __retres = 0; return (__retres); } Hope this helps, Julien -------------------------------------------------------------------- [*] If you want to use this solution with the current Frama-C Carbon, below is an "almost correct" version of File.create_rebuilt_project_from_visitor. "Almost correct" means that you use neither plug-in which analyses non-C files, nor any module Cabs*, nor module Ast.UntypedFiles. The fully correct solution uses internal kernel values and the workaround is quite ugly. let get_preprocessor_command () = let cmdline = Kernel.CppCommand.get() in if cmdline <> "" then cmdline else try Sys.getenv "CPP" with Not_found -> "gcc -C -E -I." let from_filename ?(cpp=get_preprocessor_command ()) f = if Filename.check_suffix f ".i" then File.NoCPP f else let suf = try let suf_idx = String.rindex f '.' in String.sub f suf_idx (String.length f - suf_idx) with Not_found -> (* raised by String.rindex if '.' \notin f *) "" in File.External (f, suf) let create_rebuilt_project_from_visitor ?(preprocess=false) prj_name visitor = let prj = File.create_project_from_visitor prj_name visitor in try let f = let name = "frama_c_project_" ^ prj_name ^ "_" in let ext = if preprocess then ".c" else ".i" in if Kernel.Debug.get () > 0 then Filename.temp_file name ext else Extlib.temp_file_cleanup_at_exit name ext in let cout = open_out f in let fmt = Format.formatter_of_out_channel cout in (*unjournalized_pretty prj (Some fmt) ();*) File.pretty_ast ~prj ~fmt (); let redo () = Project.clear ~selection:(State_selection.Dynamic.with_dependencies Ast.self) (); File.init_from_c_files [ if preprocess then from_filename f else File.NoCPP f ] in Project.on prj redo (); prj with Extlib.Temp_file_error s | Sys_error s -> Kernel.abort "cannot create temporary file: %s" s