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
Last modified
12 years ago
Last modified on 07/14/14 13:51:39
Note:
See TracWiki
for help on using the wiki.
