[python-frontend] Add support for non-determinism

[brcfarias]

This PR:

• Adds support for nondet_X() functions
• Adds regression test for non-determinism

[lucasccordeiro]

Can you please add some regression tests with __VERIFIER_nondet_X()? See the definition here: https://sv-comp.sosy-lab.org/2023/rules.php

In particular, try to add some regression tests that fail too.

[lucasccordeiro]

I agree with @fbrausse.

Please check these definitions:

https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/clang_c_language.cpp#L431

https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/clang_c_language.cpp#L445

We should match them.

[lucasccordeiro]

Excellent!

Many thanks for addressing our comments, @brcfarias.

[fbrausse]

LGTM. One nitpick: The test whether the underscore was found could be removed (or become an assertion).