Thanks for the test case! Of course, the history here is that the Linux kernel doesn't have floats so I never added support for it. I have this friend who is an expert on floats and people consult him when they are designing chips. He was explaining his work to me and I realized that I don't have the foggiest clue how floats work at all... Anyway, I've tried to add floats to Smatch. It turned out not so hard as I imagined, but I know there are places that I missed. Probably it changes from a false positive into a crashing bug now. :/ The fix is almost always going to be to run valgrind to see which function crashes and then add a check: if (type_is_fp(estate_type(state))) return false; Do a pull and take a look. Tell me what you think. I will hack on this tomorrow as well. regards, can carpenter
