Frama-C Bug Tracking System - Frama-C
View Issue Details
0002303Frama-CPlug-in > E-ACSLpublic2017-05-29 12:562017-12-06 09:10
evdenis 
signoles 
normalmajoralways
closedfixed 
Frama-C 14-Silicon 
Frama-C 16-Sulfur 
0002303: E-ACSL generates functions definitions without argument-names
Test: extern int test(int *); static inline int test2(int *a) { return test(a); } Output: ... /*@ predicate diffSize{L1, L2}(ℤ i) = \at(__e_acsl_heap_allocation_size,L1) - \at(__e_acsl_heap_allocation_size,L2) ≡ i; */ /*@ assigns \result; assigns \result \from \nothing; */ int __gen_e_acsl_test(int *); /*@ assigns \result; assigns \result \from \nothing; */ extern int test(int *); ... /*@ assigns \result; assigns \result \from \nothing; */ int __gen_e_acsl_test(int *) // <== ERROR { int __retres; __retres = test(); return __retres; }
frama-c -main test2 -e-acsl-prepare -rte -rte-precond ./argument_names.c -then -e-acsl -then-last -print
Possible fix: diff --git a/dup_functions.ml b/dup_functions.ml index e87ce02..d447353 100644 --- a/dup_functions.ml +++ b/dup_functions.ml @@ -157,10 +157,22 @@ let dup_funspec tbl bhv spec = end in Cil.visitCilFunspec o spec + +let gen_name name idnum = + if name = "" + then + let id = idnum + 1 in + ("__e_acsl_tmp_var_" ^ string_of_int (id), id) + else + (name, idnum) + let dup_fundec loc spec bhv kf vi new_vi = new_vi.vdefined <- true; let formals = Kernel_function.get_formals kf in - let new_formals = List.map (fun vi -> Cil.copyVarinfo vi vi.vname) formals in + let idnum : int ref = ref 0 in + let new_formals = List.map (fun vi -> let (name, id) = gen_name vi.vname !idnum in + (idnum := id); + Cil.copyVarinfo vi name) formals in let res = let ty = Kernel_function.get_return_type kf in if Cil.isVoidType ty then None
No tags attached.
c argument_names.c (80) 2017-05-29 12:56
https://bts.frama-c.com/file_download.php?file_id=1179&type=bug
patch argument_names.patch (961) 2017-05-29 12:57
https://bts.frama-c.com/file_download.php?file_id=1180&type=bug
Issue History
2017-05-29 12:56evdenisNew Issue
2017-05-29 12:56evdenisStatusnew => assigned
2017-05-29 12:56evdenisAssigned To => signoles
2017-05-29 12:56evdenisFile Added: argument_names.c
2017-05-29 12:57evdenisFile Added: argument_names.patch
2017-05-29 13:36signolesAssigned Tosignoles => kvorobyov
2017-10-24 17:42signolesAssigned Tokvorobyov => signoles
2017-10-25 16:00signolesNote Added: 0006469
2017-10-25 16:00signolesStatusassigned => resolved
2017-10-25 16:00signolesFixed in Version => Frama-C 16-Sulfur
2017-10-25 16:00signolesResolutionopen => fixed
2017-12-06 09:10signolesStatusresolved => closed

Notes
(0006469)
signoles   
2017-10-25 16:00   
Thanks for having reported this bug. It is fixed in the development version and the patch will be part of the next public release.