We should have a model of syscall in the C library; it might be possible to just call some of the existing models for several entries. See also model-checking/kani#2284.