Problem of the libc functions that don't have symbolic wrapper implementation about symcc

[sebastianpoeplau]

My question is: since we can not implement symbolic wrapper for all of the functions in libc manually, what will happen if we meet strlen during the symbolic execution? I think SymCC won't instrument strlen with symbolic code, so we will lost the constraints inside the strlen.

That's correct: SymCC won't know how the return value of strlen was obtained, and it will therefore treat it as a concrete value.

Not sure whether my understanding is right, what's other side effect (if any) for the libc functions that don't have symbolic wrapper?

In most cases, there are no negative consequences beyond SymCC losing track of symbolic constraints. One exception from this rule is when a libc function changes memory: if the modified memory cell contained symbolic data before the function call, then SymCC won't know that its symbolic expression doesn't correctly describe the new value, which can lead to incorrect (and likely conflicting) path constraints. In such cases, it makes sense to add wrappers for the offending function(s); see #23 (comment) for suggestions how to do so.

[aurelf]

Closing as duplicate of #23