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] slicing inquiry

On 02/10/2019 18:26, Ivan Postolski wrote:
> Hello Virgile
>
> Thank you very much. This is super useful!! I do not know Ocaml, so I 
> would be stuck for a long time if you didn't took the trouble to make 
> this script.
>
> There's a couple of corner cases that I will try to solve (i.e 
> conditional statements only show the line where they begin, and 
> function's declaring lines aren't shown as well).
>
> I have an spin-off question, how is the recommended way to execute 
> frama-c over a project? (e.g. gzip) that have multiple headers and .c 
> files, and have a makefile for compiling.

I did some blog posts on the subject, for instance: 
http://blog.frama-c.com/index.php?post/2018/01/25/Analysis-scripts%3A-helping-automate-case-studies

There are some newer features in the latest Frama-C releases that could 
help. Namely, frama-c-script. But the overall process is not perfectly 
robust: we rely on the JSON Compilation Database 
<https://clang.llvm.org/docs/JSONCompilationDatabase.html> format used 
by LLVM, which is not ideal, so a few caveats apply.

Overall, the process is:

- Install Build EAR <https://github.com/rizsotto/Bear> to generate a 
compile_commands.json file from running gzip's makefile (e.g. `bear make`);

- Run `frama-c-script list-files` to list the available source files 
(including the ones containing a main function);

- Run `frama-c-script make-template` to create a GNUmakefile template 
for running Frama-C;

- If everything works as expected, running `make parse` should parse the 
files with Frama-C, then `make eva` should run the Eva plug-in. If you 
want to use other plug-ins, you can load the parsing result and apply 
other command-line options, e.g.:

frama-c -load gzip.parse/framac.sav <other options>

(if you want to reuse the results /after/ running Eva, just load 
gzip.*eva*/framac.sav instead)


By the way, there is a Github repository with open source case studies 
for Eva <https://github.com/Frama-C/open-source-case-studies> which 
includes an old version of gzip. The case study is not finalized, but it 
could serve as example on how to configure things. You can take a look 
at `gzip124/GNUmakefile`.


Best regards,

André


> Cheers
>
> Ivan.-
>
>
> On Wed, Oct 2, 2019 at 5:45 AM Virgile Prevosto 
> <virgile.prevosto at m4x.org <mailto:virgile.prevosto at m4x.org>> wrote:
>
>     Hello,
>
>     Le lun. 30 sept. 2019 à 18:11, Ivan Postolski
>     <ivan.postolski at gmail.com <mailto:ivan.postolski at gmail.com>> a écrit :
>
>
>         Thanks for the fast reply. I'm running frama-c from the
>         command line. Do you know where should I look for this meta-data?
>
>     This information is stored in Frama-C's internal datastructures
>     (namely the Abstract Syntax Tree, AST). To obtain it,
>     you'll have to attack Frama-C's API and write an OCaml script. In
>     order to obtain something that does exactly what you want, you
>     will probably need to have a look at the developer manual
>     (http://frama-c.com/download/plugin-development-guide-19.1-Potassium.pdf),
>     but here is a small script that will just print on the standard
>     output the location of the statements:
>
>     --------- script.ml <http://script.ml>
>     open Cil_types
>     open Cil
>
>     include Plugin.Register(
>                 struct
>                   let name = "display-loc"
>                   let shortname = "dl"
>                   let help = "quick demo plug-in for displaying
>     location info"
>                 end)
>
>     module Output =
>       False(
>           struct
>             let option_name = "-display-loc"
>             let help = "display location of all statements"
>           end)
>
>     class display_location = object
>       inherit Visitor.frama_c_inplace
>       method! vglob_aux g =
>         match g with
>           | GFun(f,_) ->
>               Format.printf "Now considering function %s at ."
>     f.svar.vorig_name;
>               DoChildren
>           | _ -> SkipChildren
>
>       method! vstmt_aux s =
>         let loc = Cil_datatype.Stmt.loc s in
>         Format.printf "Kept statement at %a:@\n%a at ."
>           Printer.pp_location loc
>           Printer.pp_stmt s;
>         DoChildren
>     end
>
>     let print_sliced () =
>       if Output.get () then
>         Visitor.visitFramacFileSameGlobals (new display_location)
>     (Ast.get())
>
>     let () = Db.Main.extend print_sliced
>
>     ---------------
>     We register it as a plugin in order to be able to register a new
>     option `-display-loc` to control whether the print should occur in
>     `print_sliced`, the main entry point of the plugin, which in turn
>     gets registered in Frama-C's own main entry point. This option is
>     useful to ensure that `print_sliced` is called only on the
>     projects we are interested in by using the `-then*` options of the
>     command-line to properly sequence the things Frama-C should do. A
>     call to Frama-C would then be along those lines:
>
>     frama-c -load-script script.ml <http://script.ml> file1.c file2.c
>     -slice-return main -then-last -display-loc
>
>     Best regards,
>     -- 
>     E tutto per oggi, a la prossima volta
>     Virgile
>     _______________________________________________
>     Frama-c-discuss mailing list
>     Frama-c-discuss at lists.gforge.inria.fr
>     <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>     https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/List
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191002/d6cd3b68/attachment-0001.html>