* filename_convert reads a maximum of n and writes a maximum of n+1 bytes * dst string will be null-terminated */
| 610 | * dst string will be null-terminated |
| 611 | */ |
| 612 | static unsigned int filename_convert(char *dst, const char*src, const unsigned int n) |
| 613 | { |
| 614 | unsigned int i; |
| 615 | /*@ |
| 616 | @ loop assigns i, dst[0 .. i]; |
| 617 | @ loop variant n - i; |
| 618 | @*/ |
| 619 | for(i=0;i<n && src[i]!='\0';i++) |
| 620 | dst[i]=convert_char_dos(src[i]); |
| 621 | /*@ |
| 622 | @ loop variant i; |
| 623 | @*/ |
| 624 | while(i>0 && (dst[i-1]==' '||dst[i-1]=='.')) |
| 625 | i--; |
| 626 | if(i==0 && (dst[i]==' '||dst[i]=='.')) |
| 627 | dst[i++]='_'; |
| 628 | dst[i]='\0'; |
| 629 | return i; |
| 630 | } |
| 631 | #elif defined(__CYGWIN__) || defined(__MINGW32__) |
| 632 | static inline unsigned char convert_char_win(unsigned char car) |
| 633 | { |
no test coverage detected