@ @ requires valid_string(fn); @*/
| 535 | @ requires valid_string(fn); |
| 536 | @*/ |
| 537 | static void strip_fn(char *fn) |
| 538 | { |
| 539 | unsigned int i; |
| 540 | /*@ |
| 541 | @ loop assigns i; |
| 542 | @*/ |
| 543 | for(i=0;fn[i]!='\0';i++); |
| 544 | /*@ |
| 545 | @ loop assigns i; |
| 546 | @ loop invariant i; |
| 547 | @*/ |
| 548 | while(i>0 && (fn[i-1]==' '||fn[i-1]=='.')) |
| 549 | i--; |
| 550 | if(i==0 && (fn[i]==' '||fn[i]=='.')) |
| 551 | fn[i++]='_'; |
| 552 | fn[i]='\0'; |
| 553 | } |
| 554 | |
| 555 | #ifdef DJGPP |
| 556 | static inline unsigned char convert_char_dos(unsigned char car) |