search

goblint / cil

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

Option to silence `treating long double constant [...] as double constant at [...] (only relevant if first argument of CReal is used)` #136

Closed michael-schwarz closed 11 months ago

michael-schwarz commented 1 year ago

Some tools (e.g. Goblint) take care to not access the first component of CReal as OCaml floats can not accurately represent such large constants.

There should be an option to silence these warnings for tools that are aware of this pitfall to avoid polluting logs.

sim642 commented 11 months ago

Some tools (e.g. Goblint) take care to not access the first component of CReal as OCaml floats can not accurately represent such large constants.

That's not true since the addition of float domains though: https://github.com/goblint/analyzer/blob/15e6c3d636bde630a5df20d31af2c812355b68a2/src/analyses/base.ml#L764

michael-schwarz commented 11 months ago

That's not true since the addition of float domains though

Ah, that is an oversight on the Goblint side then, we should not encounter CReal that do not have a string representation there. In a separate PR to bump Goblint's dependency, I will switch that code path in Goblint to create a top value of the appropriate type to be on the safe side.

sim642 commented 11 months ago

If it should never happen, then maybe it can even be assert false to indicate intended unreachability? If that ever breaks, then CIL creates CReals without string representations when it shouldn't.

michael-schwarz commented 11 months ago

If it should never happen, then maybe it can even be assert false to indicate intended unreachability?

It is not impossible on the CIL side, as one could easily define some such value using the API, but parsing programs should not yield such values.

Asserting false would break existing usages of CIL, if we were open to that, one could just remove the float part of CReal entirely, but I want to take a more gentle approach here to not unnecessarily break compatibility even more.

We could add an assert false on the Goblint side of things, instead of going to top?

sim642 commented 11 months ago

We could add an assert false on the Goblint side of things, instead of going to top?

Yes, that's what I meant. Sorry for not being clear about it.