diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c index 9dba1dbedad2cfc282b45e6ac8af4ca5398012be..1bf6931b3419cd8216a32e4081f39286c417a3f3 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c +++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c @@ -221,6 +221,12 @@ void __gen_e_acsl_k(int x) return; } +char __gen_e_acsl_h_char(int c) +{ + char __retres = (char)c; + return __retres; +} + short __gen_e_acsl_h_short(int s) { short __retres = (short)s; @@ -348,10 +354,4 @@ long __gen_e_acsl_f1(int x, int y) return __retres; } -char __gen_e_acsl_h_char(int c) -{ - char __retres = (char)c; - return __retres; -} - diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c index bdacabaaf9c83e4b21bc9a291510c57190f32bc0..9989adf5ca2bee1aad2ee77c8cb647276dbd3573 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c +++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c @@ -266,6 +266,12 @@ void __gen_e_acsl_k(int x) return; } +char __gen_e_acsl_h_char(int c) +{ + char __retres = (char)c; + return __retres; +} + short __gen_e_acsl_h_short(int s) { short __retres = (short)s; @@ -440,10 +446,4 @@ void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y) return; } -char __gen_e_acsl_h_char(int c) -{ - char __retres = (char)c; - return __retres; -} -