Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • pub/open-source-case-studies
  • contra-bit/open-source-case-studies
2 results
Show changes
Commits on Source (2)
Hide whitespace changes
Inline Side-by-side
Showing
with 184 additions and 171 deletions
2048/.frama-c/2048.eva/alarms.csv
View file @ 5336d3c1
......@@ -11,8 +11,8 @@ directory file line function property kind status property
. 2048.c 249 addRandom initialization Unknown \initialized(&list[r][0])
. 2048.c 250 addRandom initialization Unknown \initialized(&list[r][1])
. 2048.c 287 setBufferedInput initialization Unknown \initialized(&new.c_lflag)
FRAMAC_SHARE/libc stdio.h 248 printf_va_12 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_7 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_8 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 253 printf_va_12 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 253 printf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 253 printf_va_7 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 253 printf_va_8 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc string.h 174 strlen precondition Unknown valid_string_s: valid_read_string(s)
c-testsuite/.frama-c/00186.eva/alarms.csv
View file @ 5336d3c1
directory file line function property kind status property
. 00186.c 11 main precondition of printf_va_1 Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_1 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 253 printf_va_1 precondition Unknown valid_read_string(param0)
c-testsuite/.frama-c/00187.eva/alarms.csv
View file @ 5336d3c1
......@@ -6,10 +6,10 @@ directory file line function property kind status property
. 00187.c 33 main precondition of getc Unknown valid_stream: \valid(stream)
. 00187.c 44 main precondition of fgets Unknown valid_stream: \valid(stream)
. 00187.c 45 main precondition of printf_va_5 Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_5 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 297 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 305 fgets precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 335 getc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 391 fread precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 404 fwrite precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 253 printf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 253 printf_va_5 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 302 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 310 fgets precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 340 getc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 396 fread precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 409 fwrite precondition Unknown valid_stream: \valid(stream)
c-testsuite/.frama-c/00189.eva/alarms.csv
View file @ 5336d3c1
directory file line function property kind status property
FRAMAC_SHARE/libc stdio.h 244 fprintf assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 244 fprintf from clause Unknown assigns *stream \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 244 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 249 fprintf assigns clause Unknown assigns \result, *stream;
FRAMAC_SHARE/libc stdio.h 249 fprintf from clause Unknown assigns *stream \from *stream, *(format + (0 ..));
FRAMAC_SHARE/libc stdio.h 249 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..));
cerberus/.frama-c/provenance_via_io_auto.eva/alarms.csv
View file @ 5336d3c1
directory file line function property kind status property
. provenance_via_io_auto.c 11 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_auto.c 19 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 475 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 480 rewind precondition Unknown valid_stream: \valid(stream)
cerberus/.frama-c/provenance_via_io_bytewise_global.eva/alarms.csv
View file @ 5336d3c1
......@@ -2,4 +2,4 @@ directory file line function property kind status property
. provenance_via_io_bytewise_global.c 8 main precondition of fwrite Unknown valid_stream: \valid(stream)
. provenance_via_io_bytewise_global.c 14 main initialization Unknown \initialized(&r)
. provenance_via_io_bytewise_global.c 16 main mem_access Invalid or unreachable \valid(r)
FRAMAC_SHARE/libc stdio.h 404 fwrite precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 409 fwrite precondition Unknown valid_stream: \valid(stream)
cerberus/.frama-c/provenance_via_io_global.eva/alarms.csv
View file @ 5336d3c1
directory file line function property kind status property
. provenance_via_io_global.c 10 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_global.c 18 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 475 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 480 rewind precondition Unknown valid_stream: \valid(stream)
cerberus/.frama-c/provenance_via_io_percentp_global.eva/alarms.csv
View file @ 5336d3c1
directory file line function property kind status property
. provenance_via_io_percentp_global.c 9 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_percentp_global.c 16 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 475 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 480 rewind precondition Unknown valid_stream: \valid(stream)
cerberus/.frama-c/provenance_via_io_uintptr_t_global.eva/alarms.csv
View file @ 5336d3c1
directory file line function property kind status property
. provenance_via_io_uintptr_t_global.c 10 main precondition of rewind Unknown valid_stream: \valid(stream)
. provenance_via_io_uintptr_t_global.c 18 main mem_access Unknown \valid(r)
FRAMAC_SHARE/libc stdio.h 475 rewind precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 480 rewind precondition Unknown valid_stream: \valid(stream)
chrony/.frama-c/chrony-ntp-core.eva/alarms.csv
View file @ 5336d3c1
......@@ -641,82 +641,82 @@ FRAMAC_SHARE/libc netdb.c 122 gethostbyname mem_access Unknown \valid_read(cp)
FRAMAC_SHARE/libc netdb.c 125 gethostbyname precondition of inet_addr Unknown valid_arg: valid_read_string(arg)
FRAMAC_SHARE/libc netdb.c 151 gethostbyname precondition of inet_addr Unknown valid_arg: valid_read_string(arg)
FRAMAC_SHARE/libc stdio.c 176 fgets mem_access Unknown \valid(s + i)
FRAMAC_SHARE/libc stdio.h 85 rename precondition Unknown valid_old_name: valid_read_string(old_name)
FRAMAC_SHARE/libc stdio.h 86 rename precondition Unknown valid_new_name: valid_read_string(new_name)
FRAMAC_SHARE/libc stdio.h 187 fopen precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_4 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 250 snprintf_va_10 precondition Unknown \valid(s + (0 .. n - 1)) ∨ \valid(s + (0 .. format_length(format) - 1))
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_1 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_10 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_11 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_12 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_13 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_14 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_15 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_16 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_17 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_18 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_19 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_2 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_20 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_21 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_22 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_23 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_24 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_25 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_26 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_27 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_28 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_29 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_3 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_30 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_31 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_32 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_33 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_34 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_35 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_36 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_37 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_38 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_39 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_4 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_40 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_41 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_42 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_43 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_44 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_45 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_46 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_47 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_48 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_49 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_5 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_50 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_51 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_52 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_53 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_54 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_54 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_55 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_55 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_56 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_56 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_57 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_57 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_58 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_58 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_59 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_59 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_6 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_63 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_7 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_8 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 254 sscanf_va_9 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 327 fputs precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 390 fread precondition Unknown valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
FRAMAC_SHARE/libc stdio.h 597 popen precondition Unknown valid_command: valid_read_string(command)
FRAMAC_SHARE/libc stdio.h 612 pclose precondition Unknown open_pipe: is_open_pipe(stream)
FRAMAC_SHARE/libc stdio.h 90 rename precondition Unknown valid_old_name: valid_read_string(old_name)
FRAMAC_SHARE/libc stdio.h 91 rename precondition Unknown valid_new_name: valid_read_string(new_name)
FRAMAC_SHARE/libc stdio.h 192 fopen precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_4 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 255 snprintf_va_10 precondition Unknown \valid(s + (0 .. n - 1)) ∨ \valid(s + (0 .. format_length(format) - 1))
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_1 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_10 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_11 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_12 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_13 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_14 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_15 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_16 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_17 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_18 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_19 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_2 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_20 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_21 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_22 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_23 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_24 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_25 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_26 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_27 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_28 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_29 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_3 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_30 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_31 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_32 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_33 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_34 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_35 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_36 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_37 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_38 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_39 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_4 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_40 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_41 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_42 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_43 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_44 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_45 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_46 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_47 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_48 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_49 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_5 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_50 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_51 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_52 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_53 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_54 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_54 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_55 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_55 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_56 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_56 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_57 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_57 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_58 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_58 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_59 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_59 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_6 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_63 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_7 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_8 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 259 sscanf_va_9 precondition Unknown valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 332 fputs precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 395 fread precondition Unknown valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
FRAMAC_SHARE/libc stdio.h 630 popen precondition Unknown valid_command: valid_read_string(command)
FRAMAC_SHARE/libc stdio.h 645 pclose precondition Unknown open_pipe: is_open_pipe(stream)
FRAMAC_SHARE/libc stdlib.h 438 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc string.c 146 strcmp initialization Unknown \initialized(s1 + i)
FRAMAC_SHARE/libc string.c 146 strcmp mem_access Unknown \valid_read(s1 + i)
......@@ -751,8 +751,8 @@ FRAMAC_SHARE/libc string.h 154 memmove precondition Unknown valid_src: valid_rea
FRAMAC_SHARE/libc string.h 164 memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc string.h 174 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 209 strchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 797 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1173 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 804 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1307 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 38 chmod precondition Unknown valid_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 165 stat precondition Unknown valid_pathname: valid_read_string(pathname)
test/unit ntp_core.c 179 send_response precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
......
chrony/.frama-c/chrony-ntp-core.eva/warnings.log
View file @ 5336d3c1
......@@ -3457,6 +3457,8 @@ stack: strcpy :: reference.c:651 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
reference.c:657:[eva:garbled-mix:assigns] warning: The specification of function mktime has generated a garbled mix of addresses
for assigns clause *timeptr.
reference.c:659:[eva:alarm] warning: signed overflow. assert -9223372036854775808 ≤ t - when;
stack: get_tz_leap :: reference.c:248 <-
REF_Initialise :: test/unit/ntp_core.c:325 <-
......@@ -12718,6 +12720,9 @@ test/unit/test.c:72:[kernel:annot:missing-spec] warning: Neither code nor specif
__malloc_SRC_CreateNewInstance_l229_1;
__malloc_NCR_GetInstance_l520_2;
__malloc_SRC_CreateNewInstance_l229_2}
reference.c:657: misaligned read of addresses
(read in 2 statements, propagated through 2 statements)
garbled mix of &{S_tm_zone___fc_time_tm}
addrfilt.c:327: misaligned read of addresses
(read in 1 statement, propagated through 1 statement)
garbled mix of &{__malloc_open_node_l137; __malloc_w_open_node_l137_0;
......
chrony/.frama-c/chrony-ntp-core.parse/framac.ast
View file @ 5336d3c1
......@@ -26,11 +26,14 @@
#include "string.h"
#include "strings.h"
#include "stropts.h"
#include "sys/ipc.h"
#include "sys/resource.h"
#include "sys/select.h"
#include "sys/shm.h"
#include "sys/socket.h"
#include "sys/stat.h"
#include "sys/time.h"
#include "sys/timex.h"
#include "sys/types.h"
#include "sys/uio.h"
#include "sys/un.h"
......@@ -8880,7 +8883,7 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
local_addr.sock_fd = sock_fd;
if (hdr->msg_flags & 0x20) goto return_label;
if (hdr->msg_flags & 0x8) ;
cmsg = CMSG_FIRSTHDR(hdr);
cmsg = CMSG_FIRSTHDR((struct msghdr const *)hdr);
while (cmsg) {
if (cmsg->cmsg_level == 1)
if (cmsg->cmsg_type == 29) {
......@@ -8898,7 +8901,8 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
LCL_CookTime(& ts_0,& local_ts.ts,& local_ts.err);
local_ts.source = NTP_TS_KERNEL;
}
cmsg = CMSG_NXTHDR(hdr,cmsg);
cmsg = CMSG_NXTHDR((struct msghdr const *)hdr,
(struct cmsghdr const *)cmsg);
}
if (length < 48) goto return_label;
else
......
chrony/.frama-c/chrony-regress.parse/framac.ast
View file @ 5336d3c1
......@@ -26,11 +26,14 @@
#include "string.h"
#include "strings.h"
#include "stropts.h"
#include "sys/ipc.h"
#include "sys/resource.h"
#include "sys/select.h"
#include "sys/shm.h"
#include "sys/socket.h"
#include "sys/stat.h"
#include "sys/time.h"
#include "sys/timex.h"
#include "sys/types.h"
#include "sys/uio.h"
#include "sys/un.h"
......@@ -8694,7 +8697,7 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
local_addr.sock_fd = sock_fd;
if (hdr->msg_flags & 0x20) goto return_label;
if (hdr->msg_flags & 0x8) ;
cmsg = CMSG_FIRSTHDR(hdr);
cmsg = CMSG_FIRSTHDR((struct msghdr const *)hdr);
while (cmsg) {
if (cmsg->cmsg_level == 1)
if (cmsg->cmsg_type == 29) {
......@@ -8712,7 +8715,8 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
LCL_CookTime(& ts_0,& local_ts.ts,& local_ts.err);
local_ts.source = NTP_TS_KERNEL;
}
cmsg = CMSG_NXTHDR(hdr,cmsg);
cmsg = CMSG_NXTHDR((struct msghdr const *)hdr,
(struct cmsghdr const *)cmsg);
}
if (length < 48) goto return_label;
else
......
frama-c @ b587ccf0
Compare 5d71cbfe...b587ccf0
Subproject commit 5d71cbfe9b425c6775d305846edc91ea6933ce95
Subproject commit b587ccf098032a894300b4aa6206803173d26932
genann/.frama-c/genann.eva/alarms.csv
View file @ 5336d3c1
......@@ -72,5 +72,5 @@ directory file line function property kind status property
. test.c 270 main signed_overflow Unknown -2147483648 ≤ (int)(ltests - ts_6) - (int)(lfails - fs_6)
. test.c 271 main signed_overflow Unknown (int)(ltests - ts_7) - (int)(lfails - fs_7) ≤ 2147483647
. test.c 271 main signed_overflow Unknown -2147483648 ≤ (int)(ltests - ts_7) - (int)(lfails - fs_7)
FRAMAC_SHARE/libc stdio.h 157 fclose precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 246 fscanf_va_2 precondition Unknown \valid(param0)
FRAMAC_SHARE/libc stdio.h 162 fclose precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 251 fscanf_va_2 precondition Unknown \valid(param0)
gzip124/.frama-c/gzip124.eva/alarms.csv
View file @ 5336d3c1
......@@ -903,55 +903,55 @@ directory file line function property kind status property
. zip.c 111 file_read precondition of read Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc ctype.h 174 isupper precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc fcntl.h 162 __va_open_mode_t precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_1 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_1 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_21 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_26 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_27 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_28 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_30 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_30 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_31 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_33 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_36 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_37 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_38 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_38 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_39 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_4 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_4 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_40 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_41 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_42 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_43 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_44 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_45 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_46 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_47 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_48 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_48 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_49 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_5 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_5 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_6 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_6 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_60 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_61 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_62 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_63 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_64 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_66 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_67 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_68 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_7 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_71 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_8 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 248 printf_va_8 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 362 putc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 493 fileno precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 523 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_1 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_1 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_21 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_26 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_27 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_28 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_3 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_30 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_30 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_31 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_33 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_36 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_37 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_38 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_38 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_39 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_4 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_4 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_40 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_41 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_42 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_43 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_44 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_45 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_46 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_47 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_48 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_48 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_49 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_5 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_5 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_6 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_6 precondition Unknown valid_read_string(param2)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_60 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_61 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_62 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_63 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_64 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_66 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_67 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_68 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_7 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_71 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_8 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 253 printf_va_8 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 367 putc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 498 fileno precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 528 perror precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc stdlib.c 45 atoi initialization Unknown \initialized(up)
FRAMAC_SHARE/libc stdlib.c 45 atoi mem_access Unknown \valid_read(up)
FRAMAC_SHARE/libc stdlib.c 47 atoi initialization Unknown \initialized(up)
......@@ -981,14 +981,14 @@ FRAMAC_SHARE/libc string.h 436 strcpy precondition Unknown room_string: \valid(d
FRAMAC_SHARE/libc string.h 492 strcat precondition Unknown valid_string_src: valid_read_string(src)
FRAMAC_SHARE/libc string.h 493 strcat precondition Unknown valid_string_dest: valid_string(dest)
FRAMAC_SHARE/libc string.h 494 strcat precondition Unknown room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
FRAMAC_SHARE/libc unistd.h 797 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 805 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1005 lseek precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1044 read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1045 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1173 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1189 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1190 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 804 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 812 close precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1093 lseek precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1143 read precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1144 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc unistd.h 1307 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1326 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1327 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc/sys stat.h 38 chmod precondition Unknown valid_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 121 lstat precondition Unknown valid_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 165 stat precondition Unknown valid_pathname: valid_read_string(pathname)
hiredis/.frama-c/hiredis-format.eva/alarms.csv
View file @ 5336d3c1
......@@ -226,7 +226,7 @@ directory file line function property kind status property
. test.c 1005 main precondition of fprintf_va_2 Unknown valid_read_string(param0)
. test.c 1015 main precondition of access Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Unknown nonnull_c: c ≢ 0
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdlib.h 79 atoi precondition Unknown valid_nptr: valid_read_string(nptr)
FRAMAC_SHARE/libc stdlib.h 438 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdlib.h 455 realloc precondition Unknown freeable: ptr ≡ \null ∨ \freeable(ptr)
......
hiredis/.frama-c/hiredis-misc.eva/alarms.csv
View file @ 5336d3c1
......@@ -308,8 +308,8 @@ directory file line function property kind status property
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0
FRAMAC_SHARE/libc ctype.h 134 isprint precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc netdb.h 148 freeaddrinfo precondition Unknown addrinfo_valid: \valid(addrinfo)
FRAMAC_SHARE/libc stdio.h 244 fprintf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 250 snprintf_va_15 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 249 fprintf_va_2 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 255 snprintf_va_15 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdlib.h 79 atoi precondition Unknown valid_nptr: valid_read_string(nptr)
FRAMAC_SHARE/libc stdlib.h 99 strtod precondition Unknown valid_string_nptr: valid_read_string(nptr)
FRAMAC_SHARE/libc stdlib.h 438 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
......@@ -336,5 +336,5 @@ FRAMAC_SHARE/libc string.h 652 strerror_r from clause Unknown assigns *(strerrbu
FRAMAC_SHARE/libc string.h 652 strerror_r from clause Unknown assigns \result \from *(strerrbuf + (0 ..)), errnum, buflen;
FRAMAC_SHARE/libc strings.h 77 strncasecmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc unistd.h 733 access precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys socket.h 339 connect precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 545 setsockopt precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 346 connect precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 558 setsockopt precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
ioccc/.frama-c/2019_adamovsky_iocccsize_2018.eva/alarms.csv
View file @ 5336d3c1
......@@ -58,8 +58,8 @@ directory file line function property kind status property
2019/adamovsky iocccsize_2018.c 556 count signed_overflow Unknown bcount + xbcount ≤ 2147483647
FRAMAC_SHARE/libc ctype.h 41 isalnum precondition Unknown c_uchar_or_eof_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 stdio.h 297 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 320 fputc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 382 ungetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 302 fgetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 325 fputc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc stdio.h 387 ungetc precondition Unknown valid_stream: \valid(stream)
FRAMAC_SHARE/libc string.h 194 strncmp precondition Unknown valid_string_s1: valid_read_nstring(s1, n)
FRAMAC_SHARE/libc string.h 254 strspn precondition Unknown valid_string_s: valid_read_string(s)
ioccc/.frama-c/2019_adamovsky_prog.eva/alarms.csv
View file @ 5336d3c1
......@@ -21,4 +21,4 @@ directory file line function property kind status property
2019/adamovsky prog.c 24 main precondition of fopen Unknown valid_filename: valid_read_string(filename)
2019/adamovsky prog.c 25 main initialization Unknown \initialized(&(f + 3)->a)
2019/adamovsky prog.c 38 rY1 mem_access Invalid or unreachable \valid_read(&(x + 3)->a)
FRAMAC_SHARE/libc stdio.h 187 fopen precondition Unknown valid_filename: valid_read_string(filename)
FRAMAC_SHARE/libc stdio.h 192 fopen precondition Unknown valid_filename: valid_read_string(filename)