Parsing error, understanding race warnings #1564
Comments
|
Then I installed it again from master (not from the release) and I don't get the parsing error, butI get the following error: Before that there a bunch of warnings, if that helps (these are only the last few before the error): |
|
The initial parsing error seems to be something we fixed in CIL since our latest release: goblint/cil#172. That's why it no longer appears on master. The library function exception is easier to debug on the branch of unmerged PR #1560. On that branch, running Goblint with Somehow the compilation database only contains one file, but the GCC warnings (which I haven't seen before) suggest that the project consists of more than one C source file. If Goblint is given only some files and they call a function whose definition is missing, then it expects that to come from some standard library. But maybe that function has the name of a standard function (e.g. |
|
I did create a database of the whole code with bear. Above, I wanted to show a smaller fraction of the compile code rather the whole thing that was overwhelming. In both cases, I was getting the same error. I compiled from PR #1560 and I am running it now. I get output like the following. Do these memory statics mean that it's swapping, because it's taking a while. |
I see. Soundly analyzing incomplete programs is difficult though. For example, if a function is called whose body is unknown, it may do absolutely everything (including modifying all global variables arbitrarily). Goblint does support that (when the missing function's name doesn't match a standard library one, causing the crash you saw), but the resulting analysis is likely to be very imprecise as a result.
These messages every 10 seconds simply indicate that the analysis is still running. It's unlikely to be swapping in this case: the maximum memory usage is under 2GB. You could try the large-program configuration as suggested here: https://goblint.readthedocs.io/en/latest/user-guide/configuring/. Alternatively, you could try something similar to your earlier attempt, but instead of excluding some files altogether, comment out calls to some (possibly large) parts of the program that you believe are irrelevant to what you're interested in. But of course that won't be sound w.r.t. to the entire program either. |
|
logPrint is called way too many times. Does goblint have a way to ask it to ignore it? The previous output was on an Ubuntu VM. Actually, if I let it run it goes for 15-20 minutes, and the gets killed. I incrased the VM memory and CPUs to see if that helps. Now I set it up on Mac as well, and know I see the syntax error. This doesn't come up on Linux. There are some changes in the compilation between Linux and MacOS. |
|
After increasing the VM memory it finished the analysis in 2460 seconds. |
|
Is there an introductory documentation on how to interpret the results? Are there specific keywords I should search for in the output? Also, how about false positives and false negatives? What should I expect? |
Just wondering: is this with the default configuration on the entire project or did you need to do some simplifications (large-program configuration/excluding some code) to get to that?
We don't really have such documentation. If you ran in verbose mode (
Goblint intends to be sound, so there should be no false negatives (up to implementation errors in Goblint). If a problem can appear in real execution, then there should be a Goblint warning about it. |
|
I used the large program simplification as you suggested, and also let it run with the default configuration. I think the running time is acceptable for what I do. For example, I get the following output I was mostly interested in detecting any race condition with goblint. By the way, is there a configuration file that I can use that filters only race conditions? A couple of questions:
and line 57 is To you give you some background, newSb is allocated by the main thread and holds the data needed by the watchdogFileThread thread which is also launched by the main thread. Then in watchdogFileThread newSb is free'ed. I have executed the program with address and thread sanitization, as well as valgring for with memcheck and helgrind. I haven't seen this issue popping up. I am trying to understand if this is a valid race condition issue or a false positive. |
|
The "conf." stands for "confidence", but it can practically be ignored. It's more of a historical thing that roughly tried to convey, how directly (or indirectly through pointers) the access happens. The race warning should be interpreted as follows. The race is on a pseudo-variable This perhaps isn't the usual kind of race one is looking for, so it can be disabled using There are options to hide various warnings, e.g. |
|
Got it. Thanks. |
I am getting the following parsing error. Below is my configuration.
Any idea what might be going on?
This is installed on ubuntu 22.04
My setup
The text was updated successfully, but these errors were encountered: