diff --git a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle index 4f79daab252768291202e08471503b7270f49efe..65408261baad851c4d43a72458d7890573210137 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle @@ -2,8 +2,6 @@ [e-acsl] translation done in project "e-acsl". [eva:alarm] init_function.c:16: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] init_function.c:16: Warning: assertion got status unknown. [eva] init_function.c:17: Warning: ignoring unsupported allocates clause [eva:alarm] init_function.c:18: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] init_function.c:18: Warning: assertion got status unknown. diff --git a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle index 5f0b0f66a93f2330a25b5ada4e9cccf1f8af46b1..4cd231d4748e3c00c565b704f2f4ecfa77f46068 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle @@ -3,21 +3,17 @@ [eva] memsize.c:14: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:15: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:15: Warning: assertion got status unknown. [eva] memsize.c:16: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:17: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:17: Warning: assertion got status unknown. [eva] memsize.c:20: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:20: Warning: function free: precondition 'freeable' got status unknown. [eva:alarm] memsize.c:21: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:21: Warning: assertion got status unknown. [eva] memsize.c:25: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:26: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:26: Warning: assertion got status unknown. [eva] FRAMAC_SHARE/libc/stdlib.h:452: Warning: no 'assigns \result \from ...' clause specified for function realloc [eva] memsize.c:29: Warning: ignoring unsupported allocates clause @@ -25,31 +21,25 @@ function realloc: precondition 'freeable' got status unknown. [eva:alarm] memsize.c:30: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:30: Warning: assertion got status unknown. [eva] memsize.c:33: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:33: Warning: function realloc: precondition 'freeable' got status unknown. [eva:alarm] memsize.c:34: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:34: Warning: assertion got status unknown. [eva] memsize.c:37: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:37: Warning: function realloc: precondition 'freeable' got status unknown. [eva:alarm] memsize.c:39: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:39: Warning: assertion got status unknown. [eva] memsize.c:42: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:43: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:43: Warning: assertion got status unknown. [eva] memsize.c:46: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:47: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:47: Warning: assertion got status unknown. [eva] memsize.c:50: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:51: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:51: Warning: assertion got status unknown. [eva:alarm] memsize.c:52: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva] FRAMAC_SHARE/libc/stdlib.h:385: Warning: @@ -57,10 +47,8 @@ [eva] memsize.c:55: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:56: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:56: Warning: assertion got status unknown. [eva] memsize.c:60: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:61: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] memsize.c:61: Warning: assertion got status unknown. [eva:alarm] memsize.c:62: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml index 87b85d514c7af5f9e740c6181510adc0cd1c4426..c079828acc7d1ca30e715aba4818415a89dbe1a1 100644 --- a/src/plugins/inout/operational_inputs.ml +++ b/src/plugins/inout/operational_inputs.ml @@ -590,6 +590,8 @@ module Callwise = struct let call_for_callwise_inout (call_type, state, call_stack) = let (current_function, ki as call_site) = List.hd call_stack in let merge_inout inout = + Db.Operational_inputs.Record_Inout_Callbacks.apply + (call_stack, inout); if ki = Kglobal then merge_call_in_global_tables call_site inout else diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle index 38f04f2127c018dfd6bc26731b2203fc31b51517..a6456f3e810b6a38cf5d9ac6b270397aa8ae9bde 100644 --- a/tests/builtins/oracle/linked_list.1.res.oracle +++ b/tests/builtins/oracle/linked_list.1.res.oracle @@ -807,6 +807,8 @@ [eva] using specification for function printf_va_1 [eva] linked_list.c:51: function printf_va_1: precondition got status valid. [eva] Done for function printf_va_1 +[kernel] linked_list.c:51: + more than 100(128) elements to enumerate. Approximating. [eva] linked_list.c:50: starting to merge loop iterations [eva:alarm] linked_list.c:51: Warning: out of bounds read. assert \valid_read(&curr->val); @@ -814,8 +816,6 @@ Called from linked_list.c:51. [eva] Done for function printf_va_1 [eva] Recording results for main -[kernel] linked_list.c:43: - more than 100(128) elements to enumerate. Approximating. [kernel] linked_list.c:44: more than 100(128) elements to enumerate. Approximating. [eva] done for function main diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle index 418dee718112bfacde2983c028cd5c6a76ce21de..0141d180b8fb97c279280f379a382b1fb4c2f4dc 100644 --- a/tests/libc/oracle/signal_h.res.oracle +++ b/tests/libc/oracle/signal_h.res.oracle @@ -283,7 +283,7 @@ kill_res ∈ {-1; 0} sa1 ∈ {{ garbled mix of &{__fc_sigaction} - (origin: Library function) }} or UNINITIALIZED + (origin: Library function {signal_h.c:45}) }} or UNINITIALIZED sa2 ∈ {{ garbled mix of &{__fc_sigaction} (origin: Library function {signal_h.c:48}) }} or UNINITIALIZED diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle index eb2edb9decf77dc91d8595d9841c47bcac09e7aa..cb22bbb0198fb86def1f95ae8ab4817a07775f8c 100644 --- a/tests/libc/oracle/stdlib_c.0.res.oracle +++ b/tests/libc/oracle/stdlib_c.0.res.oracle @@ -81,13 +81,24 @@ allocating variable __malloc_posix_memalign_l199_0 [eva] Recording results for posix_memalign [eva] Done for function posix_memalign +[eva] computing for function posix_memalign <- main. + Called from stdlib_c.c:40. +[eva] FRAMAC_SHARE/libc/stdlib.c:199: Call to builtin Frama_C_malloc +[eva] Recording results for posix_memalign +[eva] Done for function posix_memalign [eva] computing for function free <- main. Called from stdlib_c.c:41. [eva] stdlib_c.c:41: Warning: ignoring unsupported allocates clause [eva] stdlib_c.c:41: function free: precondition 'freeable' got status valid. [eva] Done for function free +[eva] computing for function free <- main. + Called from stdlib_c.c:41. +[eva] Done for function free [eva] stdlib_c.c:44: Call to builtin Frama_C_malloc [eva] stdlib_c.c:44: allocating variable __malloc_main_l44 +[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc +[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc +[eva] stdlib_c.c:44: Call to builtin Frama_C_malloc [eva] computing for function realpath <- main. Called from stdlib_c.c:46. [eva] computing for function Frama_C_interval <- realpath <- main. @@ -109,6 +120,9 @@ [eva] Done for function Frama_C_make_unknown [eva] Recording results for realpath [eva] Done for function realpath +[eva] stdlib_c.c:46: Reusing old results for call to realpath +[eva] stdlib_c.c:46: Reusing old results for call to realpath +[eva] stdlib_c.c:46: Reusing old results for call to realpath [eva:alarm] stdlib_c.c:48: Warning: assertion 'valid_if_exact' got status unknown. [eva] computing for function Frama_C_nondet <- main. @@ -118,6 +132,24 @@ [eva] computing for function Frama_C_nondet <- main. Called from stdlib_c.c:50. [eva] Done for function Frama_C_nondet +[eva] computing for function Frama_C_nondet <- main. + Called from stdlib_c.c:50. +[eva] Done for function Frama_C_nondet +[eva] computing for function Frama_C_nondet <- main. + Called from stdlib_c.c:50. +[eva] Done for function Frama_C_nondet +[eva] computing for function Frama_C_nondet <- main. + Called from stdlib_c.c:50. +[eva] Done for function Frama_C_nondet +[eva] computing for function Frama_C_nondet <- main. + Called from stdlib_c.c:50. +[eva] Done for function Frama_C_nondet +[eva] computing for function Frama_C_nondet <- main. + Called from stdlib_c.c:50. +[eva] Done for function Frama_C_nondet +[eva] computing for function Frama_C_nondet <- main. + Called from stdlib_c.c:50. +[eva] Done for function Frama_C_nondet [eva:alarm] stdlib_c.c:51: Warning: assertion 'maybe_uninitialized' got status unknown. [eva] computing for function free <- main. @@ -128,12 +160,6 @@ [eva] computing for function free <- main. Called from stdlib_c.c:53. [eva] Done for function free -[eva] computing for function free <- main. - Called from stdlib_c.c:53. -[eva] Done for function free -[eva] computing for function free <- main. - Called from stdlib_c.c:53. -[eva] Done for function free [eva] computing for function realpath <- main. Called from stdlib_c.c:54. [eva] computing for function Frama_C_interval <- realpath <- main. @@ -163,34 +189,6 @@ [eva] Done for function Frama_C_make_unknown [eva] Recording results for realpath [eva] Done for function realpath -[eva] computing for function realpath <- main. - Called from stdlib_c.c:54. -[eva] computing for function Frama_C_interval <- realpath <- main. - Called from FRAMAC_SHARE/libc/stdlib.c:213. -[eva] Done for function Frama_C_interval -[eva] computing for function Frama_C_interval <- realpath <- main. - Called from FRAMAC_SHARE/libc/stdlib.c:222. -[eva] Done for function Frama_C_interval -[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc -[eva] computing for function Frama_C_make_unknown <- realpath <- main. - Called from FRAMAC_SHARE/libc/stdlib.c:230. -[eva] Done for function Frama_C_make_unknown -[eva] Recording results for realpath -[eva] Done for function realpath -[eva] computing for function realpath <- main. - Called from stdlib_c.c:54. -[eva] computing for function Frama_C_interval <- realpath <- main. - Called from FRAMAC_SHARE/libc/stdlib.c:213. -[eva] Done for function Frama_C_interval -[eva] computing for function Frama_C_interval <- realpath <- main. - Called from FRAMAC_SHARE/libc/stdlib.c:222. -[eva] Done for function Frama_C_interval -[eva] FRAMAC_SHARE/libc/stdlib.c:224: Call to builtin Frama_C_malloc -[eva] computing for function Frama_C_make_unknown <- realpath <- main. - Called from FRAMAC_SHARE/libc/stdlib.c:230. -[eva] Done for function Frama_C_make_unknown -[eva] Recording results for realpath -[eva] Done for function realpath [eva] computing for function canonicalize_file_name <- main. Called from stdlib_c.c:56. [eva] computing for function realpath <- canonicalize_file_name <- main. diff --git a/tests/libc/oracle/stdlib_h.res.oracle b/tests/libc/oracle/stdlib_h.res.oracle index 158e8ba4bdca33b8329f5d2080b2620a98693034..2599293e6669fd45228a86a483e8e71ce1aefe2f 100644 --- a/tests/libc/oracle/stdlib_h.res.oracle +++ b/tests/libc/oracle/stdlib_h.res.oracle @@ -325,21 +325,21 @@ base ∈ {0; 2; 36} sl ∈ {{ "12 34 -56" }} s ∈ {{ " 3.14 0x1.2p2" }} - pl ∈ {{ "12 34 -56" + [0..--] }} - q ∈ {{ " 3.14 0x1.2p2" + [0..--] }} + pl ∈ {{ "12 34 -56" + [0..9] }} + q ∈ {{ " 3.14 0x1.2p2" + [0..13] }} l ∈ [0..2147483647] - pll ∈ {{ "12 34 -56" + [0..--] }} + pll ∈ {{ "12 34 -56" + [0..9] }} ll ∈ [--..--] - pul ∈ {{ "12 34 -56" + [0..--] }} + pul ∈ {{ "12 34 -56" + [0..9] }} ul ∈ [--..--] - pull ∈ {{ "12 34 -56" + [0..--] }} + pull ∈ {{ "12 34 -56" + [0..9] }} ull ∈ [--..--] sd ∈ {{ " 3.14 0x1.2p2" }} - pd ∈ {{ " 3.14 0x1.2p2" + [0..--] }} + pd ∈ {{ " 3.14 0x1.2p2" + [0..13] }} d ∈ [-0. .. 1.] - pld ∈ {{ " 3.14 0x1.2p2" + [0..--] }} + pld ∈ {{ " 3.14 0x1.2p2" + [0..13] }} ld ∈ [-inf .. inf] ∪ {NaN} - pf ∈ {{ " 3.14 0x1.2p2" + [0..--] }} + pf ∈ {{ " 3.14 0x1.2p2" + [0..13] }} f ∈ [-inf .. inf] ∪ {NaN} ai[0] ∈ {1} [1] ∈ {-1} diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle index 1700a2d16a409383d26178f66d3732b5aee04684..a32b98d7871f1de7738a4e07da647fc39b86cf35 100644 --- a/tests/libc/oracle/time_h.res.oracle +++ b/tests/libc/oracle/time_h.res.oracle @@ -42,8 +42,6 @@ [eva] Done for function nanosleep [eva] computing for function nanosleep <- main. Called from time_h.c:22. -[eva:invalid-assigns] time_h.c:22: - Completely invalid destination for assigns clause *rmtp. Ignoring. [eva] Done for function nanosleep [eva] computing for function clock_nanosleep <- main. Called from time_h.c:28.