Skip to content

GitLab

Commit b2ff2f68 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

synchronize with frama-c master

parent e39493d3
Pipeline #39608 failed with stage
in 58 minutes and 29 seconds
Hide whitespace changes
Inline Side-by-side
c-testsuite/.frama-c/00198.parse/warnings.log
View file @ b2ff2f68
00198.c:13:[kernel:parser:unsupported] warning: block-level typedefs currently unsupported;
trying to convert it to a global-level typedef.
Note that this may lead to incoherent error messages.
00198.c:14:[kernel:parser:unsupported] warning: block-level typedefs currently unsupported;
trying to convert it to a global-level typedef.
Note that this may lead to incoherent error messages.
chrony/.frama-c/chrony-ntp-core.eva/alarms.csv
View file @ b2ff2f68
......@@ -638,6 +638,7 @@ directory file line function property kind status property
. sourcestats.c 578 SST_DoNewRegression initialization Unknown \initialized(&est_intercept)
. sourcestats.c 579 SST_DoNewRegression initialization Unknown \initialized(&inst->last_sample)
. sourcestats.c 580 SST_DoNewRegression initialization Unknown \initialized(&est_intercept_sd)
. sourcestats.c 581 SST_DoNewRegression initialization Unknown \initialized(&est_var)
. sourcestats.c 582 SST_DoNewRegression initialization Unknown \initialized(&nruns)
. sourcestats.c 593 SST_DoNewRegression initialization Unknown \initialized(&best_start)
. sourcestats.c 593 SST_DoNewRegression initialization Unknown \initialized(&inst->asymmetry)
......@@ -853,8 +854,8 @@ FRAMAC_SHARE/libc string.h 121 memmove precondition Unknown valid_src: valid_rea
FRAMAC_SHARE/libc string.h 131 memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 141 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 173 strchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 775 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1124 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 761 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1110 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from *(__x0 + (0 ..)), __x1;
FRAMAC_SHARE/libc/sys stat.h 87 stat precondition Unknown valid_pathname: valid_read_string(pathname)
......
chrony/.frama-c/chrony-ntp-core.eva/warnings.log
View file @ b2ff2f68
......@@ -6625,6 +6625,16 @@ stack: SST_DoNewRegression :: sources.c:350 <-
main :: fc_stubs.c:37 <-
eva_main
sourcestats.c:580:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(&est_intercept_sd);
stack: SST_DoNewRegression :: sources.c:350 <-
SRC_AccumulateSample :: ntp_core.c:1506 <-
process_sample :: ntp_core.c:1834 <-
receive_packet :: ntp_core.c:2070 <-
NCR_ProcessRxKnown :: test/unit/ntp_core.c:251 <-
process_response :: test/unit/ntp_core.c:391 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
sourcestats.c:581:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(&est_var);
stack: SST_DoNewRegression :: sources.c:350 <-
SRC_AccumulateSample :: ntp_core.c:1506 <-
process_sample :: ntp_core.c:1834 <-
......
frama-c @ ea345863
Compare 9b464ff0...ea345863
Subproject commit 9b464ff0d452e265e51da668aa2daee3de212280
Subproject commit ea345863192f8b305f3d4b2a3f347e79f3b786a3
gzip124/.frama-c/gzip124.eva/alarms.csv
View file @ b2ff2f68
......@@ -674,14 +674,14 @@ FRAMAC_SHARE/libc string.h 368 strcpy precondition Invalid or unreachable room_s
FRAMAC_SHARE/libc string.h 424 strcat precondition Unknown valid_string_src: valid_read_string(src)
FRAMAC_SHARE/libc string.h 425 strcat precondition Unknown valid_string_dest: valid_string(dest)
FRAMAC_SHARE/libc string.h 426 strcat precondition Unknown room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
FRAMAC_SHARE/libc unistd.h 775 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 783 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 968 lseek precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1007 read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1008 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1124 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1140 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1141 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 761 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 769 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 954 lseek precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 993 read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 994 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1110 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1126 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1127 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from *(__x0 + (0 ..)), __x1;
FRAMAC_SHARE/libc/sys stat.h 35 fstat assigns clause Unknown assigns \result, *__x1;
......
hiredis/.frama-c/hiredis-format.eva/alarms.csv
View file @ b2ff2f68
......@@ -85,6 +85,7 @@ directory file line function property kind status property
. sds.c 198 sdsMakeRoomFor initialization Unknown \initialized(s + (int)(-1))
. sds.c 198 sdsMakeRoomFor mem_access Unknown \valid_read(s + (int)(-1))
. sds.c 221 sdsMakeRoomFor precondition of realloc Unknown freeable: ptr ≡ \null ∨ \freeable(ptr)
. sds.c 223 sdsMakeRoomFor dangling_pointer Unknown ¬\dangling(&sh)
. sds.c 223 sdsMakeRoomFor precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
. sds.c 232 sdsMakeRoomFor precondition of memcpy Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
. sds.c 232 sdsMakeRoomFor precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
......@@ -244,4 +245,4 @@ FRAMAC_SHARE/libc string.h 95 memcpy precondition Unknown valid_dest: valid_or_e
FRAMAC_SHARE/libc string.h 96 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 98 memcpy precondition Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 141 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 739 access precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 725 access precondition Unknown valid_string_path: valid_read_string(path)
hiredis/.frama-c/hiredis-misc.eva/alarms.csv
View file @ b2ff2f68
......@@ -198,6 +198,7 @@ directory file line function property kind status property
. sds.c 198 sdsMakeRoomFor initialization Unknown \initialized(s + (int)(-1))
. sds.c 198 sdsMakeRoomFor mem_access Unknown \valid_read(s + (int)(-1))
. sds.c 221 sdsMakeRoomFor precondition of realloc Unknown freeable: ptr ≡ \null ∨ \freeable(ptr)
. sds.c 223 sdsMakeRoomFor dangling_pointer Unknown ¬\dangling(&sh)
. sds.c 223 sdsMakeRoomFor precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
. sds.c 232 sdsMakeRoomFor precondition of memcpy Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
. sds.c 232 sdsMakeRoomFor precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
......@@ -334,7 +335,7 @@ FRAMAC_SHARE/libc string.h 528 strerror_r assigns clause Unknown assigns \result
FRAMAC_SHARE/libc string.h 528 strerror_r from clause Unknown assigns *(strerrbuf + (0 ..)) \from *(strerrbuf + (0 ..)), errnum, buflen;
FRAMAC_SHARE/libc string.h 528 strerror_r from clause Unknown assigns \result \from *(strerrbuf + (0 ..)), errnum, buflen;
FRAMAC_SHARE/libc strings.h 53 strncasecmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc unistd.h 739 access precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 725 access precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys socket.h 334 connect precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 370 getsockopt precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 525 setsockopt precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
icpc/.frama-c/icpc.eva/alarms.csv
View file @ b2ff2f68
directory file line function property kind status property
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_1 assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_1 from clause Unknown assigns *stream \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_1 from clause Unknown assigns \result \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_2 assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_2 from clause Unknown assigns *stream \from *stream, *(format + (0 ..)), param0, param1, param2, param3, param4;
FRAMAC_SHARE/libc stdio.h 207 fprintf_fallback_2 from clause Unknown assigns \result \from *stream, *(format + (0 ..)), param0, param1, param2, param3, param4;
src impls.c 96 Sleep signed_overflow Unknown _t + delayMs ≤ 2147483647
icpc/.frama-c/icpc.eva/warnings.log
View file @ b2ff2f68
src/main.c:33:[kernel:annot:missing-spec] warning: Neither code nor specification for function fprintf_fallback_1, generating default assigns from the prototype
src/main.c:41:[kernel:annot:missing-spec] warning: Neither code nor specification for function fprintf_fallback_2, generating default assigns from the prototype
icpc/.frama-c/icpc.parse/framac.ast
View file @ b2ff2f68
......@@ -752,11 +752,34 @@ void Sim_init(void)
char *output_header =
(char *)"time(ms)\tengineVoltage\tlegAngle\tlegAngleValid\tisActive\n";
char *output_row_fmt_string = (char *)"%d\t%f\t%f\t%d\t%d\n";
int fprintf_fallback_1(FILE * restrict stream, char const * restrict format);
int fprintf_fallback_2(FILE * restrict stream, char const * restrict format,
sint32 param0, real64 param1, real64 param2,
int param3, int param4);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param4),
(indirect: param3), (indirect: param2), (indirect: param1),
(indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param4, param3, param2, param1,
param0;
*/
int fprintf_va_2(FILE * restrict stream, char const * restrict format,
int param0, double param1, double param2, int param3,
int param4);
int main(void)
{
......@@ -772,7 +795,7 @@ int main(void)
RoCo_activeDesired = (char)1;
RoCo_moveFast = (char)0;
int cnt = 0;
fprintf(__fc_stderr,(char const *)output_header); /* fprintf_fallback_1 */
fprintf(__fc_stderr,(char const *)output_header); /* fprintf_va_1 */
while (cnt < 9000) {
sint32 tmp_0;
tmp_0 = Time();
......@@ -783,7 +806,7 @@ int main(void)
if (cnt % 5 == 0) fprintf(__fc_stderr,
(char const *)output_row_fmt_string,lastTime,
RoCo_engineVoltage,RoCo_legAngle,
(int)RoCo_legAngleValid,(int)RoCo_isActive); /* fprintf_fallback_2 */
(int)RoCo_legAngleValid,(int)RoCo_isActive); /* fprintf_va_2 */
Sleep(20);
cnt ++;
if (cnt == 2500) {
......
icpc/.frama-c/icpc.parse/warnings.log
View file @ b2ff2f68
src/roco_config.h:7:[kernel:parser:decimal-float] warning: Floating-point constant 0.33 is not represented exactly. Will use 0x1.51eb851eb851fp-2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
src/main.c:33:[variadic] warning: Call to function fprintf with non-static format argument:
no specification will be generated.
src/main.c:41:[variadic] warning: Call to function fprintf with non-static format argument:
no specification will be generated.
src/main.c:33:[variadic] warning: Call to function fprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
src/main.c:41:[variadic] warning: Call to function fprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
ioccc/.frama-c/2019_duble_prog.parse/framac.ast
View file @ b2ff2f68
......@@ -295,7 +295,17 @@ struct termios o;
int printf_va_1(char const * restrict format, char *param0, int param1,
char *param2);
int printf_fallback_1(char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_2(char const * restrict format);
/*@ requires valid_read_nstring(param2, 11);
requires valid_read_string(param7);
......@@ -316,7 +326,7 @@ int printf_fallback_1(char const * restrict format);
*(param8 + (0 ..)), *(param7 + (0 ..)), param6, param5, param4,
param3, *(param2 + (0 ..)), param1, param0;
*/
int printf_va_2(char const * restrict format, int param0, int param1,
int printf_va_3(char const * restrict format, int param0, int param1,
char *param2, int param3, int param4, int param5, int param6,
char *param7, char *param8);
......@@ -559,7 +569,7 @@ int main(int F_0, char **D_0)
}
}
}
printf((char const *)I); /* printf_fallback_1 */
printf((char const *)I); /* printf_va_2 */
break;
}
}
......@@ -594,7 +604,7 @@ int main(int F_0, char **D_0)
*(M - 6) = (char)(w.E * 7 + 48);
if (a) *(M + 2) = (char)42; else *(M + 2) = (char)32;
printf("\033[%d;%dH%.11s\033[%d;%dH\033[0;4%dm%c%s%s",
e + 2,d + 2,M - 8,24,8,x.D,x.J + 65,I + 8,J); /* printf_va_2 */
e + 2,d + 2,M - 8,24,8,x.D,x.J + 65,I + 8,J); /* printf_va_3 */
if (! ((f ^ d) | (e ^ h))) break;
b = n;
;
......
ioccc/.frama-c/2019_duble_prog.parse/warnings.log
View file @ b2ff2f68
......@@ -11,5 +11,4 @@
2019/duble/prog.c:40:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
2019/duble/prog.c:40:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
2019/duble/prog.c:44:[kernel:typing:incompatible-types-call] warning: expected 'struct sockaddr const *' but got argument of type 'struct sockaddr_un *': & A
2019/duble/prog.c:51:[variadic] warning: Call to function printf with non-static format argument:
no specification will be generated.
2019/duble/prog.c:51:[variadic] warning: Call to function printf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
ioccc/.frama-c/2019_lynn_prog.parse/framac.ast
View file @ b2ff2f68
......@@ -253,7 +253,18 @@ void d(void)
return;
}
int printf_fallback_1(char const * restrict format, P param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
int printf_va_1(char const * restrict format, unsigned int param0);
void R(void)
{
......@@ -264,7 +275,7 @@ void R(void)
D = & j[*(i + 2)];
tmp = U((unsigned int)1);
if (E) tmp_0 = "%c"; else tmp_0 = "%u,";
tmp_1 = printf(tmp_0,tmp); /* printf_fallback_1 */
tmp_1 = printf(tmp_0,tmp); /* printf_va_1 */
tmp_2 = w((unsigned int)2);
*D = l(tmp_2,(unsigned int)tmp_1);
D ++;
......
ioccc/.frama-c/2019_lynn_prog.parse/warnings.log
View file @ b2ff2f68
2019/lynn/prog.c:27:[variadic] warning: Call to function printf with non-static format argument:
no specification will be generated.
2019/lynn/prog.c:27:[variadic] warning: Call to function printf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
kilo/.frama-c/kilo.eva/alarms.csv
View file @ b2ff2f68
......@@ -557,8 +557,8 @@ FRAMAC_SHARE/libc ctype.h 94 isdigit precondition Unknown c_uchar_or_eof: (0 ≤
FRAMAC_SHARE/libc ctype.h 134 isprint precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc ctype.h 161 isspace precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc fcntl.h 165 __va_open_mode_t precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.c 68 getline mem_access Unknown \valid(*lineptr + tmp_2)
FRAMAC_SHARE/libc stdio.c 71 getline mem_access Unknown \valid(*lineptr + cur)
FRAMAC_SHARE/libc stdio.c 69 getline mem_access Unknown \valid(*lineptr + tmp_2)
FRAMAC_SHARE/libc stdio.c 72 getline mem_access Unknown \valid(*lineptr + cur)
FRAMAC_SHARE/libc stdio.h 213 snprintf_va_4 precondition Unknown valid_read_nstring(param0, 20)
FRAMAC_SHARE/libc stdio.h 217 sscanf_va_1 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
......@@ -580,6 +580,6 @@ FRAMAC_SHARE/libc string.h 120 memmove precondition Unknown valid_dest: valid_or
FRAMAC_SHARE/libc string.h 121 memmove precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 131 memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 141 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 867 ftruncate assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc unistd.h 867 ftruncate from clause Unknown assigns \result \from __x0, __x1;
FRAMAC_SHARE/libc unistd.h 1141 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 853 ftruncate assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc unistd.h 853 ftruncate from clause Unknown assigns \result \from __x0, __x1;
FRAMAC_SHARE/libc unistd.h 1127 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
libmodbus/.frama-c/libmodbus-unit-server.eva/alarms.csv
View file @ b2ff2f68
......@@ -4,9 +4,9 @@ FRAMAC_SHARE/libc string.c 146 strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 149 strcmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.h 95 memcpy precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 96 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc time.h 288 nanosleep precondition Unknown valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
FRAMAC_SHARE/libc unistd.h 1008 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1141 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc time.h 287 nanosleep precondition Unknown valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
FRAMAC_SHARE/libc unistd.h 994 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1127 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc/sys socket.h 301 accept precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 436 recv precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 437 recv precondition Unknown valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
......
microstrain/.frama-c/microstrain_gx4_45_test.eva/alarms.csv
View file @ b2ff2f68
......@@ -17,10 +17,10 @@ FRAMAC_SHARE/libc string.h 95 memcpy precondition Unknown valid_dest: valid_or_e
FRAMAC_SHARE/libc string.h 96 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 368 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 426 strcat precondition Unknown room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
FRAMAC_SHARE/libc unistd.h 1007 read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1008 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1140 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1141 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 993 read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 994 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1126 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1127 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test GX4-45_Test.c 258 main precondition of printf_va_25 Unknown valid_read_string(param0)
MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test GX4-45_Test.c 261 main precondition of printf_va_26 Unknown valid_read_string(param0)
MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test GX4-45_Test.c 264 main precondition of printf_va_27 Unknown valid_read_string(param0)
......
miniz/.frama-c/miniz-example1.eva/alarms.csv
View file @ b2ff2f68
......@@ -33,7 +33,6 @@ directory file line function property kind status property
. miniz.c 265 mz_deflate initialization Unknown \initialized(&in_bytes)
. miniz.c 270 mz_deflate dangling_pointer Unknown ¬\dangling(&out_bytes)
. miniz.c 270 mz_deflate initialization Unknown \initialized(&out_bytes)
. miniz.c 323 mz_compress2 dangling_pointer Unknown ¬\dangling(pDest_len)
. miniz.c 342 mz_compress2 dangling_pointer Unknown ¬\dangling(&stream.total_out)
. miniz.c 447 mz_inflate dangling_pointer Unknown ¬\dangling(&pState->m_window_bits)
. miniz.c 447 mz_inflate initialization Unknown \initialized(&pState->m_window_bits)
......@@ -1945,6 +1944,7 @@ FRAMAC_SHARE/libc string.h 95 memcpy precondition Unknown valid_dest: valid_or_e
FRAMAC_SHARE/libc string.h 96 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 98 memcpy precondition Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 131 memset precondition Unknown valid_s: valid_or_empty(s, n)
examples example1.c 34 main dangling_pointer Unknown ¬\dangling(&cmp_len)
examples example1.c 52 main dangling_pointer Unknown ¬\dangling(&cmp_len)
examples example1.c 60 main division_by_zero Unknown cmp_len ≢ 0
examples example1.c 61 main dangling_pointer Unknown ¬\dangling(pCmp + i)
......
miniz/.frama-c/miniz-example2.eva/alarms.csv
View file @ b2ff2f68
......@@ -2104,6 +2104,8 @@ directory file line function property kind status property
. miniz_zip.c 2643 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&new_capacity)
. miniz_zip.c 2643 mz_zip_heap_write_func mem_access Unknown \valid(&pState->m_mem_capacity)
. miniz_zip.c 2645 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&file_ofs)
. miniz_zip.c 2645 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&n)
. miniz_zip.c 2645 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&pBuf)
. miniz_zip.c 2645 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&pState->m_pMem)
. miniz_zip.c 2645 mz_zip_heap_write_func initialization Unknown \initialized(&pState->m_pMem)
. miniz_zip.c 2645 mz_zip_heap_write_func mem_access Unknown \valid_read(&pState->m_pMem)
......@@ -2112,7 +2114,6 @@ directory file line function property kind status property
. miniz_zip.c 2645 mz_zip_heap_write_func precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. miniz_zip.c 2646 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&new_size)
. miniz_zip.c 2646 mz_zip_heap_write_func mem_access Unknown \valid(&pState->m_mem_size)
. miniz_zip.c 2647 mz_zip_heap_write_func dangling_pointer Unknown ¬\dangling(&n)
. miniz_zip.c 2655 mz_zip_writer_end_internal dangling_pointer Unknown ¬\dangling(&pZip->m_pState)
. miniz_zip.c 2655 mz_zip_writer_end_internal initialization Unknown \initialized(&pZip->m_pState)
. miniz_zip.c 2655 mz_zip_writer_end_internal ptr_comparison Unknown \pointer_comparable((void *)0, (void *)pZip->m_pState)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment