AV: an interesting example that cannot be easily blocked with non-aliasing vocabulary

[shaobo-he]

Consider the following example,

struct node
{
   struct node * prev;
   struct node * next;
   int flag;
};

typedef struct node node;

void remove(node* this)
{
   this->prev->next = this->next;
   this->next->prev = this->prev;
   this->prev = 0;
   this->next = 0;
}

void foo(node* head)
{
   node* n;
   while((n = head->prev)->flag)
     remove(n);
}

There will be an error trace if the recursion bound is set to 2, which cannot be blocked by our default configuration (non aliasing + non monomial cover.

[zvonimir]

I am guessing nobody will work on this any time soon, if ever. @shuvendu-lahiri and @akashlal : are you ok if I mark this as "won't fix" and close the issue?