Commit 8d78af8e authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

sync with frama-c master

parent 44f84113
Pipeline #34077 passed with stage
in 50 minutes and 39 seconds
......@@ -158,7 +158,7 @@ memory_zero_alloc_07_cross_file_good.eva/alarms.csv (good): ok
memory_zero_alloc_08_loop_for_good.eva/alarms.csv (good): ok
memory_zero_alloc_09_loop_for_complex_good.eva/alarms.csv (good): ok
memory_zero_alloc_10_loop_while_continue_good.eva/alarms.csv (good): ok
memory_zero_alloc_11_loop_while_do_continue_good.eva/alarms.csv (good): imprecise
memory_zero_alloc_11_loop_while_do_continue_good.eva/alarms.csv (good): ok
memory_zero_alloc_12_loop_for_array_branching_good.eva/alarms.csv (good): ok
memory_zero_alloc_13_loop_for_pointer_arithmetic_good.eva/alarms.csv (good): imprecise
memory_zero_alloc_17_complex_function_pointers_good.eva/alarms.csv (good): ok
......
pointer_copy_user_ctrlflow_bytewise.c:260:[kernel] warning: Body of function control_flow_copy falls-through. Adding a return statement
pointer_copy_user_ctrlflow_bytewise.c:260:[kernel:CERT:MSC:37] warning: Body of function control_flow_copy falls-through. Adding a return statement
pointer_copy_user_ctrlflow_bytewise_abbrev.c:8:[kernel] warning: Body of function control_flow_copy falls-through. Adding a return statement
pointer_copy_user_ctrlflow_bytewise_abbrev.c:8:[kernel:CERT:MSC:37] warning: Body of function control_flow_copy falls-through. Adding a return statement
......@@ -399,8 +399,6 @@ directory file line function property kind status property
. ntp_core.c 751 adjust_poll signed_overflow Unknown -2147483648 ≤ inst->local_poll + (int)\sub_double(inst->poll_score, (double)1.0)
. ntp_core.c 751 adjust_poll float_to_int Unknown -2147483649 < inst->poll_score - 1.0
. ntp_core.c 751 adjust_poll is_nan_or_infinite Unknown \is_finite(\sub_double(inst->poll_score, (double)1.0))
. ntp_core.c 784 get_poll_adj precondition of log Unknown arg_positive: x > 0
. ntp_core.c 784 get_poll_adj precondition of log Unknown finite_arg: \is_finite(x)
. ntp_core.c 859 get_transmit_delay signed_overflow Unknown inst->remote_stratum - tmp ≤ 2147483647
. ntp_core.c 1037 transmit_packet mem_access Unknown \valid_read(remote_ntp_rx)
. ntp_core.c 1078 transmit_packet signed_overflow Unknown -9223372036854775808 ≤ local_transmit.tv_nsec + (long)tmp_10
......@@ -414,17 +412,14 @@ directory file line function property kind status property
. ntp_core.c 1447 check_delay_dev_ratio initialization Unknown \initialized(&std_dev)
. ntp_core.c 1449 check_delay_dev_ratio initialization Unknown \initialized(&min_delay)
. ntp_core.c 1454 check_delay_dev_ratio initialization Unknown \initialized(&predicted_offset)
. ntp_core.c 1459 check_delay_dev_ratio precondition of fabs Unknown finite_arg: \is_finite(x)
. ntp_core.c 1489 process_sample signed_overflow Unknown (int)(8 / 2) * filtered_samples ≤ 2147483647
. ntp_core.c 1489 process_sample signed_overflow Unknown -2147483648 ≤ (int)(8 / 2) * filtered_samples
. ntp_core.c 1504 process_sample initialization Unknown \initialized(&sample->offset)
. ntp_core.c 1504 process_sample precondition of fabs Unknown finite_arg: \is_finite(x)
. ntp_core.c 1509 process_sample initialization Unknown \initialized(&sample->peer_delay)
. ntp_core.c 1509 process_sample initialization Unknown \initialized(&sample->peer_dispersion)
. ntp_core.c 1883 receive_packet precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. ntp_io.c 161 prepare_socket initialization Unknown \initialized(&bind_address.addr.in4)
. reference.c 202 REF_Initialise precondition of fopen Unknown valid_filename: valid_read_string(filename)
. reference.c 232 REF_Initialise precondition of fabs Unknown finite_arg: \is_finite(x)
. reference.c 265 REF_Initialise signed_overflow Unknown -2147483648 ≤ fb_drift_max_0 - fb_drift_min_0
. reference.c 266 REF_Initialise precondition of memset Unknown valid_s: valid_or_empty(s, n)
. reference.c 341 update_drift_file precondition of strlen Unknown valid_string_s: valid_read_string(s)
......@@ -451,7 +446,6 @@ directory file line function property kind status property
. reference.c 422 update_fb_drifts mem_access Unknown \valid(&(fb_drifts + i)->secs)
. reference.c 427 update_fb_drifts initialization Unknown \initialized(&(fb_drifts + i)->freq)
. reference.c 427 update_fb_drifts mem_access Unknown \valid(&(fb_drifts + i)->freq)
. reference.c 427 update_fb_drifts precondition of exp Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9
. reference.c 466 schedule_fb_drift signed_overflow Unknown 1 << i ≤ 2147483647
. reference.c 466 schedule_fb_drift shift Unknown 0 ≤ i < 32
. reference.c 468 schedule_fb_drift initialization Unknown \initialized(&(fb_drifts + (int)(i - fb_drift_min_0))->secs)
......@@ -460,7 +454,6 @@ directory file line function property kind status property
. reference.c 478 schedule_fb_drift initialization Unknown \initialized(&(fb_drifts + (int)(c - fb_drift_min_0))->freq)
. reference.c 478 schedule_fb_drift mem_access Unknown \valid_read(&(fb_drifts + (int)(c - fb_drift_min_0))->freq)
. reference.c 478 schedule_fb_drift signed_overflow Unknown c - fb_drift_min_0 ≤ 2147483647
. reference.c 516 maybe_log_offset precondition of fabs Unknown finite_arg: \is_finite(x)
. reference.c 526 maybe_log_offset precondition of popen Unknown valid_command: valid_read_string(command)
. reference.c 533 fprintf_va_3 precondition Unknown valid_read_string(param0)
. reference.c 533 maybe_log_offset precondition of fprintf_va_3 Unknown valid_read_string(param0)
......@@ -468,16 +461,10 @@ directory file line function property kind status property
. reference.c 534 maybe_log_offset precondition of fprintf_va_4 Unknown valid_read_string(param0)
. reference.c 541 maybe_log_offset precondition of fputs Unknown valid_string_s: valid_read_string(s)
. reference.c 551 maybe_log_offset precondition of pclose Unknown open_pipe: is_open_pipe(stream)
. reference.c 570 is_step_limit_reached precondition of fabs Unknown finite_arg: \is_finite(x)
. reference.c 586 is_offset_ok precondition of fabs Unknown finite_arg: \is_finite(x)
. reference.c 659 get_tz_leap signed_overflow Unknown (long)(t - when) + 10 ≤ 9223372036854775807
. reference.c 659 get_tz_leap signed_overflow Unknown -9223372036854775808 ≤ t - when
. reference.c 659 get_tz_leap signed_overflow Unknown t - when ≤ 9223372036854775807
. reference.c 757 set_leap_timeout signed_overflow Unknown (long)((long)(now / (long)((int)(24 * 3600))) + 1) * (long)((int)(24 * 3600)) ≤ 9223372036854775807
. reference.c 835 get_root_dispersion precondition of fabs Unknown finite_arg: \is_finite(x)
. reference.c 941 get_clock_estimates precondition of fabs Unknown finite_arg: \is_finite(x)
. reference.c 954 get_clock_estimates precondition of sqrt Unknown arg_positive: x ≥ -0.
. reference.c 954 get_clock_estimates precondition of sqrt Unknown finite_arg: \is_finite(x)
. reference.c 1011 REF_SetReference signed_overflow Unknown stratum + 1 ≤ 2147483647
. reference.c 1212 REF_GetReferenceParams signed_overflow Unknown -9223372036854775808 ≤ ref_time->tv_sec - 1
. reference.c 1324 REF_IsLeapSecondClose signed_overflow Unknown -now.tv_sec ≤ 9223372036854775807
......@@ -519,10 +506,6 @@ directory file line function property kind status property
. regress.c 304 RGR_FindBestRegression initialization Unknown \initialized(w + i)
. regress.c 304 RGR_FindBestRegression index_bound Unknown (int)(i - resid_start) < (int)(64 * 2)
. regress.c 304 RGR_FindBestRegression index_bound Unknown 0 ≤ (int)(i - resid_start)
. regress.c 309 RGR_FindBestRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 309 RGR_FindBestRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 311 RGR_FindBestRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 311 RGR_FindBestRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 353 find_ordered_entry_with_flags initialization Unknown \initialized(flags + index_0)
. regress.c 354 find_ordered_entry_with_flags initialization Unknown \initialized(x + index_0)
. regress.c 359 find_ordered_entry_with_flags initialization Unknown \initialized(flags + u)
......@@ -547,8 +530,6 @@ directory file line function property kind status property
. regress.c 678 RGR_MultipleRegress initialization Unknown \initialized(x1 + i)
. regress.c 679 RGR_MultipleRegress initialization Unknown \initialized(x2 + i)
. regress.c 683 RGR_MultipleRegress initialization Unknown \initialized(y + i)
. regress.c 698 RGR_MultipleRegress precondition of fabs Unknown finite_arg: \is_finite(x)
. regress.c 698 RGR_MultipleRegress precondition of fabs Unknown finite_arg: \is_finite(x)
. samplefilt.h 35 SPF_CreateInstance assigns clause Unknown assigns \nothing;
. samplefilt.h 35 SPF_CreateInstance from clause Unknown assigns \result \from min_samples, max_samples, max_dispersion, combine_ratio;
. samplefilt.h 37 SPF_DestroyInstance assigns clause Unknown assigns *filter;
......@@ -590,15 +571,8 @@ directory file line function property kind status property
. sources.c 516 combine_sources initialization Unknown \initialized(&(*(sources + selected_source_index))->sel_info.root_distance)
. sources.c 522 combine_sources initialization Unknown \initialized(sel_sources + i)
. sources.c 533 combine_sources initialization Unknown \initialized(&(*(sources + index_0))->sel_info.root_distance)
. sources.c 534 combine_sources precondition of fabs Unknown finite_arg: \is_finite(x)
. sources.c 554 combine_sources initialization Unknown \initialized(&(*(sources + index_0))->sel_info.root_distance)
. sources.c 574 combine_sources precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. sources.c 576 combine_sources precondition of sqrt Unknown arg_positive: x ≥ -0.
. sources.c 576 combine_sources precondition of sqrt Unknown finite_arg: \is_finite(x)
. sources.c 578 combine_sources precondition of sqrt Unknown arg_positive: x ≥ -0.
. sources.c 578 combine_sources precondition of sqrt Unknown finite_arg: \is_finite(x)
. sources.c 579 combine_sources precondition of sqrt Unknown arg_positive: x ≥ -0.
. sources.c 579 combine_sources precondition of sqrt Unknown finite_arg: \is_finite(x)
. sources.c 634 SRC_SelectSource dangling_pointer Unknown ¬\dangling(sources + i)
. sources.c 634 SRC_SelectSource precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. sources.c 663 SRC_SelectSource initialization Unknown \initialized(&first_sample_ago)
......@@ -708,7 +682,6 @@ directory file line function property kind status property
. sourcestats.c 479 correct_asymmetry index_bound Unknown i < (int)(64 * 2)
. sourcestats.c 479 correct_asymmetry initialization Unknown \initialized(&inst->peer_delays[tmp])
. sourcestats.c 479 correct_asymmetry signed_overflow Unknown i - inst->runs_samples ≤ 2147483647
. sourcestats.c 482 correct_asymmetry precondition of fabs Unknown finite_arg: \is_finite(x)
. sourcestats.c 492 correct_asymmetry initialization Unknown \initialized(&delays[i])
. sourcestats.c 492 correct_asymmetry initialization Unknown \initialized(&inst->asymmetry)
. sourcestats.c 492 correct_asymmetry initialization Unknown \initialized(offsets + i)
......@@ -732,12 +705,7 @@ directory file line function property kind status property
. sourcestats.c 578 SST_DoNewRegression initialization Unknown \initialized(&est_intercept)
. sourcestats.c 579 SST_DoNewRegression initialization Unknown \initialized(&inst->last_sample)
. sourcestats.c 580 SST_DoNewRegression initialization Unknown \initialized(&est_intercept_sd)
. sourcestats.c 581 SST_DoNewRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. sourcestats.c 581 SST_DoNewRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. sourcestats.c 581 SST_DoNewRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. sourcestats.c 581 SST_DoNewRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. sourcestats.c 582 SST_DoNewRegression initialization Unknown \initialized(&nruns)
. sourcestats.c 585 SST_DoNewRegression precondition of fabs Unknown finite_arg: \is_finite(x)
. sourcestats.c 593 SST_DoNewRegression initialization Unknown \initialized(&best_start)
. sourcestats.c 593 SST_DoNewRegression initialization Unknown \initialized(&inst->asymmetry)
. sourcestats.c 594 SST_DoNewRegression initialization Unknown \initialized(&inst->offset_time.tv_sec)
......@@ -840,12 +808,6 @@ directory file line function property kind status property
. util.c 1213 UTI_GetRandomBytesUrandom precondition of fread Unknown valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
FRAMAC_SHARE/libc __fc_inet.h 358 inet_addr precondition Unknown valid_arg: valid_read_string(arg)
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0
FRAMAC_SHARE/libc math.h 325 exp precondition Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9
FRAMAC_SHARE/libc math.h 362 log precondition Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc math.h 363 log precondition Unknown arg_positive: x > 0
FRAMAC_SHARE/libc math.h 449 fabs precondition Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc math.h 493 sqrt precondition Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc math.h 494 sqrt precondition Unknown arg_positive: x ≥ -0.
FRAMAC_SHARE/libc netdb.c 113 gethostbyname mem_access Unknown \valid_read(cp)
FRAMAC_SHARE/libc netdb.c 116 gethostbyname mem_access Unknown \valid_read(cp)
FRAMAC_SHARE/libc netdb.c 119 gethostbyname precondition of inet_addr Unknown valid_arg: valid_read_string(arg)
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -10,10 +10,6 @@ directory file line function property kind status property
. regress.c 91 RGR_WeightedRegression initialization Unknown \initialized(x + i)
. regress.c 91 RGR_WeightedRegression initialization Unknown \initialized(y + i)
. regress.c 92 RGR_WeightedRegression initialization Unknown \initialized(w + i)
. regress.c 97 RGR_WeightedRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 97 RGR_WeightedRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 99 RGR_WeightedRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 99 RGR_WeightedRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 183 n_runs_from_residuals initialization Unknown \initialized(resid + (int)(i - 1))
. regress.c 183 n_runs_from_residuals mem_access Unknown \valid_read(resid + (int)(i - 1))
. regress.c 183 n_runs_from_residuals initialization Unknown \initialized(resid + i)
......@@ -41,10 +37,6 @@ directory file line function property kind status property
. regress.c 304 RGR_FindBestRegression initialization Unknown \initialized(&resid[(int)(i - resid_start)])
. regress.c 304 RGR_FindBestRegression initialization Unknown \initialized(w + i)
. regress.c 304 RGR_FindBestRegression index_bound Unknown 0 ≤ (int)(i - resid_start)
. regress.c 309 RGR_FindBestRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 309 RGR_FindBestRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 311 RGR_FindBestRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 311 RGR_FindBestRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 350 find_ordered_entry_with_flags precondition of __FC_assert Unknown nonnull_c: c ≢ 0
. regress.c 353 find_ordered_entry_with_flags initialization Unknown \initialized(flags + index_0)
. regress.c 354 find_ordered_entry_with_flags initialization Unknown \initialized(x + index_0)
......@@ -82,8 +74,6 @@ directory file line function property kind status property
. regress.c 564 RGR_FindBestRobustRegression initialization Unknown \initialized(x + i)
. regress.c 574 RGR_FindBestRobustRegression initialization Unknown \initialized(x + i)
. regress.c 574 RGR_FindBestRobustRegression initialization Unknown \initialized(y + i)
. regress.c 581 RGR_FindBestRobustRegression precondition of sqrt Unknown arg_positive: x ≥ -0.
. regress.c 581 RGR_FindBestRobustRegression precondition of sqrt Unknown finite_arg: \is_finite(x)
. regress.c 616 RGR_FindBestRobustRegression precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
. regress.c 630 RGR_FindBestRobustRegression initialization Unknown \initialized(x + i)
. regress.c 630 RGR_FindBestRobustRegression initialization Unknown \initialized(y + i)
......@@ -91,22 +81,10 @@ directory file line function property kind status property
. regress.c 678 RGR_MultipleRegress initialization Unknown \initialized(x1 + i)
. regress.c 679 RGR_MultipleRegress initialization Unknown \initialized(x2 + i)
. regress.c 683 RGR_MultipleRegress initialization Unknown \initialized(y + i)
. regress.c 698 RGR_MultipleRegress precondition of fabs Unknown finite_arg: \is_finite(x)
. regress.c 698 RGR_MultipleRegress precondition of fabs Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Invalid or unreachable nonnull_c: c ≢ 0
FRAMAC_SHARE/libc math.h 449 fabs precondition Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc math.h 493 sqrt precondition Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc math.h 494 sqrt precondition Unknown arg_positive: x ≥ -0.
FRAMAC_SHARE/libc string.h 115 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 52 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 53 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 60 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 61 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 66 test_unit initialization Unknown \initialized(&b2)
test/unit regress.c 66 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 70 test_unit initialization Unknown \initialized(&y[(long)(tmp_11 % (long)n)])
test/unit regress.c 75 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 76 test_unit precondition of fabs Unknown finite_arg: \is_finite(x)
test/unit regress.c 85 test_unit initialization Unknown \initialized(&x[j])
test/unit regress.c 102 test_unit initialization Unknown \initialized(&x[(int)(j - 1)])
......@@ -64,40 +64,6 @@ stack: RGR_WeightedRegression :: test/unit/regress.c:50 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:97:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:97 <-
RGR_WeightedRegression :: test/unit/regress.c:50 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:97:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:97 <-
RGR_WeightedRegression :: test/unit/regress.c:50 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:99:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:99 <-
RGR_WeightedRegression :: test/unit/regress.c:50 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:99:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:99 <-
RGR_WeightedRegression :: test/unit/regress.c:50 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:52:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:52 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:53:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:53 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:254:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(x + i);
stack: RGR_FindBestRegression :: test/unit/regress.c:55 <-
test_unit :: test/unit/test.c:70 <-
......@@ -190,40 +156,6 @@ stack: RGR_FindBestRegression :: test/unit/regress.c:55 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:309:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:309 <-
RGR_FindBestRegression :: test/unit/regress.c:55 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:309:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:309 <-
RGR_FindBestRegression :: test/unit/regress.c:55 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:311:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:311 <-
RGR_FindBestRegression :: test/unit/regress.c:55 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:311:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:311 <-
RGR_FindBestRegression :: test/unit/regress.c:55 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:60:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:60 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:61:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:61 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:552:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(y + i);
stack: RGR_FindBestRobustRegression :: test/unit/regress.c:72 <-
test_unit :: test/unit/test.c:70 <-
......@@ -254,18 +186,6 @@ stack: RGR_FindBestRobustRegression :: test/unit/regress.c:72 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:581:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:581 <-
RGR_FindBestRobustRegression :: test/unit/regress.c:72 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:581:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:581 <-
RGR_FindBestRobustRegression :: test/unit/regress.c:72 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:469:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(y + i);
stack: eval_robust_residual :: regress.c:595 <-
RGR_FindBestRobustRegression :: test/unit/regress.c:72 <-
......@@ -396,82 +316,12 @@ stack: __FC_assert :: regress.c:616 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:75:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:75 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:76:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:76 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:85:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(&x[j]);
stack: test_unit :: test/unit/test.c:70 <- main :: fc_stubs.c:37 <- eva_main
test/unit/regress.c:87:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(&x[j]);
stack: test_unit :: test/unit/test.c:70 <- main :: fc_stubs.c:37 <- eva_main
test/unit/regress.c:102:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(&x[(int)(j - 1)]);
stack: test_unit :: test/unit/test.c:70 <- main :: fc_stubs.c:37 <- eva_main
regress.c:97:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:97 <-
RGR_WeightedRegression :: test/unit/regress.c:108 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:97:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:97 <-
RGR_WeightedRegression :: test/unit/regress.c:108 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:99:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:99 <-
RGR_WeightedRegression :: test/unit/regress.c:108 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:99:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:99 <-
RGR_WeightedRegression :: test/unit/regress.c:108 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:309:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:309 <-
RGR_FindBestRegression :: test/unit/regress.c:110 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:309:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:309 <-
RGR_FindBestRegression :: test/unit/regress.c:110 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:311:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:311 <-
RGR_FindBestRegression :: test/unit/regress.c:110 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:311:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:311 <-
RGR_FindBestRegression :: test/unit/regress.c:110 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:581:[eva:alarm] warning: function sqrt: precondition 'finite_arg' got status unknown.
stack: sqrt :: regress.c:581 <-
RGR_FindBestRobustRegression :: test/unit/regress.c:115 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:581:[eva:alarm] warning: function sqrt: precondition 'arg_positive' got status unknown.
stack: sqrt :: regress.c:581 <-
RGR_FindBestRobustRegression :: test/unit/regress.c:115 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:616:[eva:alarm] warning: function __FC_assert: precondition 'nonnull_c' got status invalid.
stack: __FC_assert :: regress.c:616 <-
RGR_FindBestRobustRegression :: test/unit/regress.c:115 <-
......@@ -533,25 +383,8 @@ stack: RGR_MultipleRegress :: test/unit/regress.c:64 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:698:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: regress.c:698 <-
RGR_MultipleRegress :: test/unit/regress.c:64 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:698:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: regress.c:698 <-
RGR_MultipleRegress :: test/unit/regress.c:64 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
test/unit/regress.c:66:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(&b2);
stack: test_unit :: test/unit/test.c:70 <- main :: fc_stubs.c:37 <- eva_main
test/unit/regress.c:66:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: test/unit/regress.c:66 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:363:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(flags + v);
stack: find_ordered_entry_with_flags :: regress.c:427 <-
find_median :: regress.c:472 <-
......@@ -625,18 +458,6 @@ stack: RGR_FindBestRegression :: test/unit/regress.c:110 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:698:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: regress.c:698 <-
RGR_MultipleRegress :: test/unit/regress.c:113 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:698:[eva:alarm] warning: function fabs: precondition 'finite_arg' got status unknown.
stack: fabs :: regress.c:698 <-
RGR_MultipleRegress :: test/unit/regress.c:113 <-
test_unit :: test/unit/test.c:70 <-
main :: fc_stubs.c:37 <-
eva_main
regress.c:362:[eva:alarm] warning: accessing uninitialized left-value. assert \initialized(flags + v);
stack: find_ordered_entry_with_flags :: regress.c:425 <-
find_median :: regress.c:472 <-
......
Subproject commit db6a22445f68ffbfc12b97ebab88dfe968f85875
Subproject commit 537d662b240cc91af8ce5294deca0f760a51baea
directory file line function property kind status property
FRAMAC_SHARE/libc math.h 325 exp precondition Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9
FRAMAC_SHARE/libc math.h 449 fabs precondition Unknown finite_arg: \is_finite(x)
FRAMAC_SHARE/libc stdio.h 207 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 207 fprintf from clause Unknown assigns \result \from *stream, *(format + (0 ..));
src impls.c 26 PT1_Filter precondition of exp Unknown finite_domain: x ≤ 0x1.62e42fefa39efp+9
src impls.c 96 Sleep signed_overflow Unknown _t + delayMs ≤ 2147483647
src roco.c 170 RoCo_process precondition of fabs Unknown finite_arg: \is_finite(x)
src roco.c 228 RoCo_process precondition of fabs Unknown finite_arg: \is_finite(x)
2019/duble/prog.c:18:[kernel] warning: Body of function t falls-through. Adding a return statement
2019/duble/prog.c:18:[kernel:CERT:MSC:37] warning: Body of function t falls-through. Adding a return statement
2019/duble/prog.c:23:[kernel:typing:incompatible-types-call] warning: expected 'struct sockaddr const *' but got argument of type 'struct sockaddr_un *': tmp_0
2019/duble/prog.c:23:[kernel] warning: Body of function O falls-through. Adding a return statement
2019/duble/prog.c:23:[kernel:CERT:MSC:37] warning: Body of function O falls-through. Adding a return statement
2019/duble/prog.c:24:[kernel:typing:incompatible-types-call] warning: expected 'struct sockaddr *' but got argument of type 'struct sockaddr_un *': & A
2019/duble/prog.c:24:[kernel] warning: Body of function H falls-through. Adding a return statement
2019/duble/prog.c:26:[kernel] warning: Body of function Q falls-through. Adding a return statement
2019/duble/prog.c:26:[kernel] warning: Body of function P falls-through. Adding a return statement
2019/duble/prog.c:24:[kernel:CERT:MSC:37] warning: Body of function H falls-through. Adding a return statement
2019/duble/prog.c:26:[kernel:CERT:MSC:37] warning: Body of function Q falls-through. Adding a return statement
2019/duble/prog.c:26:[kernel:CERT:MSC:37] warning: Body of function P falls-through. Adding a return statement
2019/duble/prog.c:27:[kernel:typing:incompatible-types-call] warning: expected 'struct sockaddr const *' but got argument of type 'struct sockaddr_un *': D
2019/duble/prog.c:39:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
2019/duble/prog.c:39:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
......
01_w_Defects/data_lost.c:56:[kernel:parser:decimal-float] warning: Floating-point constant 2.14748365e+09F is not represented exactly. Will use 0x1.0000000000000p31.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
01_w_Defects/not_return.c:20:[kernel] warning: Body of function not_return_001_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:39:[kernel] warning: Body of function not_return_002_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:74:[kernel] warning: Body of function not_return_003_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:98:[kernel] warning: Body of function not_return_004_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:20:[kernel:CERT:MSC:37] warning: Body of function not_return_001_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:39:[kernel:CERT:MSC:37] warning: Body of function not_return_002_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:74:[kernel:CERT:MSC:37] warning: Body of function not_return_003_func_001 falls-through. Adding a return statement
01_w_Defects/not_return.c:98:[kernel:CERT:MSC:37] warning: Body of function not_return_004_func_001 falls-through. Adding a return statement
......@@ -501,7 +501,6 @@ src x509-parser.c 7188 find_kp_by_oid precondition Unknown len > 0 ∧ buf ≢ (
src x509-parser.c 7189 find_kp_by_oid postcondition Unknown \result ≢ (_kp_oid const *)0 ⇒ (∃ ℤ i; 0 ≤ i < sizeof(known_kp_oids) / sizeof(known_kp_oids[0]) ∧ \result ≡ &known_kp_oids[i])
src x509-parser.c 7190 find_kp_by_oid postcondition Unknown \old(len) ≡ 0 ⇒ \result ≡ (_kp_oid const *)0
src x509-parser.c 7200 find_kp_by_oid ptr_comparison Unknown \pointer_comparable((void *)buf, (void *)0)
src x509-parser.c 7215 find_kp_by_oid user assertion Unknown cur ≡ &known_kp_oids[k]
src x509-parser.c 7220 find_kp_by_oid user assertion Unknown \valid_read(buf + (0 .. len - 1))
src x509-parser.c 7244 parse_ext_EKU precondition Unknown len > 0 ∧ buf ≢ \null ⇒ \valid_read(buf + (0 .. len - 1))
src x509-parser.c 7248 parse_ext_EKU postcondition Unknown \old(len) ≡ 0 ⇒ \result < 0
......
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