Skip to content
Snippets Groups Projects
Commit bc5de85e authored by Thibaut Benjamin's avatar Thibaut Benjamin
Browse files

[e-acsl] update oracles

parent 64a2dca5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+ 27
− 25
View file @ bc5de85e
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] functions.c:70: Warning: [e-acsl] functions.c:73: Warning:
E-ACSL construct `function application' is not yet supported. E-ACSL construct `function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] functions.c:48: Warning: [eva:alarm] functions.c:51: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:48: Warning: [eva:alarm] functions.c:51: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:50: Warning: [eva:alarm] functions.c:53: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:52: Warning: [eva:alarm] functions.c:55: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:52: Warning: [eva:alarm] functions.c:55: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null || function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:53: Warning: [eva:alarm] functions.c:56: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:53: Warning: [eva:alarm] functions.c:56: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:54: Warning: [eva:alarm] functions.c:57: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:55: Warning: [eva:alarm] functions.c:58: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:60: Warning: [eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:60: Warning: [eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:63: Warning: [eva:alarm] functions.c:66: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null || function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:63: Warning: [eva:alarm] functions.c:66: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null || function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:65: Warning: [eva:alarm] functions.c:68: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null || function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:65: Warning: [eva:alarm] functions.c:68: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null || function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:70: Warning: [eva:alarm] functions.c:73: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null || function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:70: Warning: [eva:alarm] functions.c:73: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null || function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:70: Warning: assertion got status unknown. [eva:alarm] functions.c:73: Warning: assertion got status unknown.
[eva:alarm] functions.c:71: Warning: [eva:alarm] functions.c:74: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null || function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:71: Warning: [eva:alarm] functions.c:74: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null || function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:28: Warning: [eva:alarm] functions.c:28: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null || function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:76: Warning: [eva:alarm] functions.c:79: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9); non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] functions.c:76: Warning: [eva:alarm] functions.c:79: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null || function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown. \valid(data->values) got status unknown.
[eva:alarm] functions.c:76: Warning: [eva:alarm] functions.c:79: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:81: Warning: assertion got status unknown.
[eva:alarm] functions.c:83: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown. function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:78: Warning: assertion got status unknown.
src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+ 86
− 22
View file @ bc5de85e
...@@ -57,7 +57,7 @@ int __gen_e_acsl_g(int x); ...@@ -57,7 +57,7 @@ int __gen_e_acsl_g(int x);
/*@ logic mystruct t1(mystruct m) = m; /*@ logic mystruct t1(mystruct m) = m;
*/ */
mystruct __gen_e_acsl_t1(mystruct m); void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m);
/*@ logic integer t2(mystruct m) = m.k + m.l; /*@ logic integer t2(mystruct m) = m.k + m.l;
*/ */
...@@ -88,9 +88,13 @@ double __gen_e_acsl_f2(double x); ...@@ -88,9 +88,13 @@ double __gen_e_acsl_f2(double x);
/*@ logic integer f_notyet{L}(integer x) = x; /*@ logic integer f_notyet{L}(integer x) = x;
*/ */
/*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1); /*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
*/
int __gen_e_acsl_f_sum(int x);
/*@ logic real over(real a, real b) = a / b;
*/ */
int __gen_e_acsl_f_sum(int x); void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b);
int main(void) int main(void)
{ {
...@@ -112,7 +116,7 @@ int main(void) ...@@ -112,7 +116,7 @@ int main(void)
__gen_e_acsl_assert_data.pred_txt = "p1(x, y)"; __gen_e_acsl_assert_data.pred_txt = "p1(x, y)";
__gen_e_acsl_assert_data.file = "functions.c"; __gen_e_acsl_assert_data.file = "functions.c";
__gen_e_acsl_assert_data.fct = "main"; __gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 48; __gen_e_acsl_assert_data.line = 51;
__e_acsl_assert(__gen_e_acsl_p1_2,& __gen_e_acsl_assert_data); __e_acsl_assert(__gen_e_acsl_p1_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data); __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
} }
...@@ -129,7 +133,7 @@ int main(void) ...@@ -129,7 +133,7 @@ int main(void)
__gen_e_acsl_assert_data_2.pred_txt = "p2(3, 4)"; __gen_e_acsl_assert_data_2.pred_txt = "p2(3, 4)";
__gen_e_acsl_assert_data_2.file = "functions.c"; __gen_e_acsl_assert_data_2.file = "functions.c";
__gen_e_acsl_assert_data_2.fct = "main"; __gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 49; __gen_e_acsl_assert_data_2.line = 52;
__e_acsl_assert(__gen_e_acsl_p2_2,& __gen_e_acsl_assert_data_2); __e_acsl_assert(__gen_e_acsl_p2_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
} }
...@@ -150,7 +154,7 @@ int main(void) ...@@ -150,7 +154,7 @@ int main(void)
__gen_e_acsl_assert_data_3.pred_txt = "p2(5, 99999999999999999999999999999)"; __gen_e_acsl_assert_data_3.pred_txt = "p2(5, 99999999999999999999999999999)";
__gen_e_acsl_assert_data_3.file = "functions.c"; __gen_e_acsl_assert_data_3.file = "functions.c";
__gen_e_acsl_assert_data_3.fct = "main"; __gen_e_acsl_assert_data_3.fct = "main";
__gen_e_acsl_assert_data_3.line = 50; __gen_e_acsl_assert_data_3.line = 53;
__e_acsl_assert(__gen_e_acsl_p2_4,& __gen_e_acsl_assert_data_3); __e_acsl_assert(__gen_e_acsl_p2_4,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_); __gmpz_clear(__gen_e_acsl_);
...@@ -170,7 +174,7 @@ int main(void) ...@@ -170,7 +174,7 @@ int main(void)
__gen_e_acsl_assert_data_4.pred_txt = "f1(x, y) == 3"; __gen_e_acsl_assert_data_4.pred_txt = "f1(x, y) == 3";
__gen_e_acsl_assert_data_4.file = "functions.c"; __gen_e_acsl_assert_data_4.file = "functions.c";
__gen_e_acsl_assert_data_4.fct = "main"; __gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 52; __gen_e_acsl_assert_data_4.line = 55;
__e_acsl_assert(__gen_e_acsl_f1_2 == 3L,& __gen_e_acsl_assert_data_4); __e_acsl_assert(__gen_e_acsl_f1_2 == 3L,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
} }
...@@ -192,7 +196,7 @@ int main(void) ...@@ -192,7 +196,7 @@ int main(void)
__gen_e_acsl_assert_data_5.pred_txt = "p2(x, f1(3, 4))"; __gen_e_acsl_assert_data_5.pred_txt = "p2(x, f1(3, 4))";
__gen_e_acsl_assert_data_5.file = "functions.c"; __gen_e_acsl_assert_data_5.file = "functions.c";
__gen_e_acsl_assert_data_5.fct = "main"; __gen_e_acsl_assert_data_5.fct = "main";
__gen_e_acsl_assert_data_5.line = 53; __gen_e_acsl_assert_data_5.line = 56;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5); __e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
} }
...@@ -218,7 +222,7 @@ int main(void) ...@@ -218,7 +222,7 @@ int main(void)
__gen_e_acsl_assert_data_6.pred_txt = "f1(9, 99999999999999999999999999999) > 0"; __gen_e_acsl_assert_data_6.pred_txt = "f1(9, 99999999999999999999999999999) > 0";
__gen_e_acsl_assert_data_6.file = "functions.c"; __gen_e_acsl_assert_data_6.file = "functions.c";
__gen_e_acsl_assert_data_6.fct = "main"; __gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 54; __gen_e_acsl_assert_data_6.line = 57;
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,& __gen_e_acsl_assert_data_6); __e_acsl_assert(__gen_e_acsl_gt_2 > 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__gmpz_clear(__gen_e_acsl__3); __gmpz_clear(__gen_e_acsl__3);
...@@ -249,7 +253,7 @@ int main(void) ...@@ -249,7 +253,7 @@ int main(void)
__gen_e_acsl_assert_data_7.pred_txt = "f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998"; __gen_e_acsl_assert_data_7.pred_txt = "f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998";
__gen_e_acsl_assert_data_7.file = "functions.c"; __gen_e_acsl_assert_data_7.file = "functions.c";
__gen_e_acsl_assert_data_7.fct = "main"; __gen_e_acsl_assert_data_7.fct = "main";
__gen_e_acsl_assert_data_7.line = 55; __gen_e_acsl_assert_data_7.line = 58;
__e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data_7); __e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gmpz_clear(__gen_e_acsl__5); __gmpz_clear(__gen_e_acsl__5);
...@@ -275,7 +279,7 @@ int main(void) ...@@ -275,7 +279,7 @@ int main(void)
__gen_e_acsl_assert_data_8.pred_txt = "g(x) == x"; __gen_e_acsl_assert_data_8.pred_txt = "g(x) == x";
__gen_e_acsl_assert_data_8.file = "functions.c"; __gen_e_acsl_assert_data_8.file = "functions.c";
__gen_e_acsl_assert_data_8.fct = "main"; __gen_e_acsl_assert_data_8.fct = "main";
__gen_e_acsl_assert_data_8.line = 60; __gen_e_acsl_assert_data_8.line = 63;
__e_acsl_assert(__gen_e_acsl_g_2 == x,& __gen_e_acsl_assert_data_8); __e_acsl_assert(__gen_e_acsl_g_2 == x,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
} }
...@@ -295,7 +299,7 @@ int main(void) ...@@ -295,7 +299,7 @@ int main(void)
__gen_e_acsl_assert_data_9.pred_txt = "h_char(c) == c"; __gen_e_acsl_assert_data_9.pred_txt = "h_char(c) == c";
__gen_e_acsl_assert_data_9.file = "functions.c"; __gen_e_acsl_assert_data_9.file = "functions.c";
__gen_e_acsl_assert_data_9.fct = "main"; __gen_e_acsl_assert_data_9.fct = "main";
__gen_e_acsl_assert_data_9.line = 63; __gen_e_acsl_assert_data_9.line = 66;
__e_acsl_assert((int)__gen_e_acsl_h_char_2 == (int)c, __e_acsl_assert((int)__gen_e_acsl_h_char_2 == (int)c,
& __gen_e_acsl_assert_data_9); & __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
...@@ -316,7 +320,7 @@ int main(void) ...@@ -316,7 +320,7 @@ int main(void)
__gen_e_acsl_assert_data_10.pred_txt = "h_short(s) == s"; __gen_e_acsl_assert_data_10.pred_txt = "h_short(s) == s";
__gen_e_acsl_assert_data_10.file = "functions.c"; __gen_e_acsl_assert_data_10.file = "functions.c";
__gen_e_acsl_assert_data_10.fct = "main"; __gen_e_acsl_assert_data_10.fct = "main";
__gen_e_acsl_assert_data_10.line = 65; __gen_e_acsl_assert_data_10.line = 68;
__e_acsl_assert((int)__gen_e_acsl_h_short_2 == (int)s, __e_acsl_assert((int)__gen_e_acsl_h_short_2 == (int)s,
& __gen_e_acsl_assert_data_10); & __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
...@@ -329,7 +333,7 @@ int main(void) ...@@ -329,7 +333,7 @@ int main(void)
mystruct __gen_e_acsl_t1_2; mystruct __gen_e_acsl_t1_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 = __e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0}; {.values = (void *)0};
__gen_e_acsl_t1_2 = __gen_e_acsl_t1(m); __gen_e_acsl_t1(& __gen_e_acsl_t1_2,m);
__gen_e_acsl_r = __gen_e_acsl_t1_2; __gen_e_acsl_r = __gen_e_acsl_t1_2;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,"r.k",0, __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,"r.k",0,
__gen_e_acsl_r.k); __gen_e_acsl_r.k);
...@@ -340,7 +344,7 @@ int main(void) ...@@ -340,7 +344,7 @@ int main(void)
__gen_e_acsl_assert_data_11.pred_txt = "\\let r = t1(m); r.k == 8"; __gen_e_acsl_assert_data_11.pred_txt = "\\let r = t1(m); r.k == 8";
__gen_e_acsl_assert_data_11.file = "functions.c"; __gen_e_acsl_assert_data_11.file = "functions.c";
__gen_e_acsl_assert_data_11.fct = "main"; __gen_e_acsl_assert_data_11.fct = "main";
__gen_e_acsl_assert_data_11.line = 70; __gen_e_acsl_assert_data_11.line = 73;
__e_acsl_assert(__gen_e_acsl_r.k == 8,& __gen_e_acsl_assert_data_11); __e_acsl_assert(__gen_e_acsl_r.k == 8,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
} }
...@@ -350,7 +354,7 @@ int main(void) ...@@ -350,7 +354,7 @@ int main(void)
long __gen_e_acsl_t2_2; long __gen_e_acsl_t2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 = __e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0}; {.values = (void *)0};
__gen_e_acsl_t1_4 = __gen_e_acsl_t1(m); __gen_e_acsl_t1(& __gen_e_acsl_t1_4,m);
__gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_4); __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_4);
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"m"); __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"m");
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"t1(m)"); __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"t1(m)");
...@@ -361,7 +365,7 @@ int main(void) ...@@ -361,7 +365,7 @@ int main(void)
__gen_e_acsl_assert_data_12.pred_txt = "t2(t1(m)) == 17"; __gen_e_acsl_assert_data_12.pred_txt = "t2(t1(m)) == 17";
__gen_e_acsl_assert_data_12.file = "functions.c"; __gen_e_acsl_assert_data_12.file = "functions.c";
__gen_e_acsl_assert_data_12.fct = "main"; __gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 71; __gen_e_acsl_assert_data_12.line = 74;
__e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_12); __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
} }
...@@ -381,7 +385,7 @@ int main(void) ...@@ -381,7 +385,7 @@ int main(void)
__gen_e_acsl_assert_data_13.pred_txt = "f2(d) > 0"; __gen_e_acsl_assert_data_13.pred_txt = "f2(d) > 0";
__gen_e_acsl_assert_data_13.file = "functions.c"; __gen_e_acsl_assert_data_13.file = "functions.c";
__gen_e_acsl_assert_data_13.fct = "main"; __gen_e_acsl_assert_data_13.fct = "main";
__gen_e_acsl_assert_data_13.line = 76; __gen_e_acsl_assert_data_13.line = 79;
__e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_13); __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
} }
...@@ -398,12 +402,48 @@ int main(void) ...@@ -398,12 +402,48 @@ int main(void)
__gen_e_acsl_assert_data_14.pred_txt = "f_sum(100) == 100"; __gen_e_acsl_assert_data_14.pred_txt = "f_sum(100) == 100";
__gen_e_acsl_assert_data_14.file = "functions.c"; __gen_e_acsl_assert_data_14.file = "functions.c";
__gen_e_acsl_assert_data_14.fct = "main"; __gen_e_acsl_assert_data_14.fct = "main";
__gen_e_acsl_assert_data_14.line = 78; __gen_e_acsl_assert_data_14.line = 81;
__e_acsl_assert(__gen_e_acsl_f_sum_2 == 100, __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
& __gen_e_acsl_assert_data_14); & __gen_e_acsl_assert_data_14);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_14); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
} }
/*@ assert f_sum(100) == 100; */ ; /*@ assert f_sum(100) == 100; */ ;
{
__e_acsl_mpq_t __gen_e_acsl_over_2;
__e_acsl_mpq_t __gen_e_acsl__11;
__e_acsl_mpq_t __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl_div_3;
int __gen_e_acsl_eq_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_15 =
{.values = (void *)0};
__gen_e_acsl_over(& __gen_e_acsl_over_2,1.,2.);
__gmpq_init(__gen_e_acsl__11);
__gmpq_set_d(__gen_e_acsl__11,1.);
__gmpq_init(__gen_e_acsl__12);
__gmpq_set_d(__gen_e_acsl__12,2.);
__gmpq_init(__gen_e_acsl_div_3);
__gmpq_div(__gen_e_acsl_div_3,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__11),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__12));
__gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div_3));
__e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data_15,
"over(1., 2.)",
(__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2));
__gen_e_acsl_assert_data_15.blocking = 1;
__gen_e_acsl_assert_data_15.kind = "Assertion";
__gen_e_acsl_assert_data_15.pred_txt = "over(1., 2.) == 1. / 2.";
__gen_e_acsl_assert_data_15.file = "functions.c";
__gen_e_acsl_assert_data_15.fct = "main";
__gen_e_acsl_assert_data_15.line = 83;
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_15);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
__gmpq_clear(__gen_e_acsl_over_2);
__gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__12);
__gmpq_clear(__gen_e_acsl_div_3);
}
/*@ assert over(1., 2.) == 1. / 2.; */ ;
__retres = 0; __retres = 0;
__e_acsl_memory_clean(); __e_acsl_memory_clean();
return __retres; return __retres;
...@@ -561,11 +601,12 @@ int __gen_e_acsl_g(int x) ...@@ -561,11 +601,12 @@ int __gen_e_acsl_g(int x)
return __gen_e_acsl_g_hidden_2; return __gen_e_acsl_g_hidden_2;
} }
/*@ assigns \result; /*@ assigns __retres_arg;
assigns \result \from m; */ assigns __retres_arg \from m; */
mystruct __gen_e_acsl_t1(mystruct m) void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m)
{ {
return m; *__retres_arg = m;
return;
} }
/*@ assigns \result; /*@ assigns \result;
...@@ -633,4 +674,27 @@ int __gen_e_acsl_f_sum(int x) ...@@ -633,4 +674,27 @@ int __gen_e_acsl_f_sum(int x)
return __gen_e_acsl_accumulator; return __gen_e_acsl_accumulator;
} }
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from a, b; */
void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b)
{
__e_acsl_mpq_t __gen_e_acsl_b;
__e_acsl_mpq_t __gen_e_acsl__10;
__e_acsl_mpq_t __gen_e_acsl_div_2;
__gmpq_init(__gen_e_acsl_b);
__gmpq_set_d(__gen_e_acsl_b,b);
__gmpq_init(__gen_e_acsl__10);
__gmpq_set_d(__gen_e_acsl__10,a);
__gmpq_init(__gen_e_acsl_div_2);
__gmpq_div(__gen_e_acsl_div_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__10),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
__gmpq_init(*__retres_arg);
__gmpq_set(*__retres_arg,(__e_acsl_mpq_struct const *)(__gen_e_acsl_div_2));
__gmpq_clear(__gen_e_acsl_b);
__gmpq_clear(__gen_e_acsl__10);
__gmpq_clear(__gen_e_acsl_div_2);
return;
}
src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+ 7
− 6
View file @ bc5de85e
...@@ -58,7 +58,7 @@ int __gen_e_acsl_g(int x); ...@@ -58,7 +58,7 @@ int __gen_e_acsl_g(int x);
/*@ logic mystruct t1(mystruct m) = m; /*@ logic mystruct t1(mystruct m) = m;
*/ */
mystruct __gen_e_acsl_t1(mystruct m); void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m);
/*@ logic integer t2(mystruct m) = m.k + m.l; /*@ logic integer t2(mystruct m) = m.k + m.l;
*/ */
...@@ -378,7 +378,7 @@ int main(void) ...@@ -378,7 +378,7 @@ int main(void)
int __gen_e_acsl_eq_6; int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 = __e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0}; {.values = (void *)0};
__gen_e_acsl_t1_2 = __gen_e_acsl_t1(m); __gen_e_acsl_t1(& __gen_e_acsl_t1_2,m);
__gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2); __gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
__gmpz_init_set_si(__gen_e_acsl__16,17L); __gmpz_init_set_si(__gen_e_acsl__16,17L);
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2), __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2),
...@@ -657,11 +657,12 @@ int __gen_e_acsl_g(int x) ...@@ -657,11 +657,12 @@ int __gen_e_acsl_g(int x)
return __gen_e_acsl_g_hidden_2; return __gen_e_acsl_g_hidden_2;
} }
/*@ assigns \result; /*@ assigns __retres_arg;
assigns \result \from m; */ assigns __retres_arg \from m; */
mystruct __gen_e_acsl_t1(mystruct m) void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m)
{ {
return m; *__retres_arg = m;
return;
} }
/*@ assigns (*__retres_arg)[0]; /*@ assigns (*__retres_arg)[0];
......
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