My feeling is that the above clause 7.24.2.1:2 is faithfully formalized as the ACSL pre-conditions quoted at the beginning of the post. This feeling come from the contrast with the memchr function: 7.24.5.1:2 The memchr function locates the first occurrence of c (converted to an unsigned char) in the initial n chara...