Skip to content

(core) Add warning switch for wseq - #1004

Draft
dc-mak wants to merge 1 commit into
rems-project:masterfrom
dc-mak:warn-wseq
Draft

(core) Add warning switch for wseq#1004
dc-mak wants to merge 1 commit into
rems-project:masterfrom
dc-mak:warn-wseq

Conversation

@dc-mak

@dc-mak dc-mak commented May 24, 2026

Copy link
Copy Markdown
Collaborator

No description provided.

@dc-mak

dc-mak commented May 24, 2026

Copy link
Copy Markdown
Collaborator Author

Hmm, it seems a common way weak-sequencing may show up is with prefix incr/decr operators. It might be worth making the analysis more precise (e.g. taking into account promotable symbols can't alias and race), or it might just be that we need to bite the bullet and have it be supported by CN...

#include <stdio.h>

int f() {
    int x = 0;
    int y = --x > x; // UB
    y = --x > y; // ok
    return 0;
}

int main() {
    f();
    int x[5] = {1,2,3,4,5};
    int *start = &x[0];
    int y = 5;
    do {
        printf("%d\n", x[--y]); // ok, rewritable
    } while (&x[y] > start);

    return x[y] - 5;
}

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant