Skip to content
Snippets Groups Projects
Commit 9a45d44a authored by Andre Maroneze's avatar Andre Maroneze
Browse files

synchronize with frama-c master

parent e9ada7fe
No related branches found
No related tags found
1 merge request!62synchronize with frama-c master
Pipeline #81895 passed
Stage: test
    Hide whitespace changes
    Inline Side-by-side
    Showing
    with 21 additions and 44 deletions
    2048/.frama-c/2048.eva/alarms.csv
    + 5
    − 5
    View file @ 9a45d44a
    ...@@ -11,8 +11,8 @@ directory file line function property kind status property ...@@ -11,8 +11,8 @@ directory file line function property kind status property
    . 2048.c 249 addRandom initialization Unknown \initialized(&list[r][0]) . 2048.c 249 addRandom initialization Unknown \initialized(&list[r][0])
    . 2048.c 250 addRandom initialization Unknown \initialized(&list[r][1]) . 2048.c 250 addRandom initialization Unknown \initialized(&list[r][1])
    . 2048.c 287 setBufferedInput initialization Unknown \initialized(&new.c_lflag) . 2048.c 287 setBufferedInput initialization Unknown \initialized(&new.c_lflag)
    FRAMAC_SHARE/libc stdio.h 211 printf_va_12 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 248 printf_va_12 precondition Unknown valid_read_string(param0)
    FRAMAC_SHARE/libc stdio.h 211 printf_va_3 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 211 printf_va_7 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 211 printf_va_8 precondition Unknown valid_read_string(param2) FRAMAC_SHARE/libc stdio.h 248 printf_va_8 precondition Unknown valid_read_string(param2)
    FRAMAC_SHARE/libc string.h 158 strlen precondition Unknown valid_string_s: valid_read_string(s) FRAMAC_SHARE/libc string.h 174 strlen precondition Unknown valid_string_s: valid_read_string(s)
    2048/.frama-c/2048.parse/framac.ast
    + 1
    − 0
    View file @ 9a45d44a
    /* Generated by Frama-C */ /* Generated by Frama-C */
    #include "errno.h" #include "errno.h"
    #include "fcntl.h"
    #include "signal.h" #include "signal.h"
    #include "stdarg.h" #include "stdarg.h"
    #include "stddef.h" #include "stddef.h"
    ......
    basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
    + 1
    − 1
    View file @ 9a45d44a
    ...@@ -2,4 +2,4 @@ directory file line function property kind status property ...@@ -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(s1 + i)
    . cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + 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))) . cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
    FRAMAC_SHARE/libc string.h 420 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src))) FRAMAC_SHARE/libc string.h 436 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
    basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
    + 1
    − 1
    View file @ 9a45d44a
    ...@@ -2,4 +2,4 @@ directory file line function property kind status property ...@@ -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(s1 + i)
    . cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + 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))) . cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
    FRAMAC_SHARE/libc string.h 420 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src))) FRAMAC_SHARE/libc string.h 436 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
    basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
    + 1
    − 0
    View file @ 9a45d44a
    /* Generated by Frama-C */ /* Generated by Frama-C */
    #include "errno.h" #include "errno.h"
    #include "fcntl.h"
    #include "stdarg.h" #include "stdarg.h"
    #include "stddef.h" #include "stddef.h"
    #include "stdio.h" #include "stdio.h"
    ......
    basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
    + 1
    − 0
    View file @ 9a45d44a
    /* Generated by Frama-C */ /* Generated by Frama-C */
    #include "errno.h" #include "errno.h"
    #include "fcntl.h"
    #include "stdarg.h" #include "stdarg.h"
    #include "stddef.h" #include "stddef.h"
    #include "stdio.h" #include "stdio.h"
    ......
    c-testsuite/.frama-c/00186.eva/alarms.csv
    + 1
    − 1
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . 00186.c 11 main precondition of printf_va_1 Unknown valid_read_string(param0) . 00186.c 11 main precondition of printf_va_1 Unknown valid_read_string(param0)
    FRAMAC_SHARE/libc stdio.h 211 printf_va_1 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 248 printf_va_1 precondition Unknown valid_read_string(param0)
    c-testsuite/.frama-c/00187.eva/alarms.csv
    + 7
    − 7
    View file @ 9a45d44a
    ...@@ -6,10 +6,10 @@ directory file line function property kind status property ...@@ -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 33 main precondition of getc Unknown valid_stream: \valid(stream)
    . 00187.c 44 main precondition of fgets 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) . 00187.c 45 main precondition of printf_va_5 Unknown valid_read_string(param0)
    FRAMAC_SHARE/libc stdio.h 211 printf_va_2 precondition 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 211 printf_va_5 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 260 fgetc precondition Unknown valid_stream: \valid(stream) FRAMAC_SHARE/libc stdio.h 297 fgetc precondition Unknown valid_stream: \valid(stream)
    FRAMAC_SHARE/libc stdio.h 268 fgets precondition Unknown valid_stream: \valid(stream) FRAMAC_SHARE/libc stdio.h 305 fgets precondition Unknown valid_stream: \valid(stream)
    FRAMAC_SHARE/libc stdio.h 298 getc precondition Unknown valid_stream: \valid(stream) FRAMAC_SHARE/libc stdio.h 335 getc precondition Unknown valid_stream: \valid(stream)
    FRAMAC_SHARE/libc stdio.h 354 fread precondition Unknown valid_stream: \valid(stream) FRAMAC_SHARE/libc stdio.h 391 fread precondition Unknown valid_stream: \valid(stream)
    FRAMAC_SHARE/libc stdio.h 367 fwrite precondition Unknown valid_stream: \valid(stream) FRAMAC_SHARE/libc stdio.h 404 fwrite precondition Unknown valid_stream: \valid(stream)
    c-testsuite/.frama-c/00189.eva/alarms.csv
    + 3
    − 3
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    FRAMAC_SHARE/libc stdio.h 207 fprintf assigns clause Unknown assigns \result, *stream; FRAMAC_SHARE/libc stdio.h 244 fprintf assigns clause Unknown assigns \result, *stream;
    FRAMAC_SHARE/libc stdio.h 207 fprintf from clause Unknown assigns *stream \from *stream, *(format + (0 ..)); FRAMAC_SHARE/libc stdio.h 244 fprintf from clause Unknown assigns *stream \from *stream, *(format + (0 ..));
    FRAMAC_SHARE/libc stdio.h 207 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..)); FRAMAC_SHARE/libc stdio.h 244 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..));
    cerberus/.frama-c/pointer_offset_from_subtraction_1_auto.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . pointer_offset_from_subtraction_1_auto.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . pointer_offset_from_subtraction_1_auto.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . pointer_offset_from_subtraction_1_auto.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux . pointer_offset_from_subtraction_1_auto.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux
    . pointer_offset_from_subtraction_1_auto.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647 . pointer_offset_from_subtraction_1_auto.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647
    . pointer_offset_from_subtraction_1_auto.c 8 main signed_overflow Unknown -2147483648 ≤ ux + offset . pointer_offset_from_subtraction_1_auto.c 8 main signed_overflow Unknown -2147483648 ≤ ux + offset
    ......
    cerberus/.frama-c/pointer_offset_from_subtraction_1_global.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . pointer_offset_from_subtraction_1_global.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . pointer_offset_from_subtraction_1_global.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . pointer_offset_from_subtraction_1_global.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux . pointer_offset_from_subtraction_1_global.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux
    . pointer_offset_from_subtraction_1_global.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647 . pointer_offset_from_subtraction_1_global.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647
    . pointer_offset_from_subtraction_1_global.c 8 main signed_overflow Unknown -2147483648 ≤ ux + offset . pointer_offset_from_subtraction_1_global.c 8 main signed_overflow Unknown -2147483648 ≤ ux + offset
    ......
    cerberus/.frama-c/pointer_offset_from_subtraction_2_auto.eva/alarms.csv
    + 0
    − 4
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . pointer_offset_from_subtraction_2_auto.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . pointer_offset_from_subtraction_2_auto.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . pointer_offset_from_subtraction_2_auto.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux . pointer_offset_from_subtraction_2_auto.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux
    . pointer_offset_from_subtraction_2_auto.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647 . pointer_offset_from_subtraction_2_auto.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647
    . pointer_offset_from_subtraction_2_auto.c 6 main pointer_downcast Unknown (unsigned int)(&z) ≤ 2147483647
    . pointer_offset_from_subtraction_2_auto.c 7 main pointer_downcast Unknown (unsigned int)(&w) ≤ 2147483647
    . pointer_offset_from_subtraction_2_auto.c 8 main signed_overflow Unknown -2147483648 ≤ uw - uz . pointer_offset_from_subtraction_2_auto.c 8 main signed_overflow Unknown -2147483648 ≤ uw - uz
    . pointer_offset_from_subtraction_2_auto.c 8 main signed_overflow Unknown uw - uz ≤ 2147483647 . pointer_offset_from_subtraction_2_auto.c 8 main signed_overflow Unknown uw - uz ≤ 2147483647
    . pointer_offset_from_subtraction_2_auto.c 13 main precondition of __FC_assert Unknown nonnull_c: c ≢ 0 . pointer_offset_from_subtraction_2_auto.c 13 main precondition of __FC_assert Unknown nonnull_c: c ≢ 0
    ......
    cerberus/.frama-c/pointer_offset_from_subtraction_2_global.eva/alarms.csv
    + 0
    − 4
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . pointer_offset_from_subtraction_2_global.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . pointer_offset_from_subtraction_2_global.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . pointer_offset_from_subtraction_2_global.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux . pointer_offset_from_subtraction_2_global.c 5 main signed_overflow Unknown -2147483648 ≤ uy - ux
    . pointer_offset_from_subtraction_2_global.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647 . pointer_offset_from_subtraction_2_global.c 5 main signed_overflow Unknown uy - ux ≤ 2147483647
    . pointer_offset_from_subtraction_2_global.c 6 main pointer_downcast Unknown (unsigned int)(&z) ≤ 2147483647
    . pointer_offset_from_subtraction_2_global.c 7 main pointer_downcast Unknown (unsigned int)(&w) ≤ 2147483647
    . pointer_offset_from_subtraction_2_global.c 8 main signed_overflow Unknown -2147483648 ≤ uw - uz . pointer_offset_from_subtraction_2_global.c 8 main signed_overflow Unknown -2147483648 ≤ uw - uz
    . pointer_offset_from_subtraction_2_global.c 8 main signed_overflow Unknown uw - uz ≤ 2147483647 . pointer_offset_from_subtraction_2_global.c 8 main signed_overflow Unknown uw - uz ≤ 2147483647
    . pointer_offset_from_subtraction_2_global.c 13 main precondition of __FC_assert Unknown nonnull_c: c ≢ 0 . pointer_offset_from_subtraction_2_global.c 13 main precondition of __FC_assert Unknown nonnull_c: c ≢ 0
    ......
    cerberus/.frama-c/provenance_basic_mixed_auto.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_auto.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_auto.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_auto.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_auto.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_auto.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_auto.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_auto.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_auto.c 12 main mem_access Invalid or unreachable \valid(p)
    cerberus/.frama-c/provenance_basic_mixed_auto_offset+4.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_auto_offset+4.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_auto_offset+4.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_auto_offset+4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_auto_offset+4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_auto_offset+4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_auto_offset+4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_auto_offset+4.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_auto_offset+4.c 12 main mem_access Invalid or unreachable \valid(p)
    cerberus/.frama-c/provenance_basic_mixed_auto_offset-4.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_auto_offset-4.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_auto_offset-4.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_auto_offset-4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_auto_offset-4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_auto_offset-4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_auto_offset-4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_auto_offset-4.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_auto_offset-4.c 12 main mem_access Invalid or unreachable \valid(p)
    cerberus/.frama-c/provenance_basic_mixed_auto_offset-64.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_auto_offset-64.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_auto_offset-64.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_auto_offset-64.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_auto_offset-64.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_auto_offset-64.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_auto_offset-64.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_auto_offset-64.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_auto_offset-64.c 12 main mem_access Invalid or unreachable \valid(p)
    cerberus/.frama-c/provenance_basic_mixed_global_offset+4.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_global_offset+4.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_global_offset+4.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_global_offset+4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_global_offset+4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_global_offset+4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_global_offset+4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_global_offset+4.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_global_offset+4.c 12 main mem_access Invalid or unreachable \valid(p)
    cerberus/.frama-c/provenance_basic_mixed_global_offset-4.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_global_offset-4.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_global_offset-4.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_global_offset-4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_global_offset-4.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_global_offset-4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_global_offset-4.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_global_offset-4.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_global_offset-4.c 12 main mem_access Invalid or unreachable \valid(p)
    cerberus/.frama-c/provenance_basic_mixed_global_offset-64.eva/alarms.csv
    + 0
    − 2
    View file @ 9a45d44a
    directory file line function property kind status property directory file line function property kind status property
    . provenance_basic_mixed_global_offset-64.c 3 main pointer_downcast Unknown (unsigned int)(&x) ≤ 2147483647
    . provenance_basic_mixed_global_offset-64.c 4 main pointer_downcast Unknown (unsigned int)(&y) ≤ 2147483647
    . provenance_basic_mixed_global_offset-64.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset . provenance_basic_mixed_global_offset-64.c 10 main signed_overflow Unknown -2147483648 ≤ ux + offset
    . provenance_basic_mixed_global_offset-64.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647 . provenance_basic_mixed_global_offset-64.c 10 main signed_overflow Unknown ux + offset ≤ 2147483647
    . provenance_basic_mixed_global_offset-64.c 12 main mem_access Invalid or unreachable \valid(p) . provenance_basic_mixed_global_offset-64.c 12 main mem_access Invalid or unreachable \valid(p)
    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