From 4ef431af99015faaa4077c87f3ec512437b0311e Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Tue, 9 Jun 2020 13:45:41 +0200 Subject: [PATCH] sync with frama-c master --- chrony/chrony-ntp-core.eva/alarms.csv | 12 ++++++------ chrony/chrony-regress.eva/alarms.csv | 6 +++--- frama-c | 2 +- icpc/icpc.eva/alarms.csv | 4 ++-- libmodbus/libmodbus-unit-server.eva/alarms.csv | 2 +- papabench/papabench.eva/alarms.csv | 10 +++++----- 6 files changed, 18 insertions(+), 18 deletions(-) diff --git a/chrony/chrony-ntp-core.eva/alarms.csv b/chrony/chrony-ntp-core.eva/alarms.csv index 7c59f79db..ffd88c82f 100644 --- a/chrony/chrony-ntp-core.eva/alarms.csv +++ b/chrony/chrony-ntp-core.eva/alarms.csv @@ -840,12 +840,12 @@ directory file line function property kind status property . util.c 1213 UTI_GetRandomBytesUrandom precondition of fread Unknown valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1)) FRAMAC_SHARE/libc __fc_inet.h 358 inet_addr precondition Unknown valid_arg: valid_read_string(arg) FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0 -FRAMAC_SHARE/libc math.h 372 exp precondition Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9 -FRAMAC_SHARE/libc math.h 409 log precondition Unknown finite_arg: \is_finite(x) -FRAMAC_SHARE/libc math.h 410 log precondition Unknown arg_positive: x > 0 -FRAMAC_SHARE/libc math.h 496 fabs precondition Unknown finite_arg: \is_finite(x) -FRAMAC_SHARE/libc math.h 540 sqrt precondition Unknown finite_arg: \is_finite(x) -FRAMAC_SHARE/libc math.h 541 sqrt precondition Unknown arg_positive: x ≥ -0. +FRAMAC_SHARE/libc math.h 325 exp precondition Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9 +FRAMAC_SHARE/libc math.h 362 log precondition Unknown finite_arg: \is_finite(x) +FRAMAC_SHARE/libc math.h 363 log precondition Unknown arg_positive: x > 0 +FRAMAC_SHARE/libc math.h 449 fabs precondition Unknown finite_arg: \is_finite(x) +FRAMAC_SHARE/libc math.h 493 sqrt precondition Unknown finite_arg: \is_finite(x) +FRAMAC_SHARE/libc math.h 494 sqrt precondition Unknown arg_positive: x ≥ -0. FRAMAC_SHARE/libc netdb.c 113 gethostbyname mem_access Unknown \valid_read(cp) FRAMAC_SHARE/libc netdb.c 116 gethostbyname mem_access Unknown \valid_read(cp) FRAMAC_SHARE/libc netdb.c 119 gethostbyname precondition of inet_addr Unknown valid_arg: valid_read_string(arg) diff --git a/chrony/chrony-regress.eva/alarms.csv b/chrony/chrony-regress.eva/alarms.csv index 1165a78af..282a9863a 100644 --- a/chrony/chrony-regress.eva/alarms.csv +++ b/chrony/chrony-regress.eva/alarms.csv @@ -94,9 +94,9 @@ directory file line function property kind status property . regress.c 698 RGR_MultipleRegress precondition of fabs Unknown finite_arg: \is_finite(x) . regress.c 698 RGR_MultipleRegress precondition of fabs Unknown finite_arg: \is_finite(x) FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0 -FRAMAC_SHARE/libc math.h 496 fabs precondition Unknown finite_arg: \is_finite(x) -FRAMAC_SHARE/libc math.h 540 sqrt precondition Unknown finite_arg: \is_finite(x) -FRAMAC_SHARE/libc math.h 541 sqrt precondition Unknown arg_positive: x ≥ -0. +FRAMAC_SHARE/libc math.h 449 fabs precondition Unknown finite_arg: \is_finite(x) +FRAMAC_SHARE/libc math.h 493 sqrt precondition Unknown finite_arg: \is_finite(x) +FRAMAC_SHARE/libc math.h 494 sqrt precondition Unknown arg_positive: x ≥ -0. FRAMAC_SHARE/libc string.h 115 memset precondition Unknown valid_s: valid_or_empty(s, n) test/unit regress.c 45 test_unit initialization Unknown \initialized(&x[j]) test/unit regress.c 52 test_unit precondition of fabs Unknown finite_arg: \is_finite(x) diff --git a/frama-c b/frama-c index c32afcc40..5e840bb70 160000 --- a/frama-c +++ b/frama-c @@ -1 +1 @@ -Subproject commit c32afcc4038b1234219137cae196f3f776533d2f +Subproject commit 5e840bb7060585b81d8fc0d76b3627ca2b8d004d diff --git a/icpc/icpc.eva/alarms.csv b/icpc/icpc.eva/alarms.csv index a57d417ac..885b59dc3 100644 --- a/icpc/icpc.eva/alarms.csv +++ b/icpc/icpc.eva/alarms.csv @@ -1,6 +1,6 @@ directory file line function property kind status property -FRAMAC_SHARE/libc math.h 372 exp precondition Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9 -FRAMAC_SHARE/libc math.h 496 fabs precondition Unknown finite_arg: \is_finite(x) +FRAMAC_SHARE/libc math.h 325 exp precondition Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9 +FRAMAC_SHARE/libc math.h 449 fabs precondition Unknown finite_arg: \is_finite(x) FRAMAC_SHARE/libc stdio.h 207 fprintf assigns clause Unknown assigns \result, *stream; FRAMAC_SHARE/libc stdio.h 207 fprintf from clause Unknown assigns *stream \from *stream, *(format + (0 ..)); FRAMAC_SHARE/libc stdio.h 207 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..)); diff --git a/libmodbus/libmodbus-unit-server.eva/alarms.csv b/libmodbus/libmodbus-unit-server.eva/alarms.csv index 8c7b4ad6e..d73dfeb3b 100644 --- a/libmodbus/libmodbus-unit-server.eva/alarms.csv +++ b/libmodbus/libmodbus-unit-server.eva/alarms.csv @@ -4,7 +4,7 @@ FRAMAC_SHARE/libc string.c 130 strcmp mem_access Unknown \valid_read(s1 + i) FRAMAC_SHARE/libc string.c 133 strcmp mem_access Unknown \valid_read((unsigned char *)s1 + i) FRAMAC_SHARE/libc string.h 92 memcpy precondition Unknown valid_dest: valid_or_empty(dest, n) FRAMAC_SHARE/libc string.h 93 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n) -FRAMAC_SHARE/libc time.h 270 nanosleep precondition Unknown valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000 +FRAMAC_SHARE/libc time.h 280 nanosleep precondition Unknown valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000 FRAMAC_SHARE/libc unistd.h 782 close precondition Unknown valid_fd: 0 ≤ fd < 1024 FRAMAC_SHARE/libc unistd.h 1004 read precondition Unknown valid_fd: 0 ≤ fd < 1024 FRAMAC_SHARE/libc unistd.h 1005 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1)) diff --git a/papabench/papabench.eva/alarms.csv b/papabench/papabench.eva/alarms.csv index f84c7ba75..b808f21c3 100644 --- a/papabench/papabench.eva/alarms.csv +++ b/papabench/papabench.eva/alarms.csv @@ -1,9 +1,9 @@ directory file line function property kind status property -FRAMAC_SHARE/libc math.h 398 frexpf assigns clause Unknown assigns \result, *exp; -FRAMAC_SHARE/libc math.h 398 frexpf from clause Unknown assigns *exp \from *exp, value; -FRAMAC_SHARE/libc math.h 398 frexpf from clause Unknown assigns \result \from *exp, value; -FRAMAC_SHARE/libc math.h 405 ldexp assigns clause Unknown assigns \nothing; -FRAMAC_SHARE/libc math.h 405 ldexp from clause Unknown assigns \result \from x, exp; +FRAMAC_SHARE/libc math.h 351 frexpf assigns clause Unknown assigns \result, *exp; +FRAMAC_SHARE/libc math.h 351 frexpf from clause Unknown assigns *exp \from *exp, value; +FRAMAC_SHARE/libc math.h 351 frexpf from clause Unknown assigns \result \from *exp, value; +FRAMAC_SHARE/libc math.h 358 ldexp assigns clause Unknown assigns \nothing; +FRAMAC_SHARE/libc math.h 358 ldexp from clause Unknown assigns \result \from x, exp; sw/airborne/autopilot estimator.c 116 estimator_update_state_infrared is_nan Unknown ¬\is_NaN(\mul_float(rad_of_ir, (float)ir_roll)) sw/airborne/autopilot estimator.c 118 estimator_update_state_infrared is_nan Unknown ¬\is_NaN(\mul_float(rad_of_ir, (float)ir_pitch)) sw/airborne/autopilot estimator.c 158 estimator_update_ir_estim is_nan Unknown ¬\is_NaN(\div_float(estimator_update_ir_estim_sum_xy, estimator_update_ir_estim_sum_xx)) -- GitLab