Best way to translate while loops to functions for software verification
I recommend that you translate

while(c) b


to

def myWhile() = if (c) then (b ; myWhile())
myWhile()


With this translation, the precondition of myWhile is the loop invariant of the original while loop.  So, this becomes the question of how to find the loop invariant of a loop.  In general, that requires manual annotation.  If you do a search, you should be able to find a lot of information on finding loop invariants.