-
Notifications
You must be signed in to change notification settings - Fork 87
Unexpected behavior using server-mode in incremental branch #623
Description
In the master branch, reanalysing an unchanged file behaves the same as expected. In the incremental branch, the first analysis works fine, but the second analysis result is different from the first one. For example, analysing the 01-assert.c file, the first run in the incremental gives:
...
[Success][Assert] Assertion "success" will succeed (./src/individual.c:9:3-9:18)
[Error][Assert] Assertion "fail" will fail. (./src/individual.c:10:3-10:15)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (./src/individual.c:11:3-11:23)
[Warning][Assert] Assertion "unknown == 4" is unknown. (./src/individual.c:11:3-11:23)
...
but the second run gives an extra warning in the end:
...
[Warning][Unknown] Calculated state for undefined function: unexpected node Statement assert(silence);
The same happens with file smtprc_comb.c. There the added warnings are:
...
[Warning][Unknown] Calculated state for undefined function: unexpected node Statement return (0);
[Warning][Unknown] Calculated state for undefined function: unexpected node Statement free((void *)buf);
[Warning][Unknown] Calculated state for undefined function: unexpected node Statement return (-1);
This behaviour occurs with server.enabled and server.reparse enabled.
Although this is an obvious unexpected behaviour I do have another question regarding this. The "new warnings" do not have a location. Right now I assume in GobPie that the location is always provided by Goblint. Are the missing locations directly related to this bug or is it possible, that Goblint does not give some information in some chances? The main question is if I should handle the "missing" case for each field or can I continue assuming that all information is always provided?