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

src/file_txt.c: add a lot of frama-c annotations

Browse source
This commit is contained in:
Christophe Grenier 2019-12-29 17:31:36 +01:00
parent 77850b8710
commit ea04bad2e5
3 changed files with 2545 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2627
src/file_txt.c
View file

File diff suppressed because it is too large Load diff

9
src/file_txt.h
View file

@ -19,5 +19,10 @@
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
int UTF2Lat(unsigned char *buffer_lower, const unsigned char *buffer, const int buf_len);
/*@
@ requires buf_len> 0;
@ requires \valid_read(buffer+(0..buf_len-1));
@ ensures 0 <= \result <= buf_len;
@ assigns \nothing;
@*/
int UTFsize(const unsigned char *buffer, const unsigned int buf_len);

5
src/file_win.c
View file

@ -49,19 +49,16 @@ const file_hint_t file_hint_win= {
static data_check_t data_check_win(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
unsigned int i;
char *buffer_lower=(char *)MALLOC(buffer_size+16);
unsigned int offset=0;
if(file_recovery->calculated_file_size==0)
offset=3;
i=UTF2Lat((unsigned char*)buffer_lower, &buffer[buffer_size/2+offset], buffer_size/2-offset);
i=UTFsize(&buffer[buffer_size/2+offset], buffer_size/2-offset);
if(i<buffer_size/2-offset)
{
if(i>=10)
file_recovery->calculated_file_size=file_recovery->file_size+offset+i;
free(buffer_lower);
return DC_STOP;
}
free(buffer_lower);
file_recovery->calculated_file_size=file_recovery->file_size+(buffer_size/2);
return DC_CONTINUE;
}