Module Codex_options.Location

TODO: We should have a "callstack" or "Location" module.

With functions to retrieve the current callstack, current kinstr etc. which would be centralized.

And maybe functions like inside_function, inside_kinstr etc.

Internally this would rely on Tracelogs loc, but we would not see it from the outside.

Maybe we could check internal invariants, such as we cannot be inside a kinstr inside another kinstr etc, on construction.

The driving design of this module: we use OCaml's interpreter structure of calls and return to manage a (global, or per-domain) interpreter callstack.

Note: maybe assume, the current context and the control flow graph could be handled this way? Indeed, I could probably retrieve the CFG using this infrastructure. Not sure that it is a good idea though.

module L : sig ... end

include module type of struct include L end

include sig ... end

type location = Tracelog.location = ..

type location +=

1. | Function of Frama_c_kernel.Kernel_function.t
2. | Kinstr of Frama_c_kernel.Cil_types.kinstr
3. | JoinPoint of Frama_c_kernel.Cil_types.kinstr * Frama_c_kernel.Cil_types.kinstr
4. | FunctionReturn
5. | Expression of Frama_c_kernel.Cil_types.exp

type t = location

val pp_loc : Stdlib.Format.formatter -> location -> unit

val pp_loc_stack : Stdlib.Format.formatter -> location list -> unit