src/filegen.c: fix error reported by frama-c in file_check_cmp()

This commit is contained in:
Christophe Grenier 2021-01-29 22:42:05 +01:00
parent 590cf7dab3
commit 0c59aa8d22

View file

@ -80,7 +80,7 @@ int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
if(fc_a->length!=0 && fc_b->length==0) if(fc_a->length!=0 && fc_b->length==0)
return 1; return 1;
/*@ assert (fc_a->length > 0 && fc_b->length > 0) || (fc_a->length == 0 && fc_b->length == 0) ; */ /*@ assert (fc_a->length > 0 && fc_b->length > 0) || (fc_a->length == 0 && fc_b->length == 0) ; */
res=fc_a->offset-fc_b->offset; res=(int)fc_a->offset-(int)fc_b->offset;
if(res!=0) if(res!=0)
return res; return res;
/*@ assert fc_a->offset == fc_b->offset; */ /*@ assert fc_a->offset == fc_b->offset; */