@ @ requires buffer_size >= 12; @ 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); @*/
| 293 | @ ensures valid_header_check_result(\result, file_recovery_new); |
| 294 | @*/ |
| 295 | static int header_check_mpg_System(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) |
| 296 | { |
| 297 | /* MPEG-1 http://andrewduncan.ws/MPEG/MPEG-1.ps */ |
| 298 | /* ISO/IEC INTERNATIONAL 13818-1 STANDARD |
| 299 | system_header_start_code 32 |
| 300 | header_length 16 |
| 301 | marker_bit 1 |
| 302 | rate_bound 22 |
| 303 | marker_bit 1 |
| 304 | audio_bound 6 |
| 305 | fixed_flag 1 |
| 306 | CSPS_flag 1 |
| 307 | system_audio_lock_flag 1 |
| 308 | system_video_lock_flag 1 |
| 309 | marker_bit 1 |
| 310 | video_bound 5 |
| 311 | packet_rate_restriction_flag 1 |
| 312 | reserved_bits 7 |
| 313 | */ |
| 314 | |
| 315 | /* MPEG-1 system header start code */ |
| 316 | if((buffer[6]&0x80)==0x80 && (buffer[8]&0x01)==0x01 && buffer[11]==0xff) |
| 317 | { |
| 318 | if(is_valid_packet_size(buffer, buffer_size)==0) |
| 319 | return 0; |
| 320 | if(file_recovery->file_stat!=NULL && |
| 321 | file_recovery->file_check!=NULL && |
| 322 | file_recovery->file_stat->file_hint==&file_hint_mpg) |
| 323 | { |
| 324 | header_ignored(file_recovery_new); |
| 325 | return 0; |
| 326 | } |
| 327 | return header_mpg_found(file_recovery_new); |
| 328 | } |
| 329 | return 0; |
| 330 | } |
| 331 | |
| 332 | /*@ |
| 333 | @ requires buffer_size >= 11; |
nothing calls this directly
no test coverage detected