Skip to content

Coverage generates incomplete source location #6978

Closed
@markrtuttle

Description

@markrtuttle

CBMC version: 5.53.1
Operating system: Red Hat 7.3.1-13

Create the file main.c

#include <string.h>

#define BUFLEN 100

static void * (* const volatile memset_func)( void *, int, size_t ) = memset;

int main()
{
  char buffer[BUFLEN];
  memset_func(&buffer, 0, BUFLEN);
}

and run

cbmc --cover location main.c

and notice that in the output

** coverage results:
[main.coverage.1] file main.c line 9 function main block 1 (lines main.c::5; main.c:main:9,10): SATISFIED
[main.coverage.2] file main.c line 11 function main block 2 (lines main.c:main:11): SATISFIED

the line main.c::5 is missing a function name as the second component. I'm not sure what name makes sense here, but prior to this example it has been an invariant that source location information reported in coverage data included file, function, and line numbers.

Metadata

Metadata

Assignees

No one assigned

    Labels

    awsBugs or features of importance to AWS CBMC usersaws-highpending merge

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions