-
David Bühler authoredDavid Bühler authored
signal_h.res.oracle 14.28 KiB
[kernel] Parsing signal_h.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] computing for function sigemptyset <- main.
Called from signal_h.c:10.
[eva] using specification for function sigemptyset
[eva] signal_h.c:10:
function sigemptyset: precondition 'valid_set' got status valid.
[eva] Done for function sigemptyset
[eva] computing for function sigaddset <- main.
Called from signal_h.c:11.
[eva] using specification for function sigaddset
[eva] signal_h.c:11:
function sigaddset: precondition 'valid_set' got status valid.
[eva] signal_h.c:11:
function sigaddset: precondition 'initialization,set' got status valid.
[eva] Done for function sigaddset
[eva] computing for function sigdelset <- main.
Called from signal_h.c:14.
[eva] using specification for function sigdelset
[eva] signal_h.c:14:
function sigdelset: precondition 'valid_set' got status valid.
[eva] signal_h.c:14:
function sigdelset: precondition 'initialization,set' got status valid.
[eva] Done for function sigdelset
[eva] computing for function sigismember <- main.
Called from signal_h.c:17.
[eva] using specification for function sigismember
[eva] signal_h.c:17:
function sigismember: precondition 'valid_read_set' got status valid.
[eva] signal_h.c:17:
function sigismember: precondition 'initialization,set' got status valid.
[eva] Done for function sigismember
[eva] computing for function sigfillset <- main.
Called from signal_h.c:18.
[eva] using specification for function sigfillset
[eva] signal_h.c:18:
function sigfillset: precondition 'valid_set' got status valid.
[eva] Done for function sigfillset
[eva] computing for function sigismember <- main.
Called from signal_h.c:19.
[eva] signal_h.c:19:
function sigismember: precondition 'valid_read_set' got status valid.
[eva] signal_h.c:19:
function sigismember: precondition 'initialization,set' got status valid.
[eva] Done for function sigismember
[eva] computing for function sigaddset <- main.
Called from signal_h.c:22.
[eva] signal_h.c:22:
function sigaddset: precondition 'valid_set' got status valid.
[eva:alarm] signal_h.c:22: Warning:
function sigaddset: precondition 'initialization,set' got status invalid.
[eva] Done for function sigaddset
[eva] computing for function sigprocmask <- main.
Called from signal_h.c:29.
[eva] using specification for function sigprocmask
[eva] signal_h.c:29:
function sigprocmask: precondition 'valid_set_or_null' got status valid.
[eva] signal_h.c:29:
function sigprocmask: precondition 'valid_how' got status valid.
[eva] signal_h.c:29:
function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
[eva] signal_h.c:29:
function sigprocmask: precondition 'separation' got status valid.
[eva] Done for function sigprocmask
[eva] computing for function sigaddset <- main.
Called from signal_h.c:32.[eva] signal_h.c:32:
function sigaddset: precondition 'valid_set' got status valid.
[eva] signal_h.c:32:
function sigaddset: precondition 'initialization,set' got status valid.
[eva] Done for function sigaddset
[eva] computing for function sigprocmask <- main.
Called from signal_h.c:35.
[eva] signal_h.c:35:
function sigprocmask: precondition 'valid_set_or_null' got status valid.
[eva] signal_h.c:35:
function sigprocmask: precondition 'valid_how' got status valid.
[eva] signal_h.c:35:
function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
[eva] signal_h.c:35:
function sigprocmask: precondition 'separation' got status valid.
[eva:invalid-assigns] signal_h.c:35:
Completely invalid destination for assigns clause *oldset. Ignoring.
[eva] Done for function sigprocmask
[eva] computing for function sigprocmask <- main.
Called from signal_h.c:38.
[eva] signal_h.c:38:
function sigprocmask: precondition 'valid_set_or_null' got status valid.
[eva] signal_h.c:38:
function sigprocmask: precondition 'valid_how' got status valid.
[eva] signal_h.c:38:
function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
[eva] signal_h.c:38:
function sigprocmask: precondition 'separation' got status valid.
[eva] Done for function sigprocmask
[eva] computing for function kill <- main.
Called from signal_h.c:42.
[eva] using specification for function kill
[eva] Done for function kill
[eva] computing for function sigaction <- main.
Called from signal_h.c:45.
[eva] using specification for function sigaction
[eva] signal_h.c:45:
function sigaction: precondition 'valid_signal' got status valid.
[eva] signal_h.c:45:
function sigaction: precondition 'valid_oldact_or_null' got status valid.
[eva] signal_h.c:45:
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:45:
function sigaction: precondition 'separation,separated_acts' got status valid.
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:45.
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:48.
[eva] signal_h.c:48:
function sigaction: precondition 'valid_signal' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'valid_oldact_or_null' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'separation,separated_acts' got status valid.
[eva] FRAMAC_SHARE/libc/signal.h:229:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:51.
[eva] signal_h.c:51:
function sigaction: precondition 'valid_signal' got status valid.
[eva] signal_h.c:51:
function sigaction: precondition 'valid_oldact_or_null' got status valid.
[eva] signal_h.c:51:
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:51: function sigaction: precondition 'separation,separated_acts' got status valid.
[eva:invalid-assigns] signal_h.c:51:
Completely invalid destination for assigns clause *oldact. Ignoring.
[eva] Done for function sigaction
[eva] signal_h.c:55: assertion 'valid_nsig' got status valid.
[eva] computing for function sigsuspend <- main.
Called from signal_h.c:59.
[eva] using specification for function sigsuspend
[eva] signal_h.c:59:
function sigsuspend: precondition 'valid_mask_or_null' got status valid.
[eva] Done for function sigsuspend
[eva] signal_h.c:60: assertion 'sigsuspend_errno_eintr' got status valid.
[eva] signal_h.c:61: assertion 'sigsuspend_return' got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_errno ∈ [--..--]
__fc_sigaction[0]{.sa_handler; .sa_sigaction} ∈ {0}
[0]{.sa_mask; .sa_flags} ∈ [--..--]
[1]{.sa_handler; .sa_sigaction} ∈ {0}
[1]{.sa_mask; .sa_flags} ∈ [--..--]
[2]{.sa_handler; .sa_sigaction} ∈ {0}
[2]{.sa_mask; .sa_flags} ∈ [--..--]
[3]{.sa_handler; .sa_sigaction} ∈ {0}
[3]{.sa_mask; .sa_flags} ∈ [--..--]
[4]{.sa_handler; .sa_sigaction} ∈ {0}
[4]{.sa_mask; .sa_flags} ∈ [--..--]
[5]{.sa_handler; .sa_sigaction} ∈ {0}
[5]{.sa_mask; .sa_flags} ∈ [--..--]
[6]{.sa_handler; .sa_sigaction} ∈ {0}
[6]{.sa_mask; .sa_flags} ∈ [--..--]
[7]{.sa_handler; .sa_sigaction} ∈ {0}
[7]{.sa_mask; .sa_flags} ∈ [--..--]
[8]{.sa_handler; .sa_sigaction} ∈ {0}
[8]{.sa_mask; .sa_flags} ∈ [--..--]
[9]{.sa_handler; .sa_sigaction} ∈ {0}
[9]{.sa_mask; .sa_flags} ∈ [--..--]
[10] ∈
{{ garbled mix of &{__fc_sigaction}
(origin: Library function) }}
[11]{.sa_handler; .sa_sigaction} ∈ {0}
[11]{.sa_mask; .sa_flags} ∈ [--..--]
[12]{.sa_handler; .sa_sigaction} ∈ {0}
[12]{.sa_mask; .sa_flags} ∈ [--..--]
[13]{.sa_handler; .sa_sigaction} ∈ {0}
[13]{.sa_mask; .sa_flags} ∈ [--..--]
[14]{.sa_handler; .sa_sigaction} ∈ {0}
[14]{.sa_mask; .sa_flags} ∈ [--..--]
[15]{.sa_handler; .sa_sigaction} ∈ {0}
[15]{.sa_mask; .sa_flags} ∈ [--..--]
[16]{.sa_handler; .sa_sigaction} ∈ {0}
{[16]{.sa_mask; .sa_flags}; [17]} ∈ [--..--]
[18] ∈
{{ garbled mix of &{__fc_sigaction}
(origin: Library function) }}
[19]{.sa_handler; .sa_sigaction} ∈ {0}
[19]{.sa_mask; .sa_flags} ∈ [--..--]
[20]{.sa_handler; .sa_sigaction} ∈ {0}
[20]{.sa_mask; .sa_flags} ∈ [--..--]
[21]{.sa_handler; .sa_sigaction} ∈ {0}
[21]{.sa_mask; .sa_flags} ∈ [--..--]
[22]{.sa_handler; .sa_sigaction} ∈ {0}
[22]{.sa_mask; .sa_flags} ∈ [--..--]
[23]{.sa_handler; .sa_sigaction} ∈ {0}
[23]{.sa_mask; .sa_flags} ∈ [--..--]
[24]{.sa_handler; .sa_sigaction} ∈ {0}
[24]{.sa_mask; .sa_flags} ∈ [--..--]
[25]{.sa_handler; .sa_sigaction} ∈ {0}
[25]{.sa_mask; .sa_flags} ∈ [--..--] [26]{.sa_handler; .sa_sigaction} ∈ {0}
[26]{.sa_mask; .sa_flags} ∈ [--..--]
[27]{.sa_handler; .sa_sigaction} ∈ {0}
[27]{.sa_mask; .sa_flags} ∈ [--..--]
[28]{.sa_handler; .sa_sigaction} ∈ {0}
[28]{.sa_mask; .sa_flags} ∈ [--..--]
[29]{.sa_handler; .sa_sigaction} ∈ {0}
[29]{.sa_mask; .sa_flags} ∈ [--..--]
[30]{.sa_handler; .sa_sigaction} ∈ {0}
[30]{.sa_mask; .sa_flags} ∈ [--..--]
[31]{.sa_handler; .sa_sigaction} ∈ {0}
[31]{.sa_mask; .sa_flags} ∈ [--..--]
[32]{.sa_handler; .sa_sigaction} ∈ {0}
[32]{.sa_mask; .sa_flags} ∈ [--..--]
[33]{.sa_handler; .sa_sigaction} ∈ {0}
[33]{.sa_mask; .sa_flags} ∈ [--..--]
[34]{.sa_handler; .sa_sigaction} ∈ {0}
[34]{.sa_mask; .sa_flags} ∈ [--..--]
[35]{.sa_handler; .sa_sigaction} ∈ {0}
[35]{.sa_mask; .sa_flags} ∈ [--..--]
[36]{.sa_handler; .sa_sigaction} ∈ {0}
[36]{.sa_mask; .sa_flags} ∈ [--..--]
[37]{.sa_handler; .sa_sigaction} ∈ {0}
[37]{.sa_mask; .sa_flags} ∈ [--..--]
[38]{.sa_handler; .sa_sigaction} ∈ {0}
[38]{.sa_mask; .sa_flags} ∈ [--..--]
[39]{.sa_handler; .sa_sigaction} ∈ {0}
[39]{.sa_mask; .sa_flags} ∈ [--..--]
[40]{.sa_handler; .sa_sigaction} ∈ {0}
[40]{.sa_mask; .sa_flags} ∈ [--..--]
[41]{.sa_handler; .sa_sigaction} ∈ {0}
[41]{.sa_mask; .sa_flags} ∈ [--..--]
[42]{.sa_handler; .sa_sigaction} ∈ {0}
[42]{.sa_mask; .sa_flags} ∈ [--..--]
[43]{.sa_handler; .sa_sigaction} ∈ {0}
[43]{.sa_mask; .sa_flags} ∈ [--..--]
[44]{.sa_handler; .sa_sigaction} ∈ {0}
[44]{.sa_mask; .sa_flags} ∈ [--..--]
[45]{.sa_handler; .sa_sigaction} ∈ {0}
[45]{.sa_mask; .sa_flags} ∈ [--..--]
[46]{.sa_handler; .sa_sigaction} ∈ {0}
[46]{.sa_mask; .sa_flags} ∈ [--..--]
[47]{.sa_handler; .sa_sigaction} ∈ {0}
[47]{.sa_mask; .sa_flags} ∈ [--..--]
[48]{.sa_handler; .sa_sigaction} ∈ {0}
[48]{.sa_mask; .sa_flags} ∈ [--..--]
[49]{.sa_handler; .sa_sigaction} ∈ {0}
[49]{.sa_mask; .sa_flags} ∈ [--..--]
[50]{.sa_handler; .sa_sigaction} ∈ {0}
[50]{.sa_mask; .sa_flags} ∈ [--..--]
[51]{.sa_handler; .sa_sigaction} ∈ {0}
[51]{.sa_mask; .sa_flags} ∈ [--..--]
[52]{.sa_handler; .sa_sigaction} ∈ {0}
[52]{.sa_mask; .sa_flags} ∈ [--..--]
[53]{.sa_handler; .sa_sigaction} ∈ {0}
[53]{.sa_mask; .sa_flags} ∈ [--..--]
[54]{.sa_handler; .sa_sigaction} ∈ {0}
[54]{.sa_mask; .sa_flags} ∈ [--..--]
[55]{.sa_handler; .sa_sigaction} ∈ {0}
[55]{.sa_mask; .sa_flags} ∈ [--..--]
[56]{.sa_handler; .sa_sigaction} ∈ {0}
[56]{.sa_mask; .sa_flags} ∈ [--..--]
[57]{.sa_handler; .sa_sigaction} ∈ {0}
[57]{.sa_mask; .sa_flags} ∈ [--..--]
[58]{.sa_handler; .sa_sigaction} ∈ {0}
[58]{.sa_mask; .sa_flags} ∈ [--..--]
[59]{.sa_handler; .sa_sigaction} ∈ {0}
[59]{.sa_mask; .sa_flags} ∈ [--..--]
[60]{.sa_handler; .sa_sigaction} ∈ {0}
[60]{.sa_mask; .sa_flags} ∈ [--..--] [61]{.sa_handler; .sa_sigaction} ∈ {0}
[61]{.sa_mask; .sa_flags} ∈ [--..--]
[62]{.sa_handler; .sa_sigaction} ∈ {0}
[62]{.sa_mask; .sa_flags} ∈ [--..--]
[63]{.sa_handler; .sa_sigaction} ∈ {0}
[63]{.sa_mask; .sa_flags} ∈ [--..--]
[64]{.sa_handler; .sa_sigaction} ∈ {0}
[64]{.sa_mask; .sa_flags} ∈ [--..--]
s ∈ [--..--]
uninit ∈ UNINITIALIZED
old ∈ [--..--] or UNINITIALIZED
kill_res ∈ {-1; 0} or UNINITIALIZED
sa1 ∈
{{ garbled mix of &{__fc_sigaction}
(origin: Library function {signal_h.c:45}) }} or UNINITIALIZED
sa2 ∈
{{ garbled mix of &{__fc_sigaction}
(origin: Library function {signal_h.c:48}) }} or UNINITIALIZED
__retres ∈ {-1; 0; 1; 2; 3}