The specification for the listcopy is listed slightly lower down on the article as follows:
// r :-> x ** linked_list(x,S)
void listcopy(void **r)
// r :-> y ** linked_list(y,S) ** linked_list(x,S)
As the precondition explicitly states that r points to a value x, it can not be NULL, so no NULL checks are needed.I'm not sure what the sibling post is trying to imply with recursive calls though.