'Ensures' example regarding security bug is misleading

Example, bad: Consider a famous security bug

 void f() // problematic
 {
  char buffer[MAX];
  // ...
  memset(buffer,0,MAX);
 }

There was no postcondition stating that the buffer should be cleared and the optimizer eliminated the apparently redundant memset() call:

 void f() // better
 {
  char buffer[MAX];
  // ...
  memset(buffer,0,MAX);
  Ensures(buffer[0]==0);
 }

This implies that the second version averts the security bug. But this isn't true: the compiler is free to note that buffer[0]==0 should always be true at the point, replace the argument with a constant true, then make the same elimination of the memset call. And in fact, both GCC and Clang do so. The only correct way to avoid the security bug is to use a special-purpose function like memset_s (or maybe volatile).