search

goblint / cil

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

Remove unused `Libmaincil` module #165

Closed sim642 closed 9 months ago

sim642 commented 9 months ago

It calls initCIL at top level when linked with -linkall. This is unexpected, because in Goblint we explicitly call initCIL, but that's actually no-op and wouldn't account for runtime changes to Machdep and whatever else mutable initCIL reads.

This indirectly causes https://github.com/goblint/gobview/issues/38. In non-dev dune profile, jsoo now runs global dead code detection which is more aggressive than what the native compiler can on a per-module basis.

The goal here is to remove this unnecessary module from CIL and fix Goblint to not read what initCIL writes in top-level expressions. I'll open a follow-up Goblint PR for that.

michael-schwarz commented 9 months ago

It indeed appears unused, so we can remove it.

However, I agree with @stilscher that the root cause for the issue in gobview is probably different: There we have no guarantee all modules have been loaded before the main code of gobview is run. Until we can guarantee that, everything depends on the order in which the compiler (the runtime?) decides to load modules.

sim642 commented 9 months ago

However, I agree with @stilscher that the root cause for the issue in gobview is probably different: There we have no guarantee all modules have been loaded before the main code of gobview is run. Until we can guarantee that, everything depends on the order in which the compiler (the runtime?) decides to load modules.

That's what https://github.com/goblint/gobview/pull/39 does the same way that native Goblint.