The General Transformation deals with common features of C programs. Currently, we only translate away the arguments of the main function. For example, {{{ ... // declarations int main(int argc, char* argv[]){ ...//main body } ...// other code }}} After General Transformation, the code becomes: {{{ ... // declarations $input int CIVL_argc; $input char CIVL_argv[MAX_ARGC][]; $assume 0 < CIVL_argc && CIVL_argc < MAX_ARGC; void main(){ int argc = CIVL_argc; char* _argv[MAX_ARGC]; char** argv; for(int i = 0; i < MAX_ARGC; i++) _argv[i] = &CIVL_argv[i][0]; argv = &_argv[0]; ... // main body } ...// other code }}}