Skip to content

No body for 'free' during inlining when using goto-instrument with dfcc #8687

@archigup

Description

@archigup

When building files with dfcc, and a function exists in the translation unit that calls free, we get an error from goto-instrument.

This was tested with the main branch (commit 062962c).

This affects a lot of our files as we have a header with a static inline function that calls free.

I've minimized a reproducer here:

test.c:

#include <stddef.h>
#include <stdlib.h>

void foo(void) {
    free(NULL);
}

int main(void) {
}

commands to repro:

$ goto-cc test.c -o test.goto 
$ goto-instrument test.goto test.goto --dfcc main
Reading GOTO program from 'test.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
file <builtin-library-__CPROVER_contracts_library> line 1077 function __CPROVER_contracts_write_set_deallocate_freeable: no body for function 'free'
No body for 'free' during inlining
Numeric exception : 0
6$ 

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions