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 cil package.
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 --root=DIR option);
inside it, create a subdirectory, for instance foo;
run 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 foo/script.ml (script.ml can be named as you wish);
run dune build @install to build it locally;
run 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:
open Frama_c_kernel
let () =
match Cil.constFoldToInt
(Cil.sizeOf ~loc:Cil_datatype.Location.unknown
(Cil_types.TInt (Cil_types.IChar, [])))
with
| 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.