How to use Domain_builder module?

user_15647454 0
Viewed 61

I would like to implement a simple abstract domain using functors provided by module Domain_builder (documented in section EVA->Domains), but I am not able to open the module. A simple ocaml file x.ml:

open Domain_builder

and command frama-c -load-script x.ml produce error Unbound module Domain_builder. I am, however, able to import other modules documented in this section (e.g. Cvalue).

It seems that module Domain_builder is not exported by EVA's .mli file (https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/value/Eva.mli), but neither is Cvalue module.

Am I doing something wrong, or is Domain_builder module really missing in EVA's signature?

frama-c
1 Answers

Sadly, you're right, Domain_builder cannot be used outside of Eva for now (NB: if it was exported, you'd have to open Eva.Domain_builder in any case).

As for why Cvalue is available: for historical reasons, this module, together with all files within src/plugins/value_types are in fact considered as kernel modules.

user_16336650
Related