source: CIVL/examples/focus/sv-benchmarks-main-c-array-industry-pattern/c/array-industry-pattern/bug.c@ bb03188

/* Verifiable with mods:
 * Changed S *a[N] to S a[N] because of CIVL bug: Pointer symbolic info not simplified before dereference. Trying to fix this leads to deeper CIVL bug.
 */
typedef unsigned int size_t;
#include <stdlib.h>
#include <assert.h>
#pragma CIVL ACSL

extern int __VERIFIER_nondet_int(void) {
  int x;
  $havoc(&x);
  return x;
}
$input int N;
$assume(0 < N);
struct _S
{
        int *p;
        int n;
};
typedef struct _S S;

S *a[N];
int user_read()
{
        int x = __VERIFIER_nondet_int();
        return x;
}

int main()
{
        int i;

  //@ transform flatten I;
  for(i = 0; i < N; i++)
        {
                S *s1 =  (S *)malloc(sizeof(S));
                
                s1 -> n = user_read();
                
                if(s1 ->n == 1)
                {
                        s1 -> p = (int *)malloc(sizeof(int));
                }
                else
                {
                        s1 -> p = (void *)0;
                }
                a[i] = s1;
        }

  // Modified
  //@ transform flatten I;
  $assert($forall(int i:0..N-1) (a[i]->n == 1) == (a[i]->p != (void *)0));
  // Original
  /*
        for(i = 0; i < N; i++)
        {
                S *s2 = a[i];

                if(s2 ->n == 1)
                {
                        __VERIFIER_assert(s2 -> p != (void *)0);
                }
        }
  */

  /*
  //@ transform flatten I;
  for(i = 0; i < N; i++)
  {
    if (a[i]->n == 1) {
      free(a[i]->p);
    }
    free(a[i]);
  }
  */
        return 0;
}