Partially support imaxabs for SV-COMP

[sim642]

This extends #1254 to support imaxabs on the intmax_t type, which some Juliet tasks in SV-COMP use.

Changes

Actually verifying those Juliet tasks required a bit more changes:

1. The type (and thus ikind) of intmax_t is looked up from the typedef in the program. So this can bypass make sizes of primitive types configurable with current machine as default #54.
2. ana.float.evaluate_math_functions is enabled in svcomp24 and svcomp confs. We used the C stubs to evaluate sqrt and friends in SV-COMP 2024, but More precise abstractions of trigonometric functions using c-stubs #1277 added this option, which is off by default. So right now we couldn't even solve the similar tasks on smaller types that we could verify at SV-COMP 2024. I don't know if this will be a problem for soundness in SV-COMP. If so, then we'll need some non-stub implementation of floating point sqrt to solve these tasks, of which there is a lot of.
3. Casts around the refinement are somehow different in these tasks, which required handling of float-integer casts in BaseInvariant. I don't know if this is correct because previously only various float-float casts were supported and everything else was considered "incompatible types". It's not clear whether these are supposed to be impossible in the AST according to the standard or just were unsupported in the initial implementation.
4. Casts around the refinement are also different on MacOS. Apparently using typedefs screws up the refinement (Partially support imaxabs for SV-COMP #1519 (comment)). This fixes the problem by unrolling cast types in refinement.

TODO

• Fix MacOS.

[sim642]

I reverted the questionable cast refinement, but MacOS CI doesn't pass still. Apparently there are CIL differences even on the non-sqrt case.

Ubuntu:

#line 9
    tmp = imaxabs(data);
#line 9
    if (tmp < 100L) {
#line 11
      __goblint_check(data < 100L);
#line 12
      __goblint_check(-100L < data);
#line 13
      result = data * data;
    }

MacOS:

#line 9
    tmp = imaxabs((intmax_t )data);
#line 9
    if (tmp < (intmax_t __attribute__((__availability__(macosx,introduced=10.4)))  )100) {
#line 11
      __goblint_check(data < 100LL);
#line 12
      __goblint_check(-100LL < data);
#line 13
      result = data * data;
    }

I guess this has something to do with the following type definitions.
Ubuntu:

typedef long __int64_t;
typedef __int64_t int64_t;
typedef long __intmax_t;
typedef __intmax_t intmax_t;

MacOS:

typedef long long int64_t;
typedef long intmax_t;

Both are 64bit, so long and long long are the same size, but they're technically different types with different ikinds.
This is a particularly silly reason to give up on refinement. I'm surprised this hasn't come up before.
EDIT: Turns out we weren't unrolling cast types in refinement...