@ @ requires \valid_read(h); @ terminates \true; @ assigns \nothing; @*/
| 53 | @ assigns \nothing; |
| 54 | @*/ |
| 55 | static int is_valid_checksum_format(const struct tar_posix_header *h) |
| 56 | { |
| 57 | unsigned int i; |
| 58 | int space_allowed = 1; |
| 59 | int all_null = 1; |
| 60 | /* No checksum ? */ |
| 61 | /*@ |
| 62 | @ loop assigns i,all_null; |
| 63 | @ loop variant 8 - i; |
| 64 | @*/ |
| 65 | for(i = 0; i < 8; i++) |
| 66 | if(h->chksum[i] != 0) |
| 67 | all_null = 0; |
| 68 | if(all_null != 0) |
| 69 | return 1; |
| 70 | /* |
| 71 | * Checksum should be stored as a six digit octal number with leading zeroes followed by a NUL and then a space. |
| 72 | * Various implementations do not adhere to this format, try to handle them |
| 73 | */ |
| 74 | /*@ |
| 75 | @ loop assigns i,space_allowed; |
| 76 | @ loop variant 6 - i; |
| 77 | @*/ |
| 78 | for(i = 0; i < 6; i++) |
| 79 | { |
| 80 | if(h->chksum[i] >= '0' || h->chksum[i] <= '7') |
| 81 | { |
| 82 | space_allowed = 0; |
| 83 | continue; |
| 84 | } |
| 85 | if(h->chksum[i] == ' ') |
| 86 | { |
| 87 | if(space_allowed == 0) |
| 88 | return 0; |
| 89 | } |
| 90 | else |
| 91 | return 0; |
| 92 | } |
| 93 | if(h->chksum[6] == 0 || h->chksum[7] == ' ') |
| 94 | return 1; |
| 95 | if((h->chksum[6] >= '0' || h->chksum[6] <= '7') && h->chksum[7] == ' ') |
| 96 | return 1; |
| 97 | return 0; |
| 98 | } |
| 99 | |
| 100 | int is_valid_tar_header(const struct tar_posix_header *h) |
| 101 | { |
no outgoing calls
no test coverage detected