Fix SPARK warning regarding nonvolatile functions