From d5ba9f23589037c600e2025a1852046a576d220a Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Wed, 10 Feb 2021 11:43:29 +0100 Subject: [PATCH] [eacsl] Update tests --- .../e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c | 1 + src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c | 1 + src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c | 1 + src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c | 1 + src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c | 1 + .../e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c | 1 + src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c | 1 + src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c | 1 + src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c | 1 + src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c | 1 + src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c | 1 + 30 files changed, 30 insertions(+) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c index be6316c86be..02552add425 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c @@ -276,6 +276,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(target)); __e_acsl_delete_block((void *)(source)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c index 8597f7d23ee..6c2d67be537 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c @@ -57,6 +57,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& global_i_ptr)); __e_acsl_delete_block((void *)(& global_i)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c index fc9046840ed..3cf6adc6f02 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c @@ -91,6 +91,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& S)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c index 0786c95e01e..67003d8a70d 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c @@ -34,6 +34,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(_G)); + return; } int main(int argc, char **argv) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c index 5ade9142b8f..5c8f2b5dde7 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c @@ -53,6 +53,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& n)); + return; } int main(int argc, char **argv) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c index 2ce056ec2ae..327af999d25 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c @@ -27,6 +27,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& t)); + return; } int main(int argc, char **argv) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c index 08f3b321a24..827fce50a41 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c @@ -17,6 +17,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(t)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c index c3248c722e3..b83e193f02f 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c @@ -44,6 +44,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& b)); __e_acsl_delete_block((void *)(& a)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c index d1e84e229ba..b6332376af7 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c @@ -20,6 +20,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& P)); __e_acsl_delete_block((void *)(& G)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c index 09554f35c62..084b8d80b0b 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c +++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c @@ -2558,6 +2558,7 @@ void __e_acsl_globals_clean(void) __e_acsl_delete_block((void *)(& valid_specifiers)); __e_acsl_delete_block((void *)(& __fc_p_time_tm)); __e_acsl_delete_block((void *)(& __fc_time_tm)); + return; } int main(int argc, char const **argv) diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c index 8b38c74f47a..a8dbdfefe43 100644 --- a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c +++ b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c @@ -42,6 +42,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& f)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c index b831f777ef0..378a05448dd 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c @@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& PA)); __e_acsl_delete_block((void *)(A)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c index cec16f53eaf..167233407ca 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c @@ -28,6 +28,7 @@ void __e_acsl_globals_clean(void) __e_acsl_delete_block((void *)(& ZERO)); __e_acsl_delete_block((void *)(& PA)); __e_acsl_delete_block((void *)(A)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c index 33dd06e7f2d..4f427bb14ad 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c @@ -19,6 +19,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& B)); + return; } int main(int argc, char **argv) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c index ab6e1941648..f8af717e7fc 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c @@ -74,6 +74,7 @@ void __e_acsl_globals_clean(void) __e_acsl_delete_block((void *)(& _B)); __e_acsl_delete_block((void *)(_A)); __e_acsl_delete_block((void *)(& _F)); + return; } int main(int argc, char **argv) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c index 66d885e493a..95604146d29 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c @@ -17,6 +17,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& errno)); + return; } int main(int argc, char const **argv) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c index ab2185597f8..5ec1eaf5bca 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c @@ -17,6 +17,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(array)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c index aa5bc854da2..3c3305ed098 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c @@ -16,6 +16,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& a)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c index c4eb1d146e1..30203990a80 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c @@ -20,6 +20,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& b)); __e_acsl_delete_block((void *)(& a)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c index dec94db6533..7359bae6a17 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c @@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& B)); __e_acsl_delete_block((void *)(& A)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c index 3fc0d11efa0..133b539e510 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c @@ -89,6 +89,7 @@ void __e_acsl_globals_clean(void) __e_acsl_delete_block((void *)(& S2)); __e_acsl_delete_block((void *)(& S)); __e_acsl_delete_block((void *)(& T)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c index bae0a768655..946ce35b056 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c @@ -26,6 +26,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& p)); __e_acsl_delete_block((void *)(& X)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c index 90041c6e180..efd908b7a93 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c @@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& PA)); __e_acsl_delete_block((void *)(A)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c index 9f802d1b7fc..94cdae153a1 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c @@ -37,6 +37,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& B)); __e_acsl_delete_block((void *)(& A)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c index 63d1db28971..b127d652e3c 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c @@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void) __e_acsl_delete_block((void *)(& stdout)); __e_acsl_delete_block((void *)(& stdin)); __e_acsl_delete_block((void *)(& stderr)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c index 872f31b112b..5a651806a48 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c @@ -142,6 +142,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& Z)); __e_acsl_delete_block((void *)(& X)); + return; } int main(void) diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c index 8b6f8a3517a..2d5749303a2 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c @@ -62,6 +62,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(Vertices2)); __e_acsl_delete_block((void *)(Vertices)); + return; } int main(int argc, char const **argv) diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c index a0774cc3429..e3bf8c116eb 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c @@ -21,6 +21,7 @@ void __e_acsl_globals_init(void) void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(& foo)); + return; } int main(int argc, char const **argv) diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c index c91eca2c101..4b7cbfa0412 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c @@ -118,6 +118,7 @@ void __e_acsl_globals_clean(void) __e_acsl_delete_block((void *)(& l_desc)); __e_acsl_delete_block((void *)(extra_lbits)); __e_acsl_delete_block((void *)(strings)); + return; } int main(int argc, char const **argv) diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c index 1b6b3cd7af3..6086892d5bd 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c @@ -110,6 +110,7 @@ void __e_acsl_globals_clean(void) { __e_acsl_delete_block((void *)(Str)); __e_acsl_delete_block((void *)(Strings)); + return; } int main(int argc, char const **argv) -- GitLab