Well yeah, I assumed if I was doing formal verification that that would necessarily involve fully specifying/tracking data sizes, which would mean that all stri

Well yeah, I assumed if I was doing formal verification that that would necessarily involve fully specifying/tracking data sizes, which would mean that all strings would be pascal strings (at least internally; obviously it might be necessary to tack on a \0 for compatibility with external code).