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

src/common.c: add frama-c annotations for MALLOC()

Browse source
This commit is contained in:
Christophe Grenier 2019-10-12 17:01:26 +02:00
parent c315a2a6a7
commit 0004d61672
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/common.c
View file

@ -61,7 +61,7 @@ void *MALLOC(size_t size)
/* Warning, memory leak checker must be posix_memalign/memalign aware, otherwise *
* reports may look strange. Aligned memory is required if the buffer is *
* used for read/write operation with a file opened with O_DIRECT */
#if defined(HAVE_POSIX_MEMALIGN)
#if defined(HAVE_POSIX_MEMALIGN) && !defined(__FRAMAC__)
if(size>=512)
{
if(posix_memalign(&res,4096,size)==0)
@ -70,7 +70,7 @@ void *MALLOC(size_t size)
return res;
}
}
#elif defined(HAVE_MEMALIGN)
#elif defined(HAVE_MEMALIGN) && !defined(__FRAMAC__)
if(size>=512)
{
if((res=memalign(4096, size))!=NULL)

6
src/common.h
View file

@ -438,7 +438,13 @@ struct my_data_struct
uint64_t offset;
};
/*@
@ requires size > 0;
@ ensures \valid(((char *)\result)+(0..size-1));
@ ensures zero_initialization: \subset(((char *)\result)[0..size-1], {0});
@*/
void *MALLOC(size_t size);
unsigned int up2power(const unsigned int number);
void set_part_name(partition_t *partition, const char *src, const unsigned int max_size);
void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size);