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

frama-c: add annotation to fix warnings in date_dos2unix() and __td_list_add()

Browse source
This commit is contained in:
Christophe Grenier 2020-06-21 09:52:09 +02:00
parent 90d21a4d81
commit a705cb1ba7
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/common.c
View file

@ -262,7 +262,10 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
leap_day = (year + 3) / 4;
if (year > YEAR_2100) /* 2100 isn't leap year */
{
/*@ assert year > YEAR_2100 && leap_day > (YEAR_2100 + 3)/4; */
leap_day--;
}
if (IS_LEAP_YEAR(year) && month > 2)
leap_day++;
days = days_in_year[month];

4
src/list.h
View file

@ -78,6 +78,10 @@ static inline void __td_list_add(struct td_list_head *newe,
newe->next = next;
newe->prev = prev;
prev->next = newe;
/*@ assert next->prev == newe; */
/*@ assert newe->next == next; */
/*@ assert newe->prev == prev; */
/*@ assert prev->next == newe; */
}
/**