Infer needs assert statements to remove false positives

[thanhtoantnt]

I run Infer using the following program.

• Without the two assert statements, Infer doesn't know that ListRawPushBack cannot return -1. Hence, it reports a memory leak: Memory dynamically allocated by malloc on line 58 is not freed after the last access at line 62, column 13
• After adding two assert statements, Infer reports no error in the program: No issues found.

My question is whether we could configure Infer to know the two constraints without adding assert statements.

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

struct RawListNode {
    struct RawListNode *next;     /**< points to the next node */
    struct RawListNode *prev;     /**< points to the previous node */
};

typedef struct RawListNode RawListNode;

struct ListNode {
    struct RawListNode rawNode;
};

typedef struct ListNode ListNode;

typedef struct {
    struct RawListNode  head;
} RawList;

struct DoublyLinkedList {
    RawList rawList; // Linked list header
};

typedef struct DoublyLinkedList DoublyLinkedList;

void ListRawAddAfterNode(struct RawListNode *node, struct RawListNode *where)
{
    node->next       = (where)->next;
    node->prev       = (where);
    where->next      = node;
    node->next->prev = node;
}


void ListRawAddBeforeNode(RawListNode *node, const RawListNode *where)
{
    ListRawAddAfterNode(node, where->prev);
}

int ListRawPushBack(RawList *list, RawListNode *node)
{
    if ((list != NULL) && (node != NULL)) {
        ListRawAddBeforeNode(node, &(list->head));
        return 1;
    }

    return -1; // NOTE: Infer cannot check that this branch is unreachable.
}

int DoublyLinkedListPushBack(DoublyLinkedList *list)
{
    int ret = -1;
    ListNode *node = NULL;

    if (list != NULL) {
        node = malloc(sizeof(ListNode));
        if (node != NULL) {
            // assert(&list->rawList != NULL);
            // assert(&node->rawNode != NULL);
            ret = ListRawPushBack(&list->rawList, &node->rawNode);
        }
    }

    return ret;
}

int main() {
    return 0;
}

Please include the following information:

• The version of infer from infer --version: v1.2.0
• Your operating system and version: Ubuntu 22.04
• Which command you ran, for example infer -- make: infer -- clang examples/example.c