Skip to content

Limitations

caballa edited this page Feb 14, 2021 · 2 revisions

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.

Clone this wiki locally