diff --git a/src/plugins/e-acsl/tests/runtime/constmerge.c b/src/plugins/e-acsl/tests/runtime/constmerge.c new file mode 100644 index 0000000000000000000000000000000000000000..c38e39aa567130b6d0ae0320a444bfb89be696e9 --- /dev/null +++ b/src/plugins/e-acsl/tests/runtime/constmerge.c @@ -0,0 +1,16 @@ +/* run.config + COMMENT: separate tracking of string constants +*/ + +const char *f = "the cat"; +const char *s = "the dog and the cat"; + +#include <stdlib.h> + +char *strdup(const char*); + +int main(int argc, const char **argv) { + s++; + f++; + return 0; +} diff --git a/src/plugins/e-acsl/tests/runtime/oracle/constmerge.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/constmerge.err.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..b9986aac7753fbec86bfada42c891e07f97c800e --- /dev/null +++ b/src/plugins/e-acsl/tests/runtime/oracle/constmerge.res.oracle @@ -0,0 +1,3 @@ +[e-acsl] beginning translation. +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/runtime/oracle/gen_constmerge.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_constmerge.c new file mode 100644 index 0000000000000000000000000000000000000000..6d8a7d8d387238c86a3fae99b6ce0e97c4150df2 --- /dev/null +++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_constmerge.c @@ -0,0 +1,38 @@ +/* Generated by Frama-C */ +char *__gen_e_acsl_literal_string_2; +char *__gen_e_acsl_literal_string; +char const *f = "the cat"; +char const *s = "the dog and the cat"; +void __e_acsl_globals_init(void) +{ + __gen_e_acsl_literal_string_2 = "the dog and the cat"; + __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2, + sizeof("the dog and the cat")); + __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2); + __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2); + __gen_e_acsl_literal_string = "the cat"; + __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("the cat")); + __e_acsl_full_init((void *)__gen_e_acsl_literal_string); + __e_acsl_readonly((void *)__gen_e_acsl_literal_string); + __e_acsl_store_block((void *)(& s),8UL); + __e_acsl_full_init((void *)(& s)); + __e_acsl_store_block((void *)(& f),8UL); + __e_acsl_full_init((void *)(& f)); + return; +} + +int main(int argc, char const **argv) +{ + int __retres; + __e_acsl_memory_init(& argc,(char ***)(& argv),8UL); + __e_acsl_globals_init(); + s ++; + f ++; + __retres = 0; + __e_acsl_delete_block((void *)(& s)); + __e_acsl_delete_block((void *)(& f)); + __e_acsl_memory_clean(); + return __retres; +} + +