Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
open-source-case-studies
Commits
29a4d00c
Commit
29a4d00c
authored
Jul 19, 2021
by
Andre Maroneze
💬
Browse files
synchronize with frama-c master
parent
d496a077
Pipeline
#36650
failed with stage
in 90 minutes and 9 seconds
Changes
35
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
2048/.frama-c/2048.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -15,4 +15,4 @@ FRAMAC_SHARE/libc stdio.h 211 printf_va_12 precondition Unknown valid_read_strin
FRAMAC_SHARE/libc stdio.h 211 printf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_7 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 211 printf_va_8 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc string.h 1
28
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
41
strlen precondition Unknown valid_string_s: valid_read_string(s)
basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -2,4 +2,4 @@ directory file line function property kind status property
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s1 + i)
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + i)
. cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 3
55
strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 3
68
strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -2,4 +2,4 @@ directory file line function property kind status property
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s1 + i)
. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + i)
. cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 3
55
strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 3
68
strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
chrony/.frama-c/chrony-ntp-core.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -820,39 +820,39 @@ FRAMAC_SHARE/libc stdio.h 351 fread precondition Unknown valid_ptr_block: \valid
FRAMAC_SHARE/libc stdio.h 558 popen precondition Unknown valid_command: valid_read_string(command)
FRAMAC_SHARE/libc stdio.h 573 pclose precondition Unknown open_pipe: is_open_pipe(stream)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc string.c 1
30
strcmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
30
strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
30
strcmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
33
strcmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
33
strcmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
39
strncmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
39
strncmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
40
strncmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
40
strncmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
74
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 18
2
strcat precondition of strlen Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.c 1
83
strcat mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c
184
strcat mem_access Unknown \valid(dest + (unsigned long)(n + i))
FRAMAC_SHARE/libc string.c
186
strcat mem_access Unknown \valid(dest + (unsigned long)(n + i))
FRAMAC_SHARE/libc string.c 2
07
strcpy initialization Unknown \initialized(src + i)
FRAMAC_SHARE/libc string.c 2
07
strcpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c 2
08
strcpy mem_access Unknown \valid(dest + i)
FRAMAC_SHARE/libc string.c 2
09
strcpy mem_access Unknown \valid(dest + i)
FRAMAC_SHARE/libc string.c 2
17
strncpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c
292
strdup precondition of strlen Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.c
298
strdup precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.c
298
strdup precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.c 1
46
strcmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
49
strcmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
49
strcmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
55
strncmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
55
strncmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
56
strncmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
56
strncmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
90
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
9
8 strcat precondition of strlen Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.c 1
99
strcat mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c
200
strcat mem_access Unknown \valid(dest + (unsigned long)(n + i))
FRAMAC_SHARE/libc string.c
202
strcat mem_access Unknown \valid(dest + (unsigned long)(n + i))
FRAMAC_SHARE/libc string.c 2
23
strcpy initialization Unknown \initialized(src + i)
FRAMAC_SHARE/libc string.c 2
23
strcpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c 2
24
strcpy mem_access Unknown \valid(dest + i)
FRAMAC_SHARE/libc string.c 2
25
strcpy mem_access Unknown \valid(dest + i)
FRAMAC_SHARE/libc string.c 2
43
strncpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c
318
strdup precondition of strlen Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.c
324
strdup precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.c
324
strdup precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
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 string.h 98 memcpy precondition Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 10
7
memmove precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 1
08
memmove precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 11
8
memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 1
28
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
60
strchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
2
0 memmove precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 1
21
memmove precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 1
3
1 memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 1
41
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
73
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/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
...
...
chrony/.frama-c/chrony-ntp-core.eva/warnings.log
View file @
29a4d00c
This diff is collapsed.
Click to expand it.
chrony/.frama-c/chrony-regress.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -82,7 +82,7 @@ directory file line function property kind status property
. regress.c 679 RGR_MultipleRegress initialization Unknown \initialized(x2 + i)
. regress.c 683 RGR_MultipleRegress initialization Unknown \initialized(y + i)
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0
FRAMAC_SHARE/libc string.h 11
8
memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 1
3
1 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 66 test_unit initialization Unknown \initialized(&b2)
test/unit regress.c 70 test_unit initialization Unknown \initialized(&y[(long)(tmp_11 % (long)n)])
...
...
frama-c
@
1b16ab8f
Compare
ab43a5ed
...
1b16ab8f
Subproject commit
ab43a5ed6ba8a5975fa70813fdfa96d1f20586
d7
Subproject commit
1b16ab8f41f92f6efaed2ff992f933c424d15
d7
5
genann/.frama-c/genann.parse/framac.ast
View file @
29a4d00c
...
...
@@ -202,8 +202,8 @@ genann *genann_init(int inputs, int hidden_layers, int hidden, int outputs)
ret->output = ret->weight + ret->total_weights;
ret->delta = ret->output + ret->total_neurons;
genann_randomize(ret);
ret->activation_hidden =
(double (*)(struct genann const *ann, double a))(
& genann_act_sigmoid_cached
)
;
ret->activation_output =
(double (*)(struct genann const *ann, double a))(
& genann_act_sigmoid_cached
)
;
ret->activation_hidden = & genann_act_sigmoid_cached;
ret->activation_output = & genann_act_sigmoid_cached;
genann_init_sigmoid_lookup((genann const *)ret);
__retres = ret;
return_label: return __retres;
...
...
gzip124/.frama-c/gzip124.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -656,18 +656,18 @@ FRAMAC_SHARE/libc stdlib.c 60 atoi signed_overflow Unknown n + (int)((int)'0' -
FRAMAC_SHARE/libc stdlib.c 62 atoi signed_overflow Unknown -n ≤ 2147483647
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 string.h 1
28
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
40
strcmp precondition Unknown valid_string_s1: valid_read_string(s1)
FRAMAC_SHARE/libc string.h 14
1
strcmp precondition Unknown valid_string_s2: valid_read_string(s2)
FRAMAC_SHARE/libc string.h 1
47
strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 1
48
strncmp precondition Unknown valid_string_s2: valid_read_nstring(s2, n)
FRAMAC_SHARE/libc string.h 1
84
strrchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 2
00
strcspn precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 3
54
strcpy precondition Unknown valid_string_src: valid_read_string(src)
FRAMAC_SHARE/libc string.h 3
55
strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 4
11
strcat precondition Unknown valid_string_src: valid_read_string(src)
FRAMAC_SHARE/libc string.h 4
1
2 strcat precondition Unknown valid_string_dest: valid_string(dest)
FRAMAC_SHARE/libc string.h 4
13
strcat precondition Unknown room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
FRAMAC_SHARE/libc string.h 1
41
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
53
strcmp precondition Unknown valid_string_s1: valid_read_string(s1)
FRAMAC_SHARE/libc string.h 1
5
4 strcmp precondition Unknown valid_string_s2: valid_read_string(s2)
FRAMAC_SHARE/libc string.h 1
60
strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 1
61
strncmp precondition Unknown valid_string_s2: valid_read_nstring(s2, n)
FRAMAC_SHARE/libc string.h 1
97
strrchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 2
13
strcspn precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 3
67
strcpy precondition Unknown valid_string_src: valid_read_string(src)
FRAMAC_SHARE/libc string.h 3
68
strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
FRAMAC_SHARE/libc string.h 4
24
strcat precondition Unknown valid_string_src: valid_read_string(src)
FRAMAC_SHARE/libc string.h 42
5
strcat precondition Unknown valid_string_dest: valid_string(dest)
FRAMAC_SHARE/libc string.h 4
26
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
...
...
hiredis/.frama-c/hiredis-format.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -229,19 +229,19 @@ FRAMAC_SHARE/libc stdio.h 207 fprintf_va_2 precondition Unknown valid_read_strin
FRAMAC_SHARE/libc stdlib.h 78 atoi precondition Unknown valid_nptr: \valid_read(nptr)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdlib.h 422 realloc precondition Unknown freeable: ptr ≡ \null ∨ \freeable(ptr)
FRAMAC_SHARE/libc string.c 1
30
strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
30
strcmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
39
strncmp dangling_pointer Unknown ¬\dangling(s1 + i)
FRAMAC_SHARE/libc string.c 1
39
strncmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
39
strncmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
39
strncmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
40
strncmp dangling_pointer Unknown ¬\dangling((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
40
strncmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
40
strncmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
40
strncmp signed_overflow Unknown (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i) ≤ 2147483647
FRAMAC_SHARE/libc string.c 1
40
strncmp signed_overflow Unknown -2147483648 ≤ (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
55
strncmp dangling_pointer Unknown ¬\dangling(s1 + i)
FRAMAC_SHARE/libc string.c 1
55
strncmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
55
strncmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
55
strncmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
56
strncmp dangling_pointer Unknown ¬\dangling((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
56
strncmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
56
strncmp mem_access Unknown \valid_read((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
56
strncmp signed_overflow Unknown (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i) ≤ 2147483647
FRAMAC_SHARE/libc string.c 1
56
strncmp signed_overflow Unknown -2147483648 ≤ (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + 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 string.h 98 memcpy precondition Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 1
28
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
41
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)
hiredis/.frama-c/hiredis-misc.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -313,26 +313,26 @@ FRAMAC_SHARE/libc stdio.h 213 snprintf_va_15 precondition Unknown valid_read_str
FRAMAC_SHARE/libc stdlib.h 78 atoi precondition Unknown valid_nptr: \valid_read(nptr)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdlib.h 422 realloc precondition Unknown freeable: ptr ≡ \null ∨ \freeable(ptr)
FRAMAC_SHARE/libc string.c 1
30
strcmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
30
strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
30
strcmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
33
strcmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp dangling_pointer Unknown ¬\dangling(s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
70
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
74
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 2
07
strcpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c 2
17
strncpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
46
strcmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
49
strcmp initialization Unknown \initialized((unsigned char *)s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp dangling_pointer Unknown ¬\dangling(s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp mem_access Unknown \valid_read(s1 + i)
FRAMAC_SHARE/libc string.c 1
86
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 1
90
strcasecmp mem_access Unknown \valid_read(s2 + i)
FRAMAC_SHARE/libc string.c 2
23
strcpy mem_access Unknown \valid_read(src + i)
FRAMAC_SHARE/libc string.c 2
43
strncpy mem_access Unknown \valid_read(src + 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 string.h 98 memcpy precondition Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 10
7
memmove precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 1
08
memmove precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 1
28
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 5
15
strerror_r assigns clause Unknown assigns \result, *(strerrbuf + (0 ..));
FRAMAC_SHARE/libc string.h 5
15
strerror_r from clause Unknown assigns *(strerrbuf + (0 ..)) \from *(strerrbuf + (0 ..)), errnum, buflen;
FRAMAC_SHARE/libc string.h 5
15
strerror_r from clause Unknown assigns \result \from *(strerrbuf + (0 ..)), errnum, buflen;
FRAMAC_SHARE/libc string.h 1
2
0 memmove precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 1
21
memmove precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 1
41
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 5
28
strerror_r assigns clause Unknown assigns \result, *(strerrbuf + (0 ..));
FRAMAC_SHARE/libc string.h 5
28
strerror_r from clause Unknown assigns *(strerrbuf + (0 ..)) \from *(strerrbuf + (0 ..)), errnum, buflen;
FRAMAC_SHARE/libc string.h 5
28
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/sys socket.h 334 connect precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
...
...
hiredis/.frama-c/hiredis-misc.eva/warnings.log
View file @
29a4d00c
...
...
@@ -39,17 +39,17 @@ net.c:495:[eva] warning: ignoring unsupported \allocates clause
test.c:511:[eva] warning: ignoring unsupported \allocates clause
[eva:garbled-mix] warning: Garbled mix generated during analysis:
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{defaultFunctions}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{defaultFunctions}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{defaultFunctions}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77;
__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_1;
...
...
@@ -178,12 +178,12 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_0;
__realloc_sdsMakeRoomFor_l221_1;
__realloc_sdsMakeRoomFor_l221_2}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_0}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77;
__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_1;
...
...
@@ -196,16 +196,16 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_8;
__calloc_w_createReplyObject_l77_9;
__calloc_w_createReplyObject_l77_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_0;
__realloc_sdsMakeRoomFor_l221_1;
__realloc_sdsMakeRoomFor_l221_2}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_0}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77;
__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_1;
...
...
@@ -218,16 +218,16 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_8;
__calloc_w_createReplyObject_l77_9;
__calloc_w_createReplyObject_l77_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_0;
__realloc_sdsMakeRoomFor_l221_1;
__realloc_sdsMakeRoomFor_l221_2}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_0}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77;
__calloc_w_createReplyObject_l77_0;
__calloc_w_createReplyObject_l77_1;
...
...
@@ -240,7 +240,7 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_8;
__calloc_w_createReplyObject_l77_9;
__calloc_w_createReplyObject_l77_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_11;
__calloc_w_createReplyObject_l77_12;
__calloc_w_createReplyObject_l77_13;
...
...
@@ -343,32 +343,32 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_24}
(origin: Arithmetic {read.c:251}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_5}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_26}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_5}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_26}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_5}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_26}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_7}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_29;
__calloc_w_createReplyObject_l77_30}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_7}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_29;
__calloc_w_createReplyObject_l77_30}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_7}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_29;
__calloc_w_createReplyObject_l77_30}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_32;
__calloc_w_createReplyObject_l77_33;
...
...
@@ -489,12 +489,12 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_44}
(origin: Arithmetic {read.c:251}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_8}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_44}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_6}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_32;
__calloc_w_createReplyObject_l77_33;
...
...
@@ -509,14 +509,14 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_42;
__calloc_w_createReplyObject_l77_43;
__calloc_w_createReplyObject_l77_44}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_8}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_44}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_6}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_32;
__calloc_w_createReplyObject_l77_33;
...
...
@@ -531,14 +531,14 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_42;
__calloc_w_createReplyObject_l77_43;
__calloc_w_createReplyObject_l77_44}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_8}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_44}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_6}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_31;
__calloc_w_createReplyObject_l77_32;
__calloc_w_createReplyObject_l77_33;
...
...
@@ -553,25 +553,25 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_42;
__calloc_w_createReplyObject_l77_43;
__calloc_w_createReplyObject_l77_44}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_9}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_45;
__calloc_w_createReplyObject_l77_46;
__calloc_w_createReplyObject_l77_47}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_9}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_45;
__calloc_w_createReplyObject_l77_46;
__calloc_w_createReplyObject_l77_47}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_9}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_45;
__calloc_w_createReplyObject_l77_46;
__calloc_w_createReplyObject_l77_47}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_49;
__calloc_w_createReplyObject_l77_50;
...
...
@@ -674,12 +674,12 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_61}
(origin: Arithmetic {read.c:251}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_61}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_8}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_49;
__calloc_w_createReplyObject_l77_50;
...
...
@@ -694,14 +694,14 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_59;
__calloc_w_createReplyObject_l77_60;
__calloc_w_createReplyObject_l77_61}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_61}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_8}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_49;
__calloc_w_createReplyObject_l77_50;
...
...
@@ -716,14 +716,14 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_59;
__calloc_w_createReplyObject_l77_60;
__calloc_w_createReplyObject_l77_61}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_10}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_61}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_8}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_48;
__calloc_w_createReplyObject_l77_49;
__calloc_w_createReplyObject_l77_50;
...
...
@@ -738,32 +738,32 @@ test.c:511:[eva] warning: ignoring unsupported \allocates clause
__calloc_w_createReplyObject_l77_59;
__calloc_w_createReplyObject_l77_60;
__calloc_w_createReplyObject_l77_61}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_11}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_62}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
70
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
86
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_11}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_62}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
74
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
90
}) }}
{{ garbled mix of &{__realloc_sdsMakeRoomFor_l221_11}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__calloc_w_createReplyObject_l77_62}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
75
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
91
}) }}
{{ garbled mix of &{__malloc_sdsnewlen_l91_18}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_14}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
{{ garbled mix of &{__malloc_strdup_l
293
}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__malloc_strdup_l
319
}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__malloc_w_hi_malloc_l36}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__malloc_sdsnewlen_l91_20}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__calloc_redisReaderCreateWithFunctions_l561_15}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
{{ garbled mix of &{__malloc_strdup_l
293
_0}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__malloc_strdup_l
319
_0}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
{{ garbled mix of &{__malloc_w_hi_malloc_l36_0}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
30
}) }}
(origin: Misaligned {FRAMAC_SHARE/libc/string.c:1
46
}) }}
ioccc/.frama-c/2019_adamovsky_iocccsize_2018.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -61,5 +61,5 @@ FRAMAC_SHARE/libc ctype.h 161 isspace precondition Unknown c_uchar_or_eof: (0
FRAMAC_SHARE/libc stdio.h 258 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 281 fputc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 343 ungetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc string.h 1
47
strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 20
7
strspn precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
60
strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 2
2
0 strspn precondition Unknown valid_string_s: valid_read_string(s)
ioccc/.frama-c/2019_iocccsize.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -61,5 +61,5 @@ FRAMAC_SHARE/libc ctype.h 161 isspace precondition Unknown c_uchar_or_eof: (0
FRAMAC_SHARE/libc stdio.h 258 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 281 fputc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 343 ungetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc string.h 1
47
strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 20
7
strspn precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
60
strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 2
2
0 strspn precondition Unknown valid_string_s: valid_read_string(s)
ioccc/.frama-c/2020_giles_prog.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -216,5 +216,5 @@ FRAMAC_SHARE/libc stdio.h 352 fread precondition Unknown valid_stream: \valid(st
FRAMAC_SHARE/libc stdio.h 365 fwrite precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc string.h 57 memcmp precondition Unknown initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 58 memcmp precondition Unknown initialization: s2: \initialized((char *)s2 + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 1
28
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
60
strchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
41
strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 1
73
strchr precondition Unknown valid_string_s: valid_read_string(s)
itc-benchmarks/.frama-c/01_w_Defects.eva/alarms.csv
View file @
29a4d00c
...
...
@@ -423,9 +423,9 @@ directory file line function property kind status property
01_w_Defects zero_division.c 230 zero_division_015 division_by_zero Invalid or unreachable divisor1 ≢ 0
01_w_Defects zero_division.c 257 zero_division_016 division_by_zero Invalid or unreachable divisor2 ≢ 0
FRAMAC_SHARE/libc stdlib.h 405 free precondition Invalid or unreachable freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc string.c 2
07
strcpy initialization Unknown \initialized(src + i)
FRAMAC_SHARE/libc string.c 2
08
strcpy mem_access Unknown \valid(dest + i)
FRAMAC_SHARE/libc string.c 2
23
strcpy initialization Unknown \initialized(src + i)
FRAMAC_SHARE/libc string.c 2
24
strcpy mem_access Unknown \valid(dest + 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 string.h 98 memcpy precondition Unknown separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 11
8
memset precondition Invalid or unreachable valid_s: valid_or_empty(s_0, n)
FRAMAC_SHARE/libc string.h 1
3
1 memset precondition Invalid or unreachable valid_s: valid_or_empty(s_0, n)
itc-benchmarks/.frama-c/01_w_Defects.eva/nonterm.log
View file @
29a4d00c
FRAMAC_SHARE/libc/string.c:2
07
:[nonterm:stmt] warning: non-terminating loop
FRAMAC_SHARE/libc/string.c:2
23
:[nonterm:stmt] warning: non-terminating loop
stack 1: strcpy :: 01_w_Defects/null_pointer.c:238 <-
null_pointer_015 :: 01_w_Defects/null_pointer.c:430 <-
null_pointer_main :: 01_w_Defects/main.c:309 <-
...
...
@@ -15,7 +15,7 @@ stack 3: strcpy :: 01_w_Defects/uninit_var.c:145 <-
uninit_var_main :: 01_w_Defects/main.c:464 <-
main :: fc_stubs.c:21 <-
eva_main
FRAMAC_SHARE/libc/string.c:2
07
:[nonterm:stmt] warning: non-terminating statement
FRAMAC_SHARE/libc/string.c:2
23
:[nonterm:stmt] warning: non-terminating statement
stack 1: strcpy :: 01_w_Defects/uninit_pointer.c:439 <-
uninit_pointer_016 :: 01_w_Defects/uninit_pointer.c:531 <-
uninit_pointer_main :: 01_w_Defects/main.c:458 <-
...
...
@@ -27,7 +27,7 @@ stack 2: strcpy :: 01_w_Defects/uninit_var.c:145 <-
uninit_var_main :: 01_w_Defects/main.c:464 <-
main :: fc_stubs.c:21 <-