Simmo Saan

> ExpRelation is crucial to the partitioned array domains working I'm not sure how crucial it really is though. In https://github.com/goblint/analyzer/pull/770/commits/16c70bcc8d4846352d54e06395ee275892b23402 I managed to remove most of these cases without...

`--set pre.cppflags[+] -D__LINE__=0` works (and similarly for others, e.g. `__FILE__`) and just makes the preprocessor whine a bit. Not sure if there's any better solution. EDIT: We could also supply...

The standard might not like that though: > Attempts to redefine or undefine these macros result in undefined behavior. (https://en.cppreference.com/w/c/preprocessor/replace)

> We were thinking about some less brutal options, such as silently patching constant int arguments to functions that do not have a body, and for which we do not...

Kind of off-topic, but the code in https://github.com/facebook/zstd/commit/a8adfa7f67840dec0fd94f25eecfb4abda208f23 looks suspiciously weird: ```c if (fileSize == UTIL_FILESIZE_UNKNOWN) EXM_THROW(32, "This file format is not supported : Dictionary file %s\n", fileName); { //...

> Yes, but for functions for which we do not have a body (and which are not `special`, i.e.`malloc` and friends), we don't do anything with constant int arguments, so...

For future reference, Frama-C contains a bunch of machdep definitions for different architectures: https://git.frama-c.com/pub/frama-c/-/blob/master/src/kernel_internals/runtime/machdeps.ml.

On a minimized example in our regression tests, in #716 it turned out that these relational struct domains wouldn't even help, because they are still joined together before evaluating offsets...

Probably needs to be assessed as part of #107.

As discussed in GobCon, the idea of trying to unassume hints only once can be quite problematic and thus will not be added to this. In all the reasonable cases...