Skip to content

CBMC doesn't have a model for clockid_t and clock_gettime #7639

Open
@feliperodri

Description

@feliperodri

CBMC version: 5.80.0
Operating system: N/A

I tried to verify this C program:

uint32_t my_time(void)
{
    struct timespec t;
    clock_gettime(CLOCK_MONOTONIC, &t);
    return (t.tv_nsec / 1000000) + ( (t.tv_sec % 86400) * 1000);
}

but there is no model for clock_gettime in CBMC. I tried to write a stub following the specification, but there was no model for clockid_t either. Adding this issue to add this model at some point.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

    Development

    No branches or pull requests

      Participants

      @feliperodri@TGWDB

      Issue actions

        CBMC doesn't have a model for `clockid_t` and `clock_gettime` · Issue #7639 · diffblue/cbmc