sig
  val compute_using_specification_single_behavior :
    Kernel_function.t ->
    Cil_types.funspec ->
    call_kinstr:Cil_types.kinstr ->
    with_formals:Cvalue.Model.t -> Value_types.call_result
  val compute_using_specification_multiple_behaviors :
    Kernel_function.t ->
    Cil_types.funspec ->
    call_kinstr:Cil_types.kinstr ->
    with_formals:Cvalue.Model.t -> Value_types.call_result
end