diff --git a/src/plugins/e-acsl/tests/bts/bts2192.c b/src/plugins/e-acsl/tests/bts/bts2192.c new file mode 100644 index 0000000000000000000000000000000000000000..89fdf25dae7c6b6d6b4d689aed8290c512d03591 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/bts2192.c @@ -0,0 +1,11 @@ +/* run.config + COMMENT: bts #2292, failures due to unregistered RTL functions +*/ + +#include <stdlib.h> + +int a; +char *n = "134"; +int main(int argc, char **argv) { + a = argc = atoi(n); +} diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.err.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..d122567f6583309acc9703cf00c437ed641072bc --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle @@ -0,0 +1,6 @@ +[e-acsl] beginning translation. +[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:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype +[e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c new file mode 100644 index 0000000000000000000000000000000000000000..85c23235916158fddcad4495bb80c30b6aefa8eb --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c @@ -0,0 +1,15 @@ +/* Generated by Frama-C */ +int a; +char *n = (char *)"134"; +int main(int argc, char **argv) +{ + int __retres; + { /* sequence */ + argc = __gen_e_acsl_atoi((char const *)n); + a = argc; + } + __retres = 0; + return __retres; +} + +