Skip to content

Printf arguments are not evaluated #1758

Closed
@Robotechnic

Description

@Robotechnic

If found this while manipulating goblint.
When running goblint with ana.arrayoob set to true I found out that this code:

#include <stdio.h>

int table[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};

int main() {
    for (int i = 0; i < sizeof(table); i++) {
        table[i] = 0;
    }
    printf("\n");
    return 0;
}

Causes a warning to appear which is normal. But this code:

#include <stdio.h>

int table[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};

int main() {
    for (int i = 0; i < sizeof(table); i++) {
        printf("%d ", table[i]);
    }
    printf("\n");
    return 0;
}

Doesn't trigger any warning. Turns out that it does the same with other types of warning. For instance, with ana.int.interval:

#include <stdio.h>
#include <limits.h>

int main() {
    int a = INT_MAX + 1;
    return 0;
}

Causes a warning, while

#include <stdio.h>
#include <limits.h>

int main() {
    printf("%d\n", INT_MAX + 1);
    return 0;
}

don't

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions