Thanks for the answers from Shriramana Sharma. Currently I am writing a checker mainly with the following two callbacks:
void checkLocation(SVal loc, bool isLoad, const Stmt* LoadS, CheckerContext &Ctx) const; void checkBind(SVal loc, SVal val,const Stmt *StoreE,CheckerContext &Ctx) const;
And what I intended to do is to mark taints to the memory accessed value from user space and observe the propagation. However, according to your answer previously, taints can only be marked to symbols, but the parameters of these two callbacks are mainly SVals(represent the location and value), which I tried to convert to symbols but failed, I guess it is because they are not symbols. I also tried to add taints to the location( for both SVal and MemRegion), and Value in the location(got by function state->getSVa(loc)), but none of them worked.
Is there any solution that I can get my purpose?? AKA How can I add taints to the value fetched from user memory space? Thank you!