The semantics of pure and const that we use are slightly different from those defined by GCC. GCC specifies that both pure and const functions must terminate. In our method, we annotate the procedures without trying to prove termination. This could potentially cause problems if GCC hoisted a call to a non-terminating function so that it was called before it would have been. (We do not know if GCC actually does this, but the specifications of pure and const would seem to allow it.)
To prevent this, we could be conservative and only annotate functions that we could prove will terminate. Alternatively, the GCC optimization pass could be modified so that it never moved a function call to an annotated function above side effects or earlier than it is anticipated.
Because this could potentially cause incorrect results (with non-terminating functions), it would be important to resolve this issue before adopting it in a real system.