I did a rewrite of the majority of the logic that I had previously added for the memory OOB access checks. Still need to try and make it more precise.

Also, for some reason I can't get the BlobSize query for a pointer, which has dynamically allocated memory, to give me a meaningful result (i.e., not top). We should probably discuss this and see what's wrong there. I'm pretty sure I'm doing something wrong in my code.

@michael-schwarz Nonetheless, feel free to take a look at the PR and leave some feedback :)

Did yet another rewrite of the logic for this PR:

• make test runs through successfully.
• An open issue that's left is handling memory OOB accesses due to loops, such as the one in test case 77/03

Feel free to review

As a workaround, I would suggest disabling the info warnings category for this test with --disable warn.info, leaving a comment that this is not a longterm solution.

This is now added in 2b45499

It seems like the current implementation gets confused by string constants, causing quite a few normally simple CWE tests to fail, because they contain code like this:

// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>
#include <stdio.h>

void myPrint(char *str) {
    printf("%s", str);
}

int main(int argc, char const *argv[]) {
    myPrint("starting test");
    // Some stuff
    myPrint("ending test");    
}

[Warning][Unknown] Pointer str has an empty points-to-set (tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c:6:5-6:22)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer str not known. Memory out-of-bounds access might occur due to pointer arithmetic (tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c:6:5-6:22)

This should be easy to fix as we have a special representation of such string constants in the address domain, for which we could just consider all accesses to be within bound.

It seems like the current implementation gets confused by string constants, causing quite a few normally simple CWE tests to fail, because they contain code like this:

// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>
#include <stdio.h>

void myPrint(char *str) {
    printf("%s", str);
}

int main(int argc, char const *argv[]) {
    myPrint("starting test");
    // Some stuff
    myPrint("ending test");    
}

[Warning][Unknown] Pointer str has an empty points-to-set (tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c:6:5-6:22)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer str not known. Memory out-of-bounds access might occur due to pointer arithmetic (tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c:6:5-6:22)

This should be easy to fix as we have a special representation of such string constants in the address domain, for which we could just consider all accesses to be within bound.

This should be now fixed by commit 3258cce in the staging_memsafety branch. If you think it makes sense, we can cherry-pick this, as well as other commits from the staging-memsafety branch, which have introduced some changes and fixes to memOutOfBounds.ml

If you think it makes sense, we can cherry-pick this, as well as other commits from the staging-memsafety branch, which have introduced some changes and fixes to memOutOfBounds.ml

Probably a good idea, yes!

This should be now fixed by commit 3258cce in the staging_memsafety branch. If you think it makes sense, we can cherry-pick this, as well as other commits from the staging-memsafety branch, which have introduced some changes and fixes to memOutOfBounds.ml

We discussed that these changes will be taken after this PR's branch is merged into master, since cherry-picking them now would cause a lot of conflicts.

The CI job on MacOS is failing again, this time due to the 04/58 regr. test case. I'm strongly assuming that it's due to the issue, documented in #1151. Should we temporarily change some annotations of this test case as well?

The CI job on MacOS is failing again, this time due to the 04/58 regr. test case.

Probably fixed as of 7f9ec9a. I'll merge master into this again and if the CI passes then, I'll merge the PR.

The CI job on MacOS is failing again, this time due to the 04/58 regr. test case.

Probably fixed as of 7f9ec9a. I'll merge master into this again and if the CI passes then, I'll merge the PR.

Awesome, thanks!