Confusion between C and CN names when testing

[yav]

In CN the names used in specs and the names in C live in different namespaces, but this is not reflected during testing.
Here are some examples:

/*@                                                                              
function (boolean) f() { true }                                                     
@*/                                                                                 
                                                                                 
void f() {}   

This leads to "conflicting types for f"

The same sort of thing happens with type declarations, for example:

struct List
{
  int value;
  struct List* next;
};

/*@
datatype List {
  Nil {},
  Cons { i32 head, List tail }
}

predicate List ListSegment(pointer from, pointer to) {
  if (is_null(from)) {
    assert(is_null(to));
    return Nil {};
  } else {
    take head = Owned<struct List>(from);
    take tail = ListSegment(head.next, to);
    return Cons { head: head.value, tail: tail };
  }
}
@*/

This leads to "redefinition of struct List"

cn --version
git-e4de4e424 [2024-11-07 16:37:28 +0000]