wiki:GeneralTransformation

Version 3 (modified by zmanchun, 12 years ago) ( diff )

--

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
Note: See TracWiki for help on using the wiki.