--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on January 2014 ---
Hi, I ran the below code, which is a representative of the code snippet in a real code base. frama-c -wp -wp-rte cast.c -wp-proof=z3 Got this "This term has type real but is expected to have type int" float a = 0.0; float b = 1.5; int main() { a = (int)b; return 0; } Looks like type-casting seems to be a problem, but not sure. Any comments? Dharma -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140123/3f48bad3/attachment.html>