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