Hello Dan, I am an undergraduate student of Dongliang Mu's team. I'm recently working on a project on how to run smatch in all debian C code, but I found that there is little documentation on use smatch on code other than the linux kernel,so I am having trouble with this project. I'd like to ask you what do I need to do to use smatch (simplifying some of the rules is fine) in general C code, and is there documentation that can help?
