Add all math.h functions in libraryFunctions.ml with readsAll in libraryFunctions.ml

[brgr]

This makes it s.t. globals are not invalidated anymore when math.h functions are encountered.

[Dudeldu]

At this point, i have to trust in your understanding of that... ;)
Do we want to add a regression test to proof/check it?

[FelixKrayer]

Looking good.
I think a test is not really needed here.
I can also put in a test for one or two of them (ideally ones we don't directly implement) when I add a test for the Implementation of isnan, cos, etc

[Dudeldu]

Have you also considered something like errno which is definitely updated by a few of those functions?

[brgr]

I had a regression test that had all these functions inside. If you want I can add it again, but it seemed kind of useless to me, which is why I removed it again.

@Dudeldu By errno, you mean this, right? https://man7.org/linux/man-pages/man3/errno.3.html

That's a good question, but I guess this is just accepted. At least stuff like fclose is also in this list, and also with readsAll, even though it could also write to errno.

I think we can just keep it like this. Is that fine with you? Otherwise I can of course ask :)

[michael-schwarz]

I'll quickly bud in here, we currently ignore errno completely, but feel free to open an issue in goblint/analyzer: We probably unsoundly assume it is always 0, while we should assume it is T.

[Dudeldu]

If errno isn't treated correctly anyway, there is also no reason for invalidating it as far as i can see. And regarding the tests, you are probably right and Felix will add them once those functions have an actual meaning.

[brgr]

I'll quickly bud in here, we currently ignore errno completely, but feel free to open an issue in goblint/analyzer: We probably unsoundly assume it is always 0, while we should assume it is T.

Ah, really cool, thanks for the quick clarification! Then I would just ignore it for now - or should I open an issue anyway, just for you guys to have it on the list?

[michael-schwarz]

or should I open an issue anyway, just for you guys to have it on the list?

That would be great, especially if you can come up with an example where we are actually unsound!

[brgr]

I looked at this again now (I didn't have time yesterday anymore) and it actually seems like this is handled. There even is a test for this: 00-sanity/12-errno.c.

I also wrote a test with something where I knew that errno was changed:

int main()
{
    FILE *fp;
    int errno_save;

    errno = 0;
    assert(errno == 0);
    fp = fopen("non_existent.txt", "r");

    errno_save = errno;

    if (errno_save != 0)
    {
        printf("fopen failed\n");
        assert(errno == 0); // UNKNOWN!
        exit(1);
    }

    fclose(fp);
    exit(0);
}

This goes into the if branch and with goblint I also get for the assert: Assertion "*tmp___2 == 0" is unknown..

However, I tried to find where this is handled in the code but could not find, which is why I'm still a bit unsure.

@michael-schwarz Can you confirm that this is fine then?

[michael-schwarz]

I checked, and I think the reason it works is because errno is defined as follows in the errno.h of glibc, and we thus treat it as T.

/* The error code set by various library functions.  */
extern int *__errno_location (void) __THROW __attribute_const__;
# define errno (*__errno_location ())

We also have a test of this in 00/12, but thanks for reminding us of this issue. 😄

[brgr]

Ah ok, thanks for the explanation! Then I won't create an issue for that :-)