@ @ requires buffer_size >= 13; @ requires separation: \separated(&file_hint_mpg, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ terminates \true; @ ensures valid_header_check_result(\result, file_recovery_new); @*/
| 225 | @ ensures valid_header_check_result(\result, file_recovery_new); |
| 226 | @*/ |
| 227 | static int header_check_mpg_Pack(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new) |
| 228 | { |
| 229 | if(is_valid_packet_size(buffer, buffer_size)==0) |
| 230 | return 0; |
| 231 | /* MPEG-1 http://andrewduncan.ws/MPEG/MPEG-1.ps */ |
| 232 | /* pack start code 0x1BA + MPEG-1 + SCR=0 */ |
| 233 | if((buffer[4]&0xF1)==0x21 && (buffer[6]&1)==1 && (buffer[8]&1)==1 && |
| 234 | (buffer[9]&0x80)==0x80 && (buffer[11]&1)==1) |
| 235 | { |
| 236 | if(buffer[5]==0 && buffer[6]==1 && buffer[7]==0 && buffer[8]==1) |
| 237 | { |
| 238 | return header_mpg_found(file_recovery_new); |
| 239 | } |
| 240 | if(file_recovery->file_stat!=NULL && |
| 241 | file_recovery->file_check!=NULL && |
| 242 | file_recovery->file_stat->file_hint==&file_hint_mpg) |
| 243 | { |
| 244 | header_ignored(file_recovery_new); |
| 245 | return 0; |
| 246 | } |
| 247 | return header_mpg_found(file_recovery_new); |
| 248 | } |
| 249 | /* MPEG-2 Program stream http://neuron2.net/library/mpeg2/iso13818-1.pdf */ |
| 250 | /* MPEG2 system header start code, several per file */ |
| 251 | if((buffer[4]&0xc4)==0x44 && (buffer[6]&4)==4 && (buffer[8]&4)==4 && (buffer[9]&1)==1 && (buffer[12]&3)==3) |
| 252 | { |
| 253 | /* |
| 254 | * '01' 2 01 |
| 255 | system_clock_reference_base [32..30] 3 00 0 |
| 256 | marker_bit 1 1 |
| 257 | system_clock_reference_base [29..15] 15 00 buffer[4]=0x44 |
| 258 | 0000 0000 buffer[5]=0x00 |
| 259 | 0000 0 |
| 260 | marker_bit 1 1 |
| 261 | system_clock_reference_base [14..0] 15 00 buffer[6]=0x04 |
| 262 | |
| 263 | 0000 0000 buffer[7]=0x00 |
| 264 | 0000 |
| 265 | 0 |
| 266 | marker_bit 1 1 |
| 267 | system_clock_reference_extension 9 uimsbf |
| 268 | marker_bit 1 |
| 269 | => 0100 0100 |
| 270 | */ |
| 271 | |
| 272 | if(buffer[4]==0x44 && buffer[5]==0 && buffer[6]==4 && buffer[7]==0 && (buffer[8]&0xfc)==4) |
| 273 | { /* SCR=0 */ |
| 274 | return header_mpg_found(file_recovery_new); |
| 275 | } |
| 276 | if(file_recovery->file_stat!=NULL && |
| 277 | file_recovery->file_check!=NULL && |
| 278 | file_recovery->file_stat->file_hint==&file_hint_mpg) |
| 279 | { |
| 280 | header_ignored(file_recovery_new); |
| 281 | return 0; |
| 282 | } |
| 283 | return header_mpg_found(file_recovery_new); |
| 284 | } |
nothing calls this directly
no test coverage detected