search

goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

Allow parsed location directive transformation #89

Closed sim642 closed 2 years ago

sim642 commented 2 years ago

This adds Errormsg.transformLocation, which Goblint can override to supply a function for transforming the location directives. It allows us to massage paths relative to other directories from compilation databases to make them relative to the analyzed project as a whole. Also it allows ignoring the location directives which could be used to analyze already preprocessed files, which have location directives to some old absolute paths that no longer make sense.

sim642 commented 2 years ago

This would actually allow us to revert #73, because using this transformation hook Goblint could also remember what it transformed on its own. Do we want to revert that or just keep it?

michael-schwarz commented 2 years ago

Do we want to revert that or just keep it?

I'd be in favor of reverting and using this instead. No point in keeping different ways to do the same thing around!

michael-schwarz commented 2 years ago

I think we should investigate the failures on OS X. Especially since for #90 the OS X CI is now also happy.

sim642 commented 2 years ago

I added a step to the CI workflow to upload the cil.log from failed runs, so it's possible to see that from MacOS as well. Apparently all the tests fail with

Error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"dlopen(/Users/runner/work/cil/cil/_opam/lib/batteries/batteries.cmxs, 10): image not found\")")

I guess that's related to having removed the batteries dependency from the CIL library itself, but I'm very confused why it would be needed on MacOS, but not Linux. Also batteries itself does get installed into the opam switch nevertheless, so it's weird that it wouldn't be found there. It's not something in dune's _build.

sim642 commented 2 years ago

I'm just reverting that and hoping it works again. I think it's somehow related to all this dynamic feature library loading, which somehow also depends on what dependencies the CIL library itself has: https://github.com/goblint/cil/blob/e559eada8b29713ae2cf7ef34b288958c305ec20/src/feature.ml#L98-L101 I'm still not sure why it would be any different between Linux vs MacOS, but whatever for now.