Float domain ill-typed program crash on concrat/Mirai-Source-Code

[sim642]

The following snippet, extracted from concrat/Mirai-Source-Code, crashes Goblint:

// PARAM: --enable ana.float.interval
// Extracted from concrat/Mirai-Source-Code.
extern int ( /* missing proto */  ceil)() ;

int main() {
  int x = ceil(0.5);
  if (x < 5) // TODO NO CRASH: Failure("ill-typed program")
    return 1;
  return 0;
}

The exception is from here: https://github.com/goblint/analyzer/blob/093eb5ef686078baf906cc0d932a6a0c64c24053/src/analyses/baseInvariant.ml#L689-L690 It seems that the result of ceil isn't cast to int, but instead x has an abstract float value.

[michael-schwarz]

This seems like an issue with our library mechanism: The special for ceil is used, which returns a float, which would be correct in case math.h was included.

[sim642]

Not really, the library mechanism doesn't specify any types. It's the missing math.h include that has produced the ceil declaration with default signature in the merged benchmark.

We know perfectly well what type the assigned variable is, so we could just put an abstract cast in there. That would keep abstract values and program variable types in sync, avoiding the mismatch from the exceptional case.