Skip to content

Segfault in goto-cc for the syntactically incorrect C file #7770

Open
@rodionov

Description

@rodionov

CBMC version:

goto-cc --version
gcc (goto-cc 5.85.0 (cbmc-5.85.0)) 12.2.0

Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger
CBMC version: 5.85.0 (cbmc-5.85.0)
Architecture: x86_64
OS: linux
gcc: 12.2.0

Exact command line resulting in the issue:

cat > test.c<< EOF
void *malloc(unsigned long size) {
    int return_null;
    if (return_null) return 0;
    // malformed line below, should be: else return __CPROVER_allocate(size, 0); 
    else  __CPROVER_allocate(size, 0); 
}
EOF
goto-cc test.c
Segmentation fault

What behaviour did you expect:
I was expecting goto-cc to produce invalid syntax error instead of segfaulting.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions