For profiling Cerberus OCaml code could be instrumented with Landmarks
To use profiling you need to build with profiling support enabled using the following command:
make PROFILING=true
For example, to run Cerberus for CHERI C with profiling enabled:
dune exec --workspace=dune-workspace.profiling --context profiling-auto --no-print-directory --display=quiet --auto-promote --root=$pwd cerberus-cheri -- example.c
To run it without profiling:
dune exec --no-print-directory --display=quiet --auto-promote --root=$pwd cerberus-cheri -- example.c