--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on November 2016 ---
On 28/11/16 22:50, Nima Mohammadi wrote: > [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no > preprocessing) > [kernel] Parsing ext2.mod.i (no preprocessing) > ../../include/linux/math64.h:141,0:[kernel] user error: syntax error > [kernel] user error: stopping on file "ext2.mod.i" that has errors. > [kernel] Frama-C aborted: invalid user input. > > I'm not sure what the next step should be. I increased the verbosity of > frama-c, but still didn't get a better description of what had gone > wrong. Any thoughts? On my system, line 141 of /usr/src/linux-headers-4.4.0-45/include/linux/math64.h is: return (u64)(((unsigned __int128)a * mul) >> shift); The syntax error seems to be due to the __int128 type, which is not supported by Frama-C. A few lines above this there is the following guard: #if defined(CONFIG_ARCH_SUPPORTS_INT128) && defined(__SIZEOF_INT128__) and there is an alternative implementation of the operations in question that does not use __int128. See if you can get your Linux configuration to avoid defining this variable, then you should be able to parse the rest of the file. Hope this helps, Gergö