Skip to content

More precise float domain for float and double #919

@michael-schwarz

Description

@michael-schwarz

In these cases we can have a more precise interval domain (float option * float option) option * bool where the inner values are for the interval (None for the infinite cases), and the outer bool represents whether NaN is a possible value or not.

Currently we cannot benefit from guards such if(5.0f < x && x < 10.0f): For the first part, we cannot express that x needs to be betweeen 5 and +Infinity, as our domain expresses this as T.

Such a treatment is only possible when we know that the type we are using to represent a value matches the concrete one. If we will participate in SV-COMP 24, that might yield some improvement in the floats category.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions