search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Support `imaxabs` for SV-COMP #1519

Open sim642 opened 1 week ago

sim642 commented 1 week ago

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 #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 #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.

TODO