C.ExternalSemantics
module Val : Gillian.General.Val.S
module ESubst : sig ... end
module Store : sig ... end
module State : sig ... end
module Callstack : sig ... end
val execute : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i