Skip to content

GitLab

Commit cb922698 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'libc_precond_naming' into 'master' 

Sync with frama-c/frama-c!1683

See merge request frama-c/e-acsl!195
parents 985696d9 f8df6960
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
View file @ cb922698
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
View file @ cb922698
......@@ -2,6 +2,6 @@
[e-acsl] warning: annotating undefined function `atoi':
the generated program may miss memory instrumentation
if there are memory-related annotations.
FRAMAC_SHARE/libc/stdlib.h:76:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdlib.h:78:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
View file @ cb922698
......@@ -15,30 +15,32 @@ tests/format/fprintf.c:24:[kernel:typing:incompatible-types-call] warning: expec
[e-acsl] warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
FRAMAC_SHARE/libc/stdio.h:146:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:152:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:154:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:340:[kernel] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:152:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:158:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:160:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:349:[kernel] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
tests/format/fprintf.c:12:[kernel] warning: Neither code nor specification for function strcpy, generating default assigns from the prototype
tests/format/fprintf.c:13:[kernel] warning: Neither code nor specification for function mktemp, generating default assigns from the prototype
tests/format/fprintf.c:17:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdlib.h:413:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:109:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:87:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdio.h:109:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:112:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:93:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:89:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..15] ∈ {0}
......@@ -100,40 +102,5 @@ tests/format/signalled.h:12:[kernel] warning: Neither code nor specification for
[value] using specification for function __e_acsl_delete_block
tests/format/fprintf.c:18:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
tests/format/fprintf.c:18:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
[value] using specification for function fopen
tests/format/fprintf.c:21:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
[value] using specification for function __e_acsl_valid
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/libc/stdio.h:87:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function fclose
tests/format/fprintf.c:23:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
tests/format/fprintf.c:24:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
tests/format/fprintf.c:24:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
[value] using specification for function remove
FRAMAC_SHARE/libc/stdio.h:70:[value] warning: no 'assigns \result \from ...' clause specified for function remove
tests/format/fprintf.c:31:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_dprintf
tests/format/fprintf.c:31:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
tests/format/fprintf.c:32:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
tests/format/fprintf.c:38:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_sprintf
tests/format/fprintf.c:38:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
tests/format/fprintf.c:39:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
tests/format/fprintf.c:40:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
tests/format/fprintf.c:41:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
tests/format/fprintf.c:41:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_9);
tests/format/fprintf.c:42:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
tests/format/fprintf.c:42:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_10);
tests/format/fprintf.c:45:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_snprintf
tests/format/fprintf.c:45:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_11);
tests/format/fprintf.c:46:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_12);
tests/format/fprintf.c:47:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
tests/format/fprintf.c:47:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_13);
tests/format/fprintf.c:48:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_14);
tests/format/fprintf.c:49:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
tests/format/fprintf.c:49:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_15);
tests/format/fprintf.c:50:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
tests/format/fprintf.c:50:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_16);
[value] using specification for function __e_acsl_memory_clean
tests/format/fprintf.c:19:[value:alarm] warning: function __gen_e_acsl_fopen: precondition 'valid_filename' got status invalid.
[value] done for function main
src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
View file @ cb922698
......@@ -328,7 +328,6 @@ int main(int argc, char const **argv)
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
waitpid(pid_1,& process_status_1,0);
/*@ assert Value: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,0,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_1));
}
......@@ -353,7 +352,6 @@ int main(int argc, char const **argv)
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
waitpid(pid_2,& process_status_2,0);
/*@ assert Value: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,1,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_2));
}
......@@ -378,7 +376,6 @@ int main(int argc, char const **argv)
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
waitpid(pid_3,& process_status_3,0);
/*@ assert Value: initialization: \initialized(&process_status_3); */
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_3));
}
......@@ -403,7 +400,6 @@ int main(int argc, char const **argv)
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
waitpid(pid_4,& process_status_4,0);
/*@ assert Value: initialization: \initialized(&process_status_4); */
signal_eval(process_status_4,0,__gen_e_acsl_literal_string_17);
__e_acsl_delete_block((void *)(& process_status_4));
}
......@@ -426,7 +422,6 @@ int main(int argc, char const **argv)
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
waitpid(pid_5,& process_status_5,0);
/*@ assert Value: initialization: \initialized(&process_status_5); */
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_18);
__e_acsl_delete_block((void *)(& process_status_5));
}
......@@ -450,7 +445,6 @@ int main(int argc, char const **argv)
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
waitpid(pid_6,& process_status_6,0);
/*@ assert Value: initialization: \initialized(&process_status_6); */
signal_eval(process_status_6,0,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_6));
}
......@@ -474,7 +468,6 @@ int main(int argc, char const **argv)
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
waitpid(pid_7,& process_status_7,0);
/*@ assert Value: initialization: \initialized(&process_status_7); */
signal_eval(process_status_7,0,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_7));
}
......@@ -498,7 +491,6 @@ int main(int argc, char const **argv)
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
waitpid(pid_8,& process_status_8,0);
/*@ assert Value: initialization: \initialized(&process_status_8); */
signal_eval(process_status_8,1,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_8));
}
......@@ -522,7 +514,6 @@ int main(int argc, char const **argv)
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
waitpid(pid_9,& process_status_9,0);
/*@ assert Value: initialization: \initialized(&process_status_9); */
signal_eval(process_status_9,1,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_9));
}
......@@ -546,7 +537,6 @@ int main(int argc, char const **argv)
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
waitpid(pid_10,& process_status_10,0);
/*@ assert Value: initialization: \initialized(&process_status_10); */
signal_eval(process_status_10,1,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_10));
}
......@@ -571,7 +561,6 @@ int main(int argc, char const **argv)
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
waitpid(pid_11,& process_status_11,0);
/*@ assert Value: initialization: \initialized(&process_status_11); */
signal_eval(process_status_11,0,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_11));
}
......@@ -596,7 +585,6 @@ int main(int argc, char const **argv)
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
waitpid(pid_12,& process_status_12,0);
/*@ assert Value: initialization: \initialized(&process_status_12); */
signal_eval(process_status_12,0,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_12));
}
......@@ -621,7 +609,6 @@ int main(int argc, char const **argv)
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
waitpid(pid_13,& process_status_13,0);
/*@ assert Value: initialization: \initialized(&process_status_13); */
signal_eval(process_status_13,1,__gen_e_acsl_literal_string_30);
__e_acsl_delete_block((void *)(& process_status_13));
}
......@@ -646,7 +633,6 @@ int main(int argc, char const **argv)
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
waitpid(pid_14,& process_status_14,0);
/*@ assert Value: initialization: \initialized(&process_status_14); */
signal_eval(process_status_14,1,__gen_e_acsl_literal_string_31);
__e_acsl_delete_block((void *)(& process_status_14));
}
......@@ -671,7 +657,6 @@ int main(int argc, char const **argv)
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
waitpid(pid_15,& process_status_15,0);
/*@ assert Value: initialization: \initialized(&process_status_15); */
signal_eval(process_status_15,1,__gen_e_acsl_literal_string_32);
__e_acsl_delete_block((void *)(& process_status_15));
}
......@@ -696,7 +681,6 @@ int main(int argc, char const **argv)
int process_status_16;
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
waitpid(pid_16,& process_status_16,0);
/*@ assert Value: initialization: \initialized(&process_status_16); */
signal_eval(process_status_16,0,__gen_e_acsl_literal_string_33);
__e_acsl_delete_block((void *)(& process_status_16));
}
......
src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
View file @ cb922698
......@@ -15,46 +15,46 @@ tests/format/printf.c:88:[kernel] warning: Floating-point constant 0.2 is not re
[e-acsl] warning: annotating undefined function `strcpy':
the generated program may miss memory instrumentation
if there are memory-related annotations.
FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/unistd.h:785:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/unistd.h:780:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
FRAMAC_SHARE/libc/string.h:309:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
FRAMAC_SHARE/libc/string.h:317:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:310:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:312:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:312:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/string.h:318:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:320:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:320:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:315:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
FRAMAC_SHARE/libc/string.h:323:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:140:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
FRAMAC_SHARE/libc/string.h:143:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:153:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/string.h:157:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:143:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
FRAMAC_SHARE/libc/string.h:146:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:143:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
FRAMAC_SHARE/libc/string.h:146:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:150:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
FRAMAC_SHARE/libc/string.h:153:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:108:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
FRAMAC_SHARE/libc/string.h:111:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:108:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/string.h:111:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:110:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
FRAMAC_SHARE/libc/string.h:113:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:110:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/string.h:113:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
FRAMAC_SHARE/libc/stdlib.h:406:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
View file @ cb922698
......@@ -6,8 +6,8 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
View file @ cb922698
......@@ -6,8 +6,8 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
View file @ cb922698
......@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__fc_rand_max ∈ {32767}
__e_acsl_init ∈ [--..--]
__fc_fopen[0..15] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
......
Markdown is supported
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