Best way to translate while loops to functions for software verification

Question

I have a verification engine where while loops are translated into functional code, like this:

def f() = ... while(c) b ...

def f() = ... fwhile() ...                        
def fwhile() = if(c){ fwhile() } 

We want for the users to be able to annotate while loops with a decreases construct which says that certain measure decreases at each iteration. This is used to prove termination as follows:

while (x > 0) {
 decreases(x)
 x = x - 1
}

The problem is that the checker of the decreases uses the hints given by the preconditions of the functions it is working with. We cannot specify that the precondition is the while loop condition since it may be false at the first call. From my side, I proposed the following translation:

def f() = ... if(c) fwhile() else ...        
def fwhile() = b if(c) fwhile() else ...

I would like to have some feedback on the correctness of my approach as well as if there are any better options, since still this will require moving in function f a part of the while which should be naturally contained in the fwhile function.