sig val compute_using_specification : Cvalue.V.t Eval.call -> Cil_types.funspec -> call_kinstr:Cil_types.kinstr -> with_formals:Cvalue.Model.t -> Value_types.call_result Eval.or_bottom end