Cil generate incorrect casts for code of the form f(i++), where i has type short or char, and f requests an int. See http://bts.frama-c.com/view.php?id=911 for a repro case. I cannot find an online svn to see if the bug is still present, but the fix is simple. In cab2cil.ml, two lines contain (* Should this be t instead ??? *) The variable 't' should be returned there, instead of tresult.