wiki:GeneralTransformation

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.