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] Support LLVM database "compile_commands.json"

The problem that you are having with the Frama-C GUI is that the lablgtk packages from the Ubuntu repository conflict with those from OPAM. If I remember correctly, someone from Debian renamed some dependencies with different names than those used by OPAM, which makes it impossible to mix them.

The solution is simple: uninstall any and all *-ocaml packages from your Ubuntu. You should have none of them at all, OCaml packages from Ubuntu and OPAM do not mix well. If you ever need OCaml-based software, you should install it via OPAM, not Ubuntu. As far as I know, everything OCaml that has an Ubuntu package also has an OPAM package (but not the other way around!), so you shouldn't be missing anything.

Then, once you've purged the *-ocaml packages from your system, install OPAM from the binary provided in their website, and from there install all of the dependencies for Frama-C, including lablgtk. That way it should work.

More specifically, once you download opam_installer.sh from the OPAM website, ask it to install OCaml 4.02.3 (the default is 4.02.1, which is not supported by the most recent Frama-C releases, so by expliciting asking 4.02.3 you'll save some time):

./opam_installer.sh BINDIR 4.02.3 (replace BINDIR with a directory in your PATH, in which the opam binary itself will be installed; note that all other files will be put in ~/.opam)

Then install depext, use it to install Frama-C's external (non-OCaml) dependencies, and then install Frama-C itself:

opam install depext
opam depext frama-c
opam install frama-c

This might prompt you to install the required GTK-related packages, but NOT the Ubuntu OCaml packages.

Once this is done, you should have the GUI working as expected (Ubuntu 16.04 is used by many Frama-C developers, in fact, all of which use the GUI routinely).


About the stubs I mentioned, I think there are not many examples, other than some function specifications in the Frama-C libc, for instance in string.h.

The idea of these stubs is that they emulate the behavior of the C functions in a way that is sufficiently abstract, so that the stubs are easier to write than the actual source code, but also sufficiently concrete so that all possible behaviors in the real code are taken into account.

For EVA in particular, there is the possibility of combining both ACSL postconditions, and Frama-C builtins (e.g. Frama_C_interval), to simulate non-determinism, and abstract away some details.

A very crude example of what I mean by "stubs" is the example below, where we use Frama-C built-ins to emulate a subset of possible command-line arguments given to a C program.
void prepare_initial_context() {
  int argc = Frama_C_interval(0, 5);
  char argv0[256], argv1[256], argv2[256], argv3[256], argv4[256];
  char *argv[5] = {argv0, argv1, argv2, argv3, argv4};
  for (int i = 0; i < 5; i++) {
    for (int j = 0; j < 256; j++) {
      argv[i][j] = Frama_C_interval(0, 255);
    }
  }
  main(argc, argv);
}

In this configuration, we suppose the command-line may contain any number of arguments between 0 and 5, and each argument contains a string of up to 256 characters. Note that we never ensure that the strings terminate with a '\0' character, so this is not entirely realistic; also, they may contain '\0' characters anywhere, so their length is effectively anything between 0 and 255. Finally, it must be noted that due to the fact that all strings are allocated with 256 characters, the modelization cannot detect some kinds of invalid memory accesses. What I want to highlight here is that, by mixing C code and Frama-C builtins, you can give EVA enough information for the analysis to be sound, without having to write ACSL specifications (or writing a reduced amount of them).

Unfortunately, this can quickly scale when dealing with stateful contexts, imperative data structures, and so on. For instance, if you'd like to stub a function that accesses the filesystem, you'd have to create model variables for the file system (e.g. using ACSL ghost variables), with the proper abstraction level (should you model each file descriptor with a single int? Or, instead, with a struct containing several fields? Maybe a buffer should be included? etc.), and then write the pseudocode for the functions accessing this filesystem, and updating your model variables accordingly. In the end, it is often easier to use the actual source code, unless a high-level view is sufficient for your needs. The case of libuv in particular, which is asynchronous, is even more complicated, since EVA does not deal with concurrency (there is a derived plug-in for that, Mthread, but you need to know how to use EVA before using it anyway). It's not unlikely that including the actual source code of libuv in the analysis would be a faster solution, although in the end, you'd have something which EVA is not currently able to handle anyway. My advice here would be to try something simpler first, and leave this for later.

I hope this clarifies about the stubs. Otherwise, feel free to ask more questions.
________________________________________
De : Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Matt [mattator at gmail.com]
Envoyé : vendredi 2 juin 2017 23:04
À : Frama-C public discussion
Objet : Re: [Frama-c-discuss] Support LLVM database "compile_commands.json"

That's really cool ! I've upgraded frama-c from opam and succeeded
completing the analysis thanks to your flag. I will try to fix the GUI
compilation otherwise I am not sure how to exploit the data.

> (e.g. from libuv ; such stubbing might be done via ACSL specifications
Any keyword I could lookup to ? I suppose I could generate the stubs
via pygccxml/castxml ? what's the usual thing ?

>If you just want to see how EVA works on an almost-ideal case (embedded software), I'd recommend case study debie1-e-free from the open-source-case-studies repository. You can easily modify the provided Makefile and obtain different analysis results, and try to add some ACSL specifications here and there and see how they impact the analysis. It's a small code base, but in my opinion a much better environment to "get a feeling about formal methods", without having to deal with several concurrent issues all at once.
Thanks for the tip, I might very well do that even if I aim at
applying those techniques on "real" software.

>If you want a tutorial oriented towards functional specifications, based on deductive verification, I'd recommend ACSL by Example. Finally, there is a tutorial on the WP plug-in (deductive verification) on https://github.com/AllanBlanchard/tutoriel_wp/ (the original version is in French only, but it is being translated into English).
This was part of my plan. Le francais ne devrait pas etre un problème :)

@+
Matt