Cannot use ppx_inline_test in a Frama-C plugin
Steps to reproduce the issue
Setup a minimal Frama-C plugin which uses the ppx_inline_tests
test runner, and run tests using dune runtest
.
The test runner is configured according to this documentation: https://dune.readthedocs.io/en/stable/tests.html#inline-tests
Project structure:
hello/
├── dune
├── dune-project
└── hello.ml
dune-project:
(lang dune 3.2)
(using dune_site 0.1)
(name frama-c-hello)
(package (name frama-c-hello))
dune:
(library
(name hello)
(public_name frama-c-hello.core)
(libraries frama-c.kernel)
(preprocess (pps ppx_inline_test))
(inline_tests)
)
(plugin
(optional)
(name hello)
(libraries frama-c-hello.core)
(site (frama-c plugins))
)
hello.ml:
let%test "should fail" = 1 = 2
Expected behaviour
The test inside hello.ml
executes and prints an assertion error.
Actual behaviour
Building the test fails with the following error:
Error: No implementation found for virtual library "frama-c.init" in
/home/tb/.opam/default/lib/frama-c/init.
-> required by library "frama-c.kernel" in
/home/tb/.opam/default/lib/frama-c/kernel
-> required by library "frama-c-hello.core" in _build/default
-> required by
_build/default/.hello.inline-tests/inline_test_runner_hello.exe
-> required by _build/default/.hello.inline-tests/partitions-best
-> required by alias runtest in dune:6
Contextual information
- Frama-C installation mode: installed using
opam install frama-c
- Frama-C version: 28.0 (Nickel)
- Plug-in used: minimal plugin
- OS name: Fedora Linux
- OS version: 38 (Workstation Edition)
Additional information (optional)
The project build just fine using dune build
, only the @runtest
target fails to build.