summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-08-22 13:31:37 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-08-22 13:31:37 +0200
commit3443c8df1512c893a066d5a885967fd13af59150 (patch)
tree04dc44a611fe0041cc4738f689cea2af9312066b
parent1e1d6345661c21ff09e1301048d7fce59152e99b (diff)
common.c: add some frama-c annotations in strip_dup(), date_dos2unix()
date_dos2unix() - avoid using localtime_r()
-rw-r--r--src/common.c24
1 files changed, 22 insertions, 2 deletions
diff --git a/src/common.c b/src/common.c
index 04ed1aa..6d78832 100644
--- a/src/common.c
+++ b/src/common.c
@@ -217,9 +217,15 @@ char* strip_dup(char* str)
{
unsigned int i;
char *end;
+ /*@
+ @ loop assigns str;
+ @*/
while(isspace(*str))
str++;
end=str;
+ /*@
+ @ loop assigns i, end;
+ @*/
for (i = 0; str[i] != 0; i++)
if (!isspace (str[i]))
end=&str[i];
@@ -257,17 +263,31 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
unsigned long int day,leap_day,month,year,days;
unsigned long int secs;
year = f_date >> 9;
+ /*@ assert 0 <= year <= 127; */
month = td_max(1, (f_date >> 5) & 0xf);
+ /*@ assert 1 <= month <= 15; */
day = td_max(1, f_date & 0x1f) - 1;
+ /*@ assert 0 <= day <= 30; */
leap_day = (year + 3) / 4;
+ /*@ assert 0 <= leap_day <= 32; */
if (year > YEAR_2100) /* 2100 isn't leap year */
{
- /*@ assert year > YEAR_2100 && leap_day > (YEAR_2100 + 3)/4; */
+ /*@ assert year > YEAR_2100; */
+ leap_day = (year + 3) / 4;
+ /*@ assert (YEAR_2100 + 3)/4 < leap_day <= 32; */
leap_day--;
+ /*@ assert (YEAR_2100 + 3)/4 <= leap_day < 32; */
+ }
+ else
+ {
+ /*@ assert year <= YEAR_2100; */
+ /*@ assert 0 <= leap_day <= (YEAR_2100 + 3)/4; */
}
+ /*@ assert 0 <= leap_day < 32; */
if (IS_LEAP_YEAR(year) && month > 2)
leap_day++;
+ /*@ assert 0 <= leap_day <= 32; */
days = days_in_year[month];
/*@ assert days <= 334; */
days += year * 365 + leap_day + day + DAYS_DELTA;
@@ -283,7 +303,7 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
void set_secwest(void)
{
const time_t t = time(NULL);
-#if defined(__MINGW32__)
+#if defined(__MINGW32__) || defined(__FRAMAC__)
const struct tm *tmptr = localtime(&t);
#else
struct tm tmp;