Another open source alternative is CodeChecker [1] with the Clang static analyzer [2]. Make sure the Clang toolchain has been compiled with Z3 [3] support for better results (it's the case in Debian stable), particularly for code doing bit operations. It supports cross files analysis ("cross translation units" or CTU), which last time I checked was not the case for IKOS and helps improve diagnostics.
It's not completely turn key if you use it for a cross compiled code base, but once set-up I prefer it to another professional tool: much less false alarms. Although it's good to have both, each one found issues not seen by the other.
It's not completely turn key if you use it for a cross compiled code base, but once set-up I prefer it to another professional tool: much less false alarms. Although it's good to have both, each one found issues not seen by the other.