Showing error 1456

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: list-properties/splice_safe.i
Line in file: 678
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

648  p->h = 3;
649  if (a->h == 3) return 0;
650  flag = 1;
651  l1 = 0;
652  l2 = 0;
653  p = a;
654  while (p->h != 3) {
655    t = p;
656    p = p->n;
657    if (flag) {
658      t->n = l1;
659      l1 = t;
660      flag = 0;
661    } else {
662      t->n = l2;
663      l2 = t;
664      flag = 1;
665    }
666  }
667  p = l1;
668  while (p != 0) {
669    if (p->h != 1) goto ERROR;
670    p = p->n;
671  }
672  p = l2;
673  while (p != 0) {
674    if (p->h != 2) goto ERROR;
675    p = p->n;
676  }
677  return 0;
678  ERROR: return 1;
679}
Show full sources