Complexity of programm and Kani limitations

[daschawarde]

Hi, does Kani have any limitations regarding the cyclomatic complexity of the checked program, the level of nesting per function (e.g. nested if/else statements and loops), or the number of parameters passed to a function? Or does it not matter at all, and will Kani work fine with any program, no matter how complex it is or how many nested statements it contains?

[zhassan-aws]

Hi @daschawarde. Yes, the larger the program is and/or the more complex it is, the less the likelihood Kani will be able to handle it. For such cases, stubbing could help overcome the complexity. Please refer to these sections of the documentation for more details:

https://model-checking.github.io/kani/tutorial-real-code.html
https://model-checking.github.io/kani/reference/experimental/stubbing.html
https://model-checking.github.io/kani/reference/experimental/contracts.html

[daschawarde]

Thank you for the answer!