1919 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
2020
2121 */
22-
2322#if !defined(SINGLE_FORMAT ) || defined(SINGLE_FORMAT_hdf5 )
2423#ifdef HAVE_CONFIG_H
2524#include <config.h>
@@ -62,72 +61,6 @@ struct hdf5_superblock
6261 uint8_t lengths_size ;
6362} __attribute__ ((gcc_struct , __packed__ ));
6463
65- /*@
66- @ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source, &__fc_heap_status);
67- @ requires valid_file_check_param(file_recovery);
68- @ ensures valid_file_check_result(file_recovery);
69- @*/
70- static void file_check_hdf5_0 (file_recovery_t * file_recovery )
71- {
72- const uint8_t eof_address_offset = 0x18 + 2 * 8 ;
73- FILE * handle = file_recovery -> handle ;
74- uint64_t eof_address = 0 ;
75- /* Get EOF Address */
76- if (my_fseek (handle , eof_address_offset , SEEK_SET ) < 0 ||
77- fread (& eof_address , sizeof (eof_address ), 1 , handle ) != 1 )
78- {
79- #ifdef DEBUG_HDF5
80- log_error ("file_check_hdf5_0: Couldn't read HDF End of File Address" );
81- #endif
82- file_recovery -> file_size = 0 ;
83- return ;
84- }
85- eof_address = le64 (eof_address );
86- #ifdef DEBUG_HDF5
87- log_info ("file_check_hdf5_0: dec eof_address = %lu\n" , (long unsigned )eof_address );
88- log_info ("file_check_hdf5_0: hex eof_address = 0x%02lX\n" , eof_address );
89- #endif
90- if (eof_address < eof_address_offset || eof_address < file_recovery -> file_size )
91- {
92- file_recovery -> file_size = 0 ;
93- return ;
94- }
95- file_recovery -> file_size = eof_address ;
96- }
97-
98- /*@
99- @ requires \separated(file_recovery, file_recovery->handle, &errno, &Frama_C_entropy_source, &__fc_heap_status);
100- @ requires valid_file_check_param(file_recovery);
101- @ ensures valid_file_check_result(file_recovery);
102- @*/
103- static void file_check_hdf5_1 (file_recovery_t * file_recovery )
104- {
105- const uint8_t eof_address_offset = 0x1C + 2 * 0x8 ;
106- FILE * handle = file_recovery -> handle ;
107- uint64_t eof_address = 0 ;
108- /* Get EOF Address */
109- if (my_fseek (handle , eof_address_offset , SEEK_SET ) < 0 ||
110- fread (& eof_address , sizeof (eof_address ), 1 , handle ) != 1 )
111- {
112- #ifdef DEBUG_HDF5
113- log_error ("file_check_hdf5_1: Couldn't read HDF End of File Address" );
114- #endif
115- file_recovery -> file_size = 0 ;
116- return ;
117- }
118- eof_address = le64 (eof_address );
119- #ifdef DEBUG_HDF5
120- log_info ("file_check_hdf5_1: dec eof_address = %lu\n" , (long unsigned )eof_address );
121- log_info ("file_check_hdf5_1: hex eof_address = 0x%02lX\n" , eof_address );
122- #endif
123- if (eof_address < eof_address_offset || eof_address < file_recovery -> file_size )
124- {
125- file_recovery -> file_size = 0 ;
126- return ;
127- }
128- file_recovery -> file_size = eof_address ;
129- }
130-
13164/*@
13265 @ requires buffer_size >= sizeof(struct hdf5_superblock);
13366 @ requires separation: \separated(&file_hint_hdf5, buffer+(..), file_recovery, file_recovery_new);
@@ -141,15 +74,30 @@ static int header_check_hdf5(const unsigned char *buffer, const unsigned int buf
14174 /*@ assert \valid_read(sb); */
14275 if (sb -> version > 2 )
14376 return 0 ;
77+ if (sb -> offsets_size < 1 )
78+ return 0 ;
79+ if (sb -> offsets_size == 8 )
80+ {
81+ uint64_t calculated_file_size ;
82+ /* Currently only handle 64-bits offsets */
83+ if (sb -> version == 0 )
84+ calculated_file_size = le64 (* (const uint64_t * )(& buffer [0x18 + 2 * 8 ]));
85+ else
86+ calculated_file_size = le64 (* (const uint64_t * )(& buffer [0x1C + 2 * 8 ]));
87+ if (calculated_file_size < 0x1C + 3 * 8 )
88+ return 0 ;
89+ reset_file_recovery (file_recovery_new );
90+ file_recovery_new -> extension = file_hint_hdf5 .extension ;
91+ file_recovery_new -> calculated_file_size = calculated_file_size ;
92+ #ifdef DEBUG_HDF5
93+ log_info ("calculated_file_size %llu\n" , (long long unsigned )calculated_file_size );
94+ #endif
95+ file_recovery_new -> data_check = & data_check_size ;
96+ file_recovery_new -> file_check = & file_check_size ;
97+ return 1 ;
98+ }
14499 reset_file_recovery (file_recovery_new );
145100 file_recovery_new -> extension = file_hint_hdf5 .extension ;
146- if (sb -> offsets_size != 8 )
147- return 1 ;
148- /* Currently only handle 64-bits offsets */
149- if (sb -> version == 0 )
150- file_recovery_new -> file_check = & file_check_hdf5_0 ;
151- else
152- file_recovery_new -> file_check = & file_check_hdf5_1 ;
153101 return 1 ;
154102}
155103
0 commit comments