Function header_ignored

src/filegen.c:1038–1048

@ @ requires \separated(file_recovery_new, &offset_skipped_header); @ assigns offset_skipped_header; @*/

  @ assigns offset_skipped_header;
  @*/
void header_ignored(const file_recovery_t *file_recovery_new)
{
  if(file_recovery_new==NULL)
  {
    offset_skipped_header=0;
    return ;
  }
  /*@ assert \valid_read(file_recovery_new); */
  if(file_recovery_new->location.start < offset_skipped_header || offset_skipped_header==0)
    offset_skipped_header=file_recovery_new->location.start;
}

/*@
  @ requires \separated(list_search_space, current_search_space, offset, &gpls_nbr, &offset_skipped_header);