Module Oneret

module Oneret: sig .. end

type returns_clause = Cil_types.stmt * Cil_types.behavior * Cil_types.identified_predicate 
type goto_annot = Cil_types.stmt * Cil_types.code_annotation 
type callback = returns_clause -> goto_annot list -> unit 
val oneret : ?callback:callback -> Cil_types.fundec -> unit

Make sure that there is only one Return statement in the whole body. Replace all the other returns with Goto. Make sure that there is a return if the function is supposed to return something, and it is not declared to not return.