Limitations

These are some of the main limitations of the tool:

• No support for floating point operations.

• Very little support for non-linear reasoning. Most Crab numerical domains reason about linear arithmetic. The term-int domain is an exception. This domain can treat non-linear arithmetic expressions as uninterpreted functions.

• Most Crab numerical domains reason about mathematical integers. The w-int domain is an exception because it can reason about machine arithmetic. The zones domain can use machine arithmetic but it is not enabled by default.

• There are several Crab numerical domains that compute some form of disjunctive invariants (e.g., boxes or dis-int) but they are still limited in terms of expressiveness to keep them tractable.

• The backward analysis is too experimental and it requires more work.

• Reasoning about memory relies heavily on sea-dsa which is context- and field-sensitive pointer analysis but flow-insensitive.