Limitation
==========

Python Syntax
-------------

**Loop** in general is not supported due to complex data flow analysis needed. It could be supported in the future
after I have some sort of idea how people are doing it. Loop includes ``For``, ``While`` and  ``recursive call``

**Import** is not supported yet, though it's likely to be supported in the future since it's not that difficult.

All comprehensions are not supported.

Python data structure (list, set, tuple, dict) is supported in inference system, but it's not supported
when it's used as a constraint, e.g. checking ``len()`` or testing membership.

**Exceptions** is not supported now and will simply get ignored. In the future, Klara will be able to generate
inputs to trigger exceptions, with contract support.

Uninferable
-----------

If the return value doesn't understand by Klara (e.g. multiply a list with z3 variable, which is possible
in python context, but invalid in Z3 context), it will yield a special node called uninferable. Even though
the value can't be determined, but it will still contain bound conditions. Consider following::

    def foo(v1: int):
        return 3 if v1 > 2 else xxx

The function can return the number 3, or the invalid variable ``xxx``. Even though we can't determine
the value of ``xxx``, it will still contain the bound: ``not(v1 > 2)``, so Klara still be able to generate
2 test cases for this function, using ``is not None`` as test.::

    def test_foo_0():
        assert foo(3) == 3
        assert foo(0) is not None


There will be a lot of undocumented cases of uninferable that doesn't contain the expected bound. One example
is where binary operation with list, the bound for the element of the list will not include in the uninferable
result. E.g.::

    def foo(v1: int, v2: int):
        a = 1 if v1 > 3 else 2
        b = 3 if v2 > 3 else 4
        return [a, b] * xxx

Because ``[a, b] * v1`` will be uninferable since `xxx` is undefined, this test case
will not yield any test inputs, even though the list: ``[a, b]`` will have 4 combinations in total. This
is because the ``xxx`` of binop: ``[a, b] * xxx`` is uninferable, the left hand side operand will not
get expanded.