Commit 1d909dd1 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

fix oracles after synchronization

parent 6b4aaead
Pipeline #37504 failed with stage
in 90 minutes and 2 seconds
...@@ -856,7 +856,7 @@ FRAMAC_SHARE/libc string.h 173 strchr precondition Unknown valid_string_s: valid ...@@ -856,7 +856,7 @@ FRAMAC_SHARE/libc string.h 173 strchr precondition Unknown valid_string_s: valid
FRAMAC_SHARE/libc unistd.h 775 chown precondition Unknown valid_string_path: valid_read_string(path) FRAMAC_SHARE/libc unistd.h 775 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1124 unlink precondition Unknown valid_string_path: valid_read_string(path) FRAMAC_SHARE/libc unistd.h 1124 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing; FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from \nothing; FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from *(__x0 + (0 ..)), __x1;
FRAMAC_SHARE/libc/sys stat.h 87 stat precondition Unknown valid_pathname: valid_read_string(pathname) FRAMAC_SHARE/libc/sys stat.h 87 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 test/unit ntp_core.c 179 send_response precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
test/unit ntp_core.c 186 send_response precondition of __FC_assert Unknown nonnull_c: c ≢ 0 test/unit ntp_core.c 186 send_response precondition of __FC_assert Unknown nonnull_c: c ≢ 0
......
...@@ -159,6 +159,9 @@ directory file line function property kind status property ...@@ -159,6 +159,9 @@ directory file line function property kind status property
. gzip.c 896 create_outfile precondition of fprintf_va_27 Unknown valid_read_string(param0) . gzip.c 896 create_outfile precondition of fprintf_va_27 Unknown valid_read_string(param0)
. gzip.c 897 create_outfile precondition of perror Unknown valid_string_s: valid_read_string(s) . gzip.c 897 create_outfile precondition of perror Unknown valid_string_s: valid_read_string(s)
. gzip.c 899 create_outfile precondition of unlink Unknown valid_string_path: valid_read_string(path) . gzip.c 899 create_outfile precondition of unlink Unknown valid_string_path: valid_read_string(path)
. gzip.c 907 create_outfile precondition of fprintf_va_28 Unknown valid_read_string(param0)
. gzip.c 907 create_outfile precondition of fprintf_va_28 Unknown valid_read_string(param1)
. gzip.c 912 create_outfile precondition of unlink Unknown valid_string_path: valid_read_string(path)
. gzip.c 933 do_stat precondition of lstat Unknown valid_path: valid_read_string(path) . gzip.c 933 do_stat precondition of lstat Unknown valid_path: valid_read_string(path)
. gzip.c 936 do_stat precondition of stat Unknown valid_pathname: valid_read_string(pathname) . gzip.c 936 do_stat precondition of stat Unknown valid_pathname: valid_read_string(pathname)
. gzip.c 964 get_suffix precondition of strcmp Unknown valid_string_s1: valid_read_string(s1) . gzip.c 964 get_suffix precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
...@@ -257,6 +260,7 @@ directory file line function property kind status property ...@@ -257,6 +260,7 @@ directory file line function property kind status property
. gzip.c 1402 do_list signed_overflow Unknown bytes_in - header_bytes ≤ 2147483647 . gzip.c 1402 do_list signed_overflow Unknown bytes_in - header_bytes ≤ 2147483647
. gzip.c 1403 do_list precondition of printf_va_8 Unknown valid_read_string(param0) . gzip.c 1403 do_list precondition of printf_va_8 Unknown valid_read_string(param0)
. gzip.c 1413 same_file initialization Unknown \initialized(&stat1->st_ino) . gzip.c 1413 same_file initialization Unknown \initialized(&stat1->st_ino)
. gzip.c 1414 same_file initialization Unknown \initialized(&stat1->st_dev)
. gzip.c 1436 name_too_long precondition of strlen Unknown valid_string_s: valid_read_string(s) . gzip.c 1436 name_too_long precondition of strlen Unknown valid_string_s: valid_read_string(s)
. gzip.c 1437 name_too_long mem_access Unknown \valid_read(name + (int)(s - 1)) . gzip.c 1437 name_too_long mem_access Unknown \valid_read(name + (int)(s - 1))
. gzip.c 1437 name_too_long signed_overflow Unknown -2147483648 ≤ s - 1 . gzip.c 1437 name_too_long signed_overflow Unknown -2147483648 ≤ s - 1
...@@ -576,6 +580,8 @@ FRAMAC_SHARE/libc stdio.h 207 fprintf_va_22 precondition Unknown valid_read_stri ...@@ -576,6 +580,8 @@ FRAMAC_SHARE/libc stdio.h 207 fprintf_va_22 precondition Unknown valid_read_stri
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_23 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 207 fprintf_va_23 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_25 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 207 fprintf_va_25 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_27 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 207 fprintf_va_27 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_28 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_28 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_29 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 207 fprintf_va_29 precondition Unknown valid_read_string(param0)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_29 precondition Unknown valid_read_string(param1) FRAMAC_SHARE/libc stdio.h 207 fprintf_va_29 precondition Unknown valid_read_string(param1)
FRAMAC_SHARE/libc stdio.h 207 fprintf_va_30 precondition Unknown valid_read_string(param0) FRAMAC_SHARE/libc stdio.h 207 fprintf_va_30 precondition Unknown valid_read_string(param0)
...@@ -677,8 +683,9 @@ FRAMAC_SHARE/libc unistd.h 1124 unlink precondition Unknown valid_string_path: v ...@@ -677,8 +683,9 @@ FRAMAC_SHARE/libc unistd.h 1124 unlink precondition Unknown valid_string_path: v
FRAMAC_SHARE/libc unistd.h 1140 write precondition Unknown valid_fd: 0 ≤ fd < 1024 FRAMAC_SHARE/libc unistd.h 1140 write precondition Unknown valid_fd: 0 ≤ fd < 1024
FRAMAC_SHARE/libc unistd.h 1141 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1)) FRAMAC_SHARE/libc unistd.h 1141 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing; FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from \nothing; FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from *(__x0 + (0 ..)), __x1;
FRAMAC_SHARE/libc/sys stat.h 35 fstat assigns clause Unknown assigns \nothing; FRAMAC_SHARE/libc/sys stat.h 35 fstat assigns clause Unknown assigns \result, *__x1;
FRAMAC_SHARE/libc/sys stat.h 35 fstat from clause Unknown assigns \result \from \nothing; FRAMAC_SHARE/libc/sys stat.h 35 fstat from clause Unknown assigns *__x1 \from *__x1, __x0;
FRAMAC_SHARE/libc/sys stat.h 35 fstat from clause Unknown assigns \result \from *__x1, __x0;
FRAMAC_SHARE/libc/sys stat.h 43 lstat precondition Unknown valid_path: valid_read_string(path) FRAMAC_SHARE/libc/sys stat.h 43 lstat precondition Unknown valid_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 87 stat precondition Unknown valid_pathname: valid_read_string(pathname) FRAMAC_SHARE/libc/sys stat.h 87 stat precondition Unknown valid_pathname: valid_read_string(pathname)
...@@ -13,7 +13,7 @@ Function flush_block calls set_file_type (at trees.c:864) ...@@ -13,7 +13,7 @@ Function flush_block calls set_file_type (at trees.c:864)
Function main references lzw (at gzip.c:573) Function main references lzw (at gzip.c:573)
[metrics] Statements analyzed by Eva [metrics] Statements analyzed by Eva
-------------------------- --------------------------
4844 stmts in analyzed functions, 4280 stmts analyzed (88.4%) 4844 stmts in analyzed functions, 4292 stmts analyzed (88.6%)
bi_init: 6 stmts out of 6 (100.0%) bi_init: 6 stmts out of 6 (100.0%)
bi_reverse: 11 stmts out of 11 (100.0%) bi_reverse: 11 stmts out of 11 (100.0%)
bi_windup: 36 stmts out of 36 (100.0%) bi_windup: 36 stmts out of 36 (100.0%)
...@@ -25,6 +25,7 @@ clear_bufs: 8 stmts out of 8 (100.0%) ...@@ -25,6 +25,7 @@ clear_bufs: 8 stmts out of 8 (100.0%)
compress_block: 41 stmts out of 41 (100.0%) compress_block: 41 stmts out of 41 (100.0%)
copy_block: 68 stmts out of 68 (100.0%) copy_block: 68 stmts out of 68 (100.0%)
copy_stat: 22 stmts out of 22 (100.0%) copy_stat: 22 stmts out of 22 (100.0%)
create_outfile: 49 stmts out of 49 (100.0%)
ct_init: 114 stmts out of 114 (100.0%) ct_init: 114 stmts out of 114 (100.0%)
ct_tally: 51 stmts out of 51 (100.0%) ct_tally: 51 stmts out of 51 (100.0%)
decode: 50 stmts out of 50 (100.0%) decode: 50 stmts out of 50 (100.0%)
...@@ -98,7 +99,6 @@ inflate: 22 stmts out of 26 (84.6%) ...@@ -98,7 +99,6 @@ inflate: 22 stmts out of 26 (84.6%)
basename: 5 stmts out of 6 (83.3%) basename: 5 stmts out of 6 (83.3%)
read_error: 5 stmts out of 6 (83.3%) read_error: 5 stmts out of 6 (83.3%)
abort_gzip: 4 stmts out of 5 (80.0%) abort_gzip: 4 stmts out of 5 (80.0%)
create_outfile: 37 stmts out of 49 (75.5%)
write_error: 3 stmts out of 4 (75.0%) write_error: 3 stmts out of 4 (75.0%)
error: 2 stmts out of 3 (66.7%) error: 2 stmts out of 3 (66.7%)
huft_free: 6 stmts out of 12 (50.0%) huft_free: 6 stmts out of 12 (50.0%)
......
gzip.c:602:[nonterm:unreachable] warning: unreachable return gzip.c:602:[nonterm:unreachable] warning: unreachable return
gzip.c:1413:[nonterm:stmt] warning: non-terminating statement
stack: same_file :: gzip.c:1443 <-
name_too_long :: gzip.c:903 <-
create_outfile :: gzip.c:799 <-
treat_file :: gzip.c:593 <-
main :: fc_stubs.c:21 <-
eva_main
gzip.c:1747:[nonterm:unreachable] warning: unreachable return gzip.c:1747:[nonterm:unreachable] warning: unreachable return
inflate.c:412:[nonterm:stmt] warning: non-terminating statement inflate.c:412:[nonterm:stmt] warning: non-terminating statement
stack 1: huft_build :: inflate.c:763 <- stack 1: huft_build :: inflate.c:763 <-
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment