Skip to content

CBMC malloc should be able to non-determinstically fail #4605

Closed
@danielsn

Description

@danielsn
#include <assert.h>
#include <stdlib.h>
#include <stdint.h>

int main() {
    char*p = malloc(100);
    assert(p);
}

the assertion never triggers, tho it ought to be able to, given that real malloc can fail.

Metadata

Metadata

Assignees

No one assigned

    Labels

    awsBugs or features of importance to AWS CBMC usersaws-medium

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions