source: CIVL/mods/dev.civl.com/examples/languageFeatures/mallocBad.cvl@ cb4d4f4

/* Commandline execution:
 *              civl verify mallocBad.cvl
 * */
#include <civlc.cvh>
void main() {
  double *p = (double *) $malloc($here, 5*sizeof(double));
  
  p[4]=3.14;
  $free(p);
  // Uses pointer after free.
  $assert(p[4]==3.14);
}