diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 49ca8b5c56c1fd21ab1c0327f93153cea87537fe..887096d1497b000c0d32ff5044f19dd768b75897 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -25,6 +25,8 @@ Plugin E-ACSL <next-release> ############################ +-* E-ACSL [2022-11-08] Fix clashing name when a function with contract and a + logic function have the same name (frama-c/eacsl#204) - E-ACSL [2022-11-08] Add support for functions returning a rational -* E-ACSL [2022-11-08] Fix assign clause and result as extra argument for functions returning a structure (frama-c/frama-c#1139) diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml index 861672fca4f8924e8b715a2947c25673ab164c1d..f4d829607802c9a7b5dae8a120efeb8bb531d150 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml +++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml @@ -495,7 +495,7 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs = fname in let gen_fname = - Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname) + Varname.get ~scope:Global (Functions.RTL.mk_gen_name fname) in let profile = Profile.make li.l_profile params_ival in let profile = Interval.get_widened_profile profile li in diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml index f28a37a3eb525a806a694efb4a6cfc7200ac0e5f..d3b9353faf697321bb3adfffba751e16d49373a2 100644 --- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml +++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml @@ -47,7 +47,9 @@ end = struct (* assume [vi] is not already in [tbl] *) let generate_vi vi = - let new_name = Functions.RTL.mk_gen_name vi.vname in + let new_name = Varname.get ~scope:Global + (Functions.RTL.mk_gen_name vi.vname) + in let new_vi = Cil.makeGlobalVar ~referenced:vi.vreferenced diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-204.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-204.c new file mode 100644 index 0000000000000000000000000000000000000000..9072e82aa2d5dc32ce0b674b61382594afe41935 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-204.c @@ -0,0 +1,16 @@ +/* + run.config + COMMENT: issue eacsl#204: name conflict when a function + COMMENT: with contract shares a name with a logic function +*/ + +/*@ predicate equalTag(integer n) = n; */ + +/*@ ensures equalTag(1); */ +int equalTag() { + return 1; +} + +int main(void) { + return 0; +} diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-204.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-204.c new file mode 100644 index 0000000000000000000000000000000000000000..09c27db7daec2c0235e179c11aa7c9110c8d01b0 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-204.c @@ -0,0 +1,66 @@ +/* Generated by Frama-C */ +#include "pthread.h" +#include "sched.h" +#include "signal.h" +#include "stddef.h" +#include "stdint.h" +#include "stdio.h" +#include "time.h" +extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; + +/*@ predicate equalTag(integer n) = n != 0; + +*/ +int __gen_e_acsl_equalTag_2(int n); + +/*@ ensures equalTag(1); */ +int __gen_e_acsl_equalTag(void); + +int equalTag(void) +{ + int __retres; + __retres = 1; + return __retres; +} + +int main(void) +{ + int __retres; + __e_acsl_memory_init((int *)0,(char ***)0,8UL); + __retres = 0; + __e_acsl_memory_clean(); + return __retres; +} + +/*@ ensures equalTag(1); */ +int __gen_e_acsl_equalTag(void) +{ + int __retres; + __retres = equalTag(); + { + int __gen_e_acsl_equalTag_3; + __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0}; + __gen_e_acsl_equalTag_3 = __gen_e_acsl_equalTag_2(1); + __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"equalTag(1)",0, + __gen_e_acsl_equalTag_3); + __gen_e_acsl_assert_data.blocking = 1; + __gen_e_acsl_assert_data.kind = "Postcondition"; + __gen_e_acsl_assert_data.pred_txt = "equalTag(1)"; + __gen_e_acsl_assert_data.file = "issue-eacsl-204.c"; + __gen_e_acsl_assert_data.fct = "equalTag"; + __gen_e_acsl_assert_data.line = 9; + __e_acsl_assert(__gen_e_acsl_equalTag_3,& __gen_e_acsl_assert_data); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data); + return __retres; + } +} + +/*@ assigns \result; + assigns \result \from n; */ +int __gen_e_acsl_equalTag_2(int n) +{ + int __retres = n != 0; + return __retres; +} + + diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-204.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-204.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624 --- /dev/null +++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-204.res.oracle @@ -0,0 +1,2 @@ +[e-acsl] beginning translation. +[e-acsl] translation done in project "e-acsl".