Kiwamu Okabe

Thanks for your advice. I get success with my desktop PC having 16GB memory without swap. ``` MLton 20130715 (built Fri Dec 23 23:55:28 UTC 2016 on x86-ubc-01) MLton starting...

Also I get success on my notebook having 8GB memory without swap, while any rich application such like `firefox` and `emacs`. I think the building needs 4GB memory, because I...

I think it makes sense.

You can use Infer for Linux kernel with some patches. Please read following: * https://github.com/facebook/infer/pull/1781 * https://gist.github.com/master-q/4b3e09e664a15187290f0f22d1bcb3c6

First step, the output should be split into following: - c2ats_out.sats which includes typedef, macdef, (template) function declaration, #define, staload, %{}. - c2ats_out_tmpl.sats which includes template function definition, staload.

Read carefully following: https://gcc.gnu.org/onlinedocs/cpp/Include-Syntax.html

Need sub-program to seek C language headers and build tree.

http://qiita.com/akachochin/items/71536ca5183b1f7c8db1 Include path can be found at following: ``` $ gcc -Q -v example/hello/example.h --snip-- ignoring nonexistent directory "/usr/local/include/x86_64-linux-gnu" ignoring nonexistent directory "/usr/lib/gcc/x86_64-linux-gnu/6/../../../../x86_64-linux-gnu/include" #include "..." search starts here: #include search...

Header search is ordered. It means at above example, if you do #include .... - First, try to find /usr/lib/gcc/x86_64-linux-gnu/6/include/stdio.h - Next, try /usr/local/include/stdio.h - ... - Finally, try /usr/include/stdio.h

Need to drop unused headers from the tree.