ESBMC-Python-CPP fails for a simple Python program that mixes the data types

[lucasccordeiro]

var = 8
print(var)

var = 3.142
assert var > 0

var = 'Python in easy steps'
assert var == 'Python in easy steps'

example_34_mix_types.cpp:19:11: error: assigning to 'pyobj *' from incompatible type '__ss_float' (aka 'double')
 var = ((__ss_float)(__ss_int(8)));
 ^~~~~~~~~~~~~~~~~~~~~~~~~~~
example_34_mix_types.cpp:21:11: error: assigning to 'pyobj *' from incompatible type '__ss_float' (aka 'double')
 var = __ss_float(3.142);
 ^~~~~~~~~~~~~~~~~
example_34_mix_types.cpp:22:20: error: use of undeclared identifier '__gt'
 ASSERT(___bool(__gt(__example_34_mix_types__::var, ((__ss_float)(__ss_int(0))))), 0);
 ^
ERROR: PARSING ERROR

[sshivaji]

This is a well known issue, we have to define types and not mix them due to implied type inference, this is sort of a feature and not a bug as type inference is preventing verification. I will see what we can do to alert the user Em sáb., 1 de fev. de 2025 07:38, Lucas C. Cordeiro < ***@***.***> escreveu:

…

var = 8print(var) var = 3.142assert var > 0 var = 'Python in easy steps'assert var == 'Python in easy steps' example_34_mix_types.cpp:19:11: error: assigning to 'pyobj *' from incompatible type '__ss_float' (aka 'double') var = ((__ss_float)(__ss_int(8))); ^~~~~~~~~~~~~~~~~~~~~~~~~~~ example_34_mix_types.cpp:21:11: error: assigning to 'pyobj *' from incompatible type '__ss_float' (aka 'double') var = __ss_float(3.142); ^~~~~~~~~~~~~~~~~ example_34_mix_types.cpp:22:20: error: use of undeclared identifier '__gt' ASSERT(___bool(__gt(__example_34_mix_types__::var, ((__ss_float)(__ss_int(0))))), 0); ^ ERROR: PARSING ERROR — Reply to this email directly, view it on GitHub <#14>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAK5IGRNIRKYLIOKWL2KFND2NTS7BAVCNFSM6AAAAABWJMXNT6VHI2DSMVQWIX3LMV43ASLTON2WKOZSHAZDKMRXGQ4TMOA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>