Skip to content

Missing overflow warning on division by -1 #1803

@sim642

Description

@sim642

INT_MIN / -1 is the same as -INT_MIN, which is an overflow.

Goblint warns about it if the expression is constant, but is missing a warning when numerator may be INT_MIN and denominator may be -1:

#include <limits.h>

int main() {
    int bad = INT_MIN / -1; // WARN
    int x, y;
    if (y != 0) {
        bad = x / y; // TODO WARN
    }
    return 0;
}

Metadata

Metadata

Assignees

Labels

sv-compSV-COMP (analyses, results), witnessesunsound

Type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions