luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Fix "make frama-c-fidentify-rw2"

Browse source
This commit is contained in:
Christophe Grenier 2020-10-11 11:02:09 +02:00
parent 7640708ca8
commit 13cb4c5048
4 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/file_tiff.c
View file

@ -20,7 +20,7 @@
*/
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg)
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@ -184,7 +184,7 @@ static void register_header_check_tiff(file_stat_t *file_stat)
{
static const unsigned char tiff_header_be[4]= { 'M','M',0x00, 0x2a};
static const unsigned char tiff_header_le[4]= { 'I','I',0x2a, 0x00};
#if !defined(SINGLE_FORMAT_jpg)
#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2)
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be, file_stat);
#endif

7
src/file_tiff.h
View file

@ -19,6 +19,8 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#ifndef _FILE_TIFF_H
#define _FILE_TIFF_H
#ifdef __cplusplus
extern "C" {
#endif
@ -105,7 +107,9 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
@ ensures valid_read_string(fr->extension);
@*/
void file_check_tiff_le(file_recovery_t *fr);
#endif
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2)
/*@
@ requires buffer_size > 0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ -150,7 +154,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
#endif
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg)
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2)
/*@
@ requires buffer_size > 0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ -195,3 +199,4 @@ const char *tag_name(unsigned int tag);
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif
#endif

4
src/file_tiff_be.c
View file

@ -20,7 +20,7 @@
*/
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg)
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@ -382,7 +382,7 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
#endif
#endif
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg)
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2)
static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
/*@

4
src/file_tiff_le.c
View file

@ -20,7 +20,7 @@
*/
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg)
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@ -755,7 +755,7 @@ void file_check_tiff_le(file_recovery_t *fr)
}
#endif
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg)
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2)
/*@
@ requires separation: \separated(&file_hint_tiff, buffer+(..), file_recovery, file_recovery_new);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_tiff.extension ||