Module `Debugger_lifter.Gil_fallback_lifter`

A Lifter implementation that acts as a proxy to another lifter (TLLifter), while also keeping a Gil_lifter updated alongside.

TLLifter can access the GIL lifter and its state via Gil_lifter_with_state.

Note that if the GIL lifter gives anything other than Stop when handling a command, it is considered skipped, and TLLifter won't be asked to handle it.

module type Gil_lifter_with_state = Gil_fallback_lifter.Gil_lifter_with_state

A Gil_lifter, along with a function to get its state

module Make
  (SMemory : Engine.SMemory.S)
  (PC : Gillian.Command_line.ParserAndCompiler.S)
  (TLLifter : 
    functor (Gil : sig ... end) ->
    functor (V : Engine.Verifier.S with type annot = PC.Annot.t) ->
    sig ... end)
  (V : Engine.Verifier.S with type annot = PC.Annot.t) : 
  sig ... end