[CN] unhelpful error message when struct with padding is leftover

[peterohanley]

I want to start out by saying this is not a bug, CN is behaving correctly here, it's just a little unfortunate.

#include <stdlib.h>
struct list {
  int a;
  #ifdef NAMEPADDING
  int pad;
  #endif
  struct list *next;
};
/*@
datatype List {
  Nil {},
  Cons {datatype List next}
}


predicate (List) OwnedList(pointer p) {
  if (is_null(p)) {
    return Nil{};
  } else {
    take node = Owned<struct list>(p);
    take next = OwnedList(node.next);
    return Cons
      {
       next:  next
      };
  }
}
@*/

void bar(struct list *n)
/*@ requires take ni = OwnedList(n);
    ensures take no = OwnedList(n);
@*/
{
  struct list *cur = n;

  while (cur != NULL)
  /*@ inv
    {n} unchanged;
    take x = OwnedList(cur);
  @*/
  {
    cur = cur->next;
  }
}

% cn verify bst_map.c
[1/1]: bar -- fail
bst_map.c:37:3: error: Left-over unused resource 'each(u64 i; 0'u64 <= i && i < 4'u64)
{Block<char>(&O_cur0[4'u64] + i * 1'u64)}(default(map<u64, u8>))'
  while (cur != NULL)
  ^~~~~~~~~~~~~~~~~~~ 
State file: ...

% cn verify -DNAMEPADDING bst_map.c
[1/1]: bar -- fail
bst_map.c:37:3: error: Left-over unused resource 'Owned<struct list*>(&O_cur0->next)(unpack_OwnedList0.node.next)'
  while (cur != NULL)
  ^~~~~~~~~~~~~~~~~~~ 
State file: ...

@yav and I looked at the original of this for a few minutes in confusion. We knew the invariant was not right and expected an error like the second one, and we couldn't figure out where this mysterious uninitialized memory came from. I still don't know why naming it prevents it from being displayed*. The state file displays all resources but doesn't indicate which are not used (I believe because this information is not reliable in a failing context?).

If it's possible to just indicate that this block is padding, probably when the resource management for the struct is created, that would entirely address this IMO.

* I mean why it's no longer chosen as the main error to indicate on the CLI.