I tried to install an old version of frama-c (because library cil requires ocaml < 4.06) …
opam switch create 4.05-ocaml-cil 4.05.0+rc1
opam install frama-c
everything seems fine:
opam list | grep frama-c provides
frama-c 21.1 Platform dedicated to ...
$(opam var lib)/frama-c provides
/home/***/.opam/4.05-ocaml-cil/lib/frama-c: Is a directory
frama-c --version is providing
dune build is complaining
Error: The package frama-c is not found and
ocamlfind list do not know or list the package.
I found similar topics, e.g. https://discuss.ocaml.org/t/package-not-found-after-opam-install/11044, but I wasn’t able to solve my issue.
I appreciate hints in all directions:
- How can I fix this gap between opan and ocmalfind?
- Why is it not possible to use the cil-library (I need cil_types) with a current version of ocaml?
- Did I made something wired???
Thanks a lot in advance!!!
I’m not entirely sure what you are trying to do, but it seems something may have led you astray.
You mention that the
cil library requires OCaml < 4.06, which is nowadays a very old version. Indeed, as far as we know, the
cil library is no longer maintained. But Frama-C includes its own (modified) version of CIL, which is completely independent from the
By the way, the version suffix
+rc1 means it is a release candidate, so older than the actual 4.05 version. In such cases, consider installing the “base” version, it will be more stable than a release candidate.
Now, why the cil project is no longer maintained, I don’t know. But if you want to use Frama-C’s version of
Cil_types, just install a recent OCaml compiler, a recent Frama-C package, and configure a dune project to import Frama-C’s kernel. (I’ll try to provide a working example later.)
The last Frama-C version compatible with that old OCaml compiler (4.05) is indeed version 21. Frama-C did not use
dune back then, so the available API was different. I’ll check about the other issues (dune build error and ocamlfind), but to answer your last 3 questions:
- I’m not sure yet, I’ll check a few things related to it, but you probably won’t have the issue anyway, if you use a recent Frama-C. By the way, do not mix
opam packages with
ocamlfind packages; even if in many cases both exist with identical names, this is not always true.
- Because cil library is no longer maintained, for several years now. But you can try using Frama-C’s Cil_types instead.
- Yes, you probably mixed up CIL and Frama-C’s CIL, and that is causing issues. Given that CIL is no longer a maintained package, I’m assuming you will be fine using Frama-C’s version of the library. So I’ll try providing some instructions about using its latest version.
In the meanwhile, if someone more savvy about ocamlfind could step in and explain the issue, that might help.
Not sure if it’s only CIL you want, but the Goblint project still maintains a fork of standalone CIL: GitHub - goblint/cil: C Intermediate Language. It is also published on opam as goblint-cil.
If you want something to do with Frama-C, then goblint-cil won’t be relevant to you. Also, it has likely deviated significantly from Frama-C’s integrated version.
Thanks for mentioning goblint-cil, I knew I had seen some recent version of cil somewhere but I couldn’t find it anymore, so I assumed I just misremembered it.
I just tried producing a minimal example of using the Frama-C kernel for Cil_types, and frankly, it’s not as simple as I would like it to be.
Recent Frama-C versions have a
frama-c-build-scripts.sh that should help, but it’s still cumbersome. Here’s how I produced a minimal example:
- Create a directory somewhere (not inside a directory already containing a
dune-project file, otherwise things will not work well! This also applies to parent folders, none of them may contain a
dune-project, or you’ll have to manually set the
- inside it, create a subdirectory, for instance
frama-c-build-scripts.sh init foo (if you installed a recent Frama-C, this script should be in your PATH);
- put your code in a file such as
script.ml can be named as you wish);
dune build @install to build it locally;
dune exec -- frama-c -load-library frama-c-scripts.foo. You should obtain the result of running your code.
- you can also run
dune install, then you don’t need the
dune exec -- part. But this will install the “library” in your opam PATH. You can run
dune uninstall to remove it.
Here’s the example code I tested:
let () =
(Cil_types.TInt (Cil_types.IChar, )))
| None -> Format.printf "constfold failed@."
| Some sz -> Format.printf "sizeof(char) = %d@." (Integer.to_int_exn sz)
As expected, running
dune exec -- frama-c -load-library frama-c-scripts.foo will output:
sizeof(char) = 1
But this is way more complex than I would expect it. Unfortunately, the way Frama-C is currently developed, you cannot simply take the kernel and use it as a library; you actually need to create a Frama-C library (almost the same as a Frama-C plug-in, in fact) and load it when running Frama-C itself.
So, if it is really only CIL that you need, using goblint-cil will probably be an easier approach.
Thank you so much guys, you helped me a lot by providing such a detailled description.
I recognised, that cil (or cil_types) is from 2013 and totally outdated, but I didn’t got that frama-c is using its own librarys, which seems to be highly extended.
I didn’t explained my goal in general, but the CIL-Module is pointing to c-analysis, so we decided to move closer to frama and I found my solution in the plug-in-delevloper-guide of frama-c.
Thanks for the efforts and time you spend!