summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-12 19:21:56 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-12 19:21:56 +0100
commit26c361bac08b0d69a247f01662014057e8ba52b1 (patch)
tree1d26d4db3a0d40c5b926189b6ed864b1b13f19fa
parentac95883e2216cae52285b72dbdda9d443f9894ea (diff)
Drop "-wp-depth" from Makefile.am as it has been removed in frama-c 20.0
Update annotations for frama-c 20.0
-rw-r--r--Makefile.am2
-rw-r--r--src/file_jpg.c28
-rw-r--r--src/file_mp3.c21
3 files changed, 30 insertions, 21 deletions
diff --git a/Makefile.am b/Makefile.am
index 7b424bf..441d27e 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -14,7 +14,7 @@ FRAMA_C_FLAGS=-machdep x86_64 \
-then \
-wp \
-wp-dynamic \
- -wp-steps 100000 -wp-depth 100000 \
+ -wp-steps 100000 \
-wp-split -wp-literals \
-wp-timeout 20 -pp-annot \
-kernel-msg-key pp
diff --git a/src/file_jpg.c b/src/file_jpg.c
index f448773..997e855 100644
--- a/src/file_jpg.c
+++ b/src/file_jpg.c
@@ -1401,6 +1401,7 @@ static void jpg_check_picture(file_recovery_t *file_recovery)
/*@
@ requires i < buffer_size;
@ requires \valid_read(buffer+(0..buffer_size-1));
+ @ assigns \nothing;
@*/
static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i, const unsigned int size)
{
@@ -1409,6 +1410,7 @@ static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_
/* DHT should not be longer than 1088 bytes, 4*(1+16+255) */
if(size<18)
return 2;
+ /*@ loop assigns j; */
while(j < buffer_size && j < i+size)
{
const unsigned int tc=buffer[j]>>4;
@@ -1422,6 +1424,12 @@ static int jpg_check_dht(const unsigned char *buffer, const unsigned int buffer_
if(n > 3)
return 2;
j++;
+ /*@
+ @ loop invariant 0 <= l <= 16;
+ @ loop invariant sum <= l*255;
+ @ loop assigns l,sum;
+ @ loop variant 16-l;
+ @*/
for(l=0; l < 16; l++)
if(j+l < buffer_size)
sum+=buffer[j+l];
@@ -1486,43 +1494,46 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
FILE* infile=file_recovery->handle;
unsigned char buffer[40*8192];
size_t nbytes;
- uint64_t offset_test=file_recovery->offset_error;
+ const uint64_t offset_error=file_recovery->offset_error;
+ uint64_t offset_test=offset_error;
uint64_t offset;
- /*@ assert offset_test == file_recovery->offset_error; */
+ /*@ assert offset_test == offset_error; */
if(file_recovery->blocksize==0)
return ;
offset=offset_test / file_recovery->blocksize * file_recovery->blocksize;
if(my_fseek(infile, offset, SEEK_SET) < 0)
return ;
- /*@ assert offset_test == file_recovery->offset_error; */
+ /*@ assert offset_test == offset_error; */
/*@
- @ loop invariant offset_test >= file_recovery->offset_error;
+ @ loop invariant offset_test >= offset_error;
@*/
while((nbytes=fread(&buffer, 1, sizeof(buffer), infile))>0)
{
unsigned int i;
/*@ assert 0 < nbytes <= sizeof(buffer); */
- /*@ assert offset_test >= file_recovery->offset_error; */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&buffer, sizeof(buffer));
if(offset_test > 0x80000000)
return ;
#endif
+ /*@ assert offset_test >= offset_error; */
offset=offset_test / file_recovery->blocksize * file_recovery->blocksize;
i=offset_test % file_recovery->blocksize;
/*@ assert offset + i == offset_test; */
/*@ assert i == offset_test - offset; */
- /*@ assert offset_test >= file_recovery->offset_error; */
+ /*@ assert offset_test >= offset_error; */
/*@
@ loop invariant offset + i >= offset_test;
- @ loop invariant offset_test >= file_recovery->offset_error;
+ @ loop invariant offset_test >= offset_error;
@ loop invariant 0 <= i < nbytes + file_recovery->blocksize;
@ loop assigns i,file_recovery->extra;
@*/
while(i+1<nbytes)
{
const uint64_t tmp=offset + i;
+ /*@ assert tmp == offset + i; */
/*@ assert tmp >= offset_test; */
+ /*@ assert offset_test >= offset_error; */
if(buffer[i]==0xff &&
(buffer[i+1]==0xd8 || /* SOI */
buffer[i+1]==0xdb || /* DQT */
@@ -1533,7 +1544,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
buffer[i+1]==0xfe) /* COM */
)
{
- file_recovery->extra=tmp - file_recovery->offset_error;
+ file_recovery->extra=tmp - offset_error;
#ifndef __FRAMAC__
if(file_recovery->extra % file_recovery->blocksize != 0)
{
@@ -2036,6 +2047,7 @@ data_check_t data_check_jpg(const unsigned char *buffer, const unsigned int buff
if( i + size <= buffer_size)
{
/*@ assert i + size <= buffer_size; */
+ /*@ assert size <= buffer_size - i; */
if(size >= 16)
{
/*@ assert 16 <= size; */
diff --git a/src/file_mp3.c b/src/file_mp3.c
index f264390..468a40d 100644
--- a/src/file_mp3.c
+++ b/src/file_mp3.c
@@ -299,19 +299,15 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
const unsigned int bit_rate_key =(buffer[i+2]>>4)&0x0F;
const unsigned int sampling_rate_key=(buffer[i+2]>>2)&0x03;
const unsigned int padding =(buffer[i+2]>>1)&0x01;
- const unsigned int bit_rate =bit_rate_table[mpeg_version][mpeg_layer][bit_rate_key];
+ /*@ split mpeg_version; */
const unsigned int sample_rate =sample_rate_table[mpeg_version][sampling_rate_key];
+ /*@ assert sample_rate == 0 || 8000 <= sample_rate <= 48000; */
+ const unsigned int bit_rate =bit_rate_table[mpeg_version][mpeg_layer][bit_rate_key];
unsigned int frameLengthInBytes=0;
- /*
- log_info("frame_offset=%u\n",i);
- log_info("bit_rate=%u\n",bit_rate);
- log_info("sample_rate=%u\n",sample_rate);
- log_info("frameLengthInBytes=%u\n",frameLengthInBytes);
- */
if(sample_rate==0 || bit_rate==0 || mpeg_layer==MPEG_L1)
return DC_STOP;
- /*@ assert 8 <= bit_rate <= 448; */
/*@ assert 8000 <= sample_rate <= 48000; */
+ /*@ assert 0 < bit_rate <= 448; */
if(mpeg_layer==MPEG_L3)
{
if(mpeg_version==MPEG_V1)
@@ -325,7 +321,7 @@ static data_check_t data_check_mp3(const unsigned char *buffer, const unsigned i
frameLengthInBytes = (12000 * bit_rate / sample_rate + padding)*4;
if(frameLengthInBytes<3)
return DC_STOP;
- /*@ assert 3 < frameLengthInBytes <= 8065; */
+ /*@ assert 3 <= frameLengthInBytes <= 8065; */
file_recovery->calculated_file_size+=frameLengthInBytes;
/*@ assert file_recovery->calculated_file_size > 0; */
}
@@ -555,13 +551,14 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
const unsigned int bit_rate_key =(buffer[potential_frame_offset+2]>>4)&0x0F;
const unsigned int sampling_rate_key=(buffer[potential_frame_offset+2]>>2)&0x03;
const unsigned int padding =(buffer[potential_frame_offset+2]>>1)&0x01;
+ /*@ split mpeg_version; */
const unsigned int bit_rate =bit_rate_table[mpeg_version][mpeg_layer][bit_rate_key];
const unsigned int sample_rate =sample_rate_table[mpeg_version][sampling_rate_key];
unsigned int frameLengthInBytes=0;
if(sample_rate==0 || bit_rate==0 || mpeg_layer==MPEG_L1)
return 0;
- /*@ assert 8 <= bit_rate <= 448; */
/*@ assert 8000 <= sample_rate <= 48000; */
+ /*@ assert 0 < bit_rate <= 448; */
if(mpeg_layer==MPEG_L3)
{
if(mpeg_version==MPEG_V1)
@@ -577,9 +574,9 @@ static int header_check_mp3(const unsigned char *buffer, const unsigned int buff
log_info("framesize: %u, layer: %u, bitrate: %u, padding: %u\n",
frameLengthInBytes, 4-mpeg_layer, bit_rate, padding);
#endif
- if(frameLengthInBytes==0)
+ if(frameLengthInBytes<3)
return 0;
- /*@ assert 0 < frameLengthInBytes <= 8065; */
+ /*@ assert 3 <= frameLengthInBytes <= 8065; */
potential_frame_offset+=frameLengthInBytes;
/*@ assert potential_frame_offset > 0; */
nbr++;