diff --git a/src/plugins/e-acsl/tests/bts/bts2191.c b/src/plugins/e-acsl/tests/bts/bts2191.c index 0291959acba483a0cff69a91a42ae4f5bec4c6eb..8ce8acf7fa83169d40763aed125cca1b7817f8a8 100644 --- a/src/plugins/e-acsl/tests/bts/bts2191.c +++ b/src/plugins/e-acsl/tests/bts/bts2191.c @@ -1,3 +1,7 @@ +/* run.config + COMMENT: bts #2191, issue with unrolling types of struct members +*/ + struct ST { char *str; int num; 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_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c index 25a3068c5ea0f9f587f8b14c4fdc09d1f72ba492..a4f6f4a9c2cfbf191e30a185bfd32af30ee89ef6 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c @@ -44,7 +44,7 @@ int main(int argc, char **argv) } else __gen_e_acsl_and = 0; __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main", - (char *)"\\valid_read(_G[0].str)",18); + (char *)"\\valid_read(_G[0].str)",22); } __retres = 0; __e_acsl_delete_block((void *)(_G)); 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; +} + +