Open stilscher opened 2 years ago
bear: 3.0.8 (compiledb throws errors about not being able to create the already existing directory
.deps
and not being able to regenerate the Makefile. A workaround for this seems to be the removal of the.deps
... and Makefile targets from the Makefile before runningcompiledb make
)
This sounds like the project itself wants to use -MD
to generate additional Makefiles on the go, but the current include dependency gathering mechanism in Goblint also tries to use the same mechanism, which can break both Goblint and the project's build process. I think it's inevitable that we need to gather the includes via CIL.
I think it's inevitable that we need to gather the includes via CIL.
I've been planning on getting started with that, but spent today almost only teaching. I'll hopefully get around to it tomorrow :smile:
Well, this is fabulous, Goblint's analysis of chrony is also unsound. @vesalvojdani
There's also a function end_resolving
, which accesses the same inst
struct and its fields, but none of those accesses show with allglobs
because the entire function is simply dead.
EDIT: Based on a quick look, this again seems to because the project uses malloc wrappers (memory.c
), but Goblint conf doesn't declare them, so all allocated data is joined together into a supertop.
Just adding malloc wrappers isn't enough to fix the issue though, because chrony uses its own dynamic array implementation in array.c
, which itself requires Goblint to properly handle realloc
(https://github.com/goblint/analyzer/issues/701) and memcpy
such that the array contents don't immediately get invalidated to oblivion.
That unsoundness looks fixed by https://github.com/goblint/analyzer/pull/712. Then 8 races are reported, all of which seem to be exclude-able using https://github.com/goblint/analyzer/pull/695 and https://github.com/goblint/analyzer/pull/707.
There would still be unsoundness due to https://github.com/goblint/analyzer/issues/716.
I cannot get this to run on the current Goblint Master Branch. This is my setup. To reproduce simple cherry pick this commit onto the master branch.
The analysis fails with Fatal error: exception Invalid_argument("Cilfacade.get_ikind: non-integer type double ")
for me.
Probably due to https://github.com/goblint/analyzer/commit/2bfadcda082e653fa314d79d88d8d7449353fc38. Might be good to identify where the call comes from, one suspect is e.g. comparisons of floats.
I am not really interested in the analysis result but rather in the performance. Can I somehow deactivate this exception without breaking everything? It doesn't matter if the analysis result is wrong afterwards.
You could locally change cilfacade.ml
to the old behavior, i.e., warn and return IInt
.
I am not really interested in the analysis result but rather in the performance. Can I somehow deactivate this exception without breaking everything? It doesn't matter if the analysis result is wrong afterwards.
https://theprofoundprogrammer.com/post/28974600028/text-it-doesnt-work-but-its-fast — the correctness of the analysis result does matter for performance, because it's easy to make things faster by breaking them.
It's good to have this regression come out though, because we'll need to fix it if there's going to be an interactive paper artifact that uses chrony.
#define NTP_ERA_SPLIT
seems to be randomly changing between different runs of Goblint. I did not have time to investigate this. However, when inspecting the incremental results you will find UTI_Int64ToTimeval
and UTI_IsTimeOffsetSane
and do_time_checks
changed, because they reference NTP_ERA_SPLIT.
I am getting a ton of Fixpoint not reached errors when analyzing chrony with the default analysis configuration (ana.activated not set). However the analysis works with only base and mallocWrapper set. What could be the reason for this? Logfile
These seem to be somehow related to anonymous structs and unions for which CIL generates fresh names containing some numbers. The errors don't look exactly like these, but it could be related to https://github.com/goblint/analyzer/issues/678.
It might also be due to some difference between Goblint's master and interactive branches, because we used the latter for some evaluation and AFAIK didn't get fixpoint errors at the time.
Which analysis do I have to disable to circumvent this error?
I tried to run Goblint on this repository that is also in frama-c's case study benchmarks (#4).
chrony: https://chrony.tuxfamily.org/ at
a2d1569455aa10a273e41eba5f79ca6210934d68
goblint: at goblint/analyzer@5ecb6c50e4a341b7cd0e2fd605d5e6650c8202d6 with https://github.com/goblint/analyzer/pull/585 bear: 3.0.8 (compiledb throws errors about not being able to create the already existing directory.deps
and not being able to regenerate the Makefile. A workaround for this seems to be the removal of the.deps
... and Makefile targets from the Makefile before runningcompiledb make
)run in chrony:
./configure && bear -- make chronyd
(alternatively one can also choose to usechronyc
) or when using compiledb:then run the analysis with:
output for the analysis of
chronyd
: