summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-06-21 09:52:09 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-06-21 09:52:09 +0200
commita705cb1ba79bffce0f180c2f00fa8d664b6d5d7b (patch)
tree9b97f9f6c0101733f5edd5ffe4e204f9551735f8
parent90d21a4d8126553876d324bc0ffa24293e610550 (diff)
frama-c: add annotation to fix warnings in date_dos2unix() and __td_list_add()
-rw-r--r--src/common.c3
-rw-r--r--src/list.h4
2 files changed, 7 insertions, 0 deletions
diff --git a/src/common.c b/src/common.c
index 3e93f19..7b09290 100644
--- a/src/common.c
+++ b/src/common.c
@@ -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];
diff --git a/src/list.h b/src/list.h
index c4fbe67..2abb40a 100644
--- a/src/list.h
+++ b/src/list.h
@@ -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; */
}
/**