diff --git a/src/plugins/e-acsl/tests/builtin/builtin_literal_string.c b/src/plugins/e-acsl/tests/builtin/builtin_literal_string.c new file mode 100644 index 0000000000000000000000000000000000000000..f50b2ef5aa6f6da615d210bf43c4ef02539f202b --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/builtin_literal_string.c @@ -0,0 +1,10 @@ +/* + Test literal string replacement in builtin arguments +*/ + +#include <string.h> + +int main() { + strlen("a cow"); + return 0; +} diff --git a/src/plugins/e-acsl/tests/builtin/builtin_literal_string_local_init.c b/src/plugins/e-acsl/tests/builtin/builtin_literal_string_local_init.c new file mode 100644 index 0000000000000000000000000000000000000000..8ca18d73b7844b17a9d70f15140f432bf4d57350 --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/builtin_literal_string_local_init.c @@ -0,0 +1,10 @@ +/* + Test literal string replacement in builtin arguments on a local init +*/ + +#include <string.h> + +int main() { + size_t len = strlen("a horse"); + return 0; +} diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624 --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string.res.oracle @@ -0,0 +1,2 @@ +[e-acsl] beginning translation. +[e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string_local_init.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string_local_init.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624 --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string_local_init.res.oracle @@ -0,0 +1,2 @@ +[e-acsl] beginning translation. +[e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string.c new file mode 100644 index 0000000000000000000000000000000000000000..e5950f81d786a1284cf59b6880c77f26070f06d2 --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string.c @@ -0,0 +1,30 @@ +/* Generated by Frama-C */ +#include "stddef.h" +#include "stdio.h" +#include "string.h" +char *__gen_e_acsl_literal_string; +void __e_acsl_globals_init(void) +{ + static char __e_acsl_already_run = 0; + if (! __e_acsl_already_run) { + __e_acsl_already_run = 1; + __gen_e_acsl_literal_string = "a cow"; + __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("a cow")); + __e_acsl_full_init((void *)__gen_e_acsl_literal_string); + __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string); + } + return; +} + +int main(void) +{ + int __retres; + __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8); + __e_acsl_globals_init(); + __e_acsl_builtin_strlen(__gen_e_acsl_literal_string); + __retres = 0; + __e_acsl_memory_clean(); + return __retres; +} + + diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string_local_init.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string_local_init.c new file mode 100644 index 0000000000000000000000000000000000000000..c3b9b764653aa7a972e75a909e458ba40db58700 --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string_local_init.c @@ -0,0 +1,31 @@ +/* Generated by Frama-C */ +#include "stddef.h" +#include "stdio.h" +#include "string.h" +char *__gen_e_acsl_literal_string; +void __e_acsl_globals_init(void) +{ + static char __e_acsl_already_run = 0; + if (! __e_acsl_already_run) { + __e_acsl_already_run = 1; + __gen_e_acsl_literal_string = "a horse"; + __e_acsl_store_block((void *)__gen_e_acsl_literal_string, + sizeof("a horse")); + __e_acsl_full_init((void *)__gen_e_acsl_literal_string); + __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string); + } + return; +} + +int main(void) +{ + int __retres; + __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8); + __e_acsl_globals_init(); + size_t len = __e_acsl_builtin_strlen(__gen_e_acsl_literal_string); + __retres = 0; + __e_acsl_memory_clean(); + return __retres; +} + + diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/builtin_literal_string.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/builtin_literal_string.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/builtin_literal_string_local_init.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/builtin_literal_string_local_init.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391