Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002303Frama-CPlug-in > E-ACSLpublic2017-05-29 12:562017-12-06 09:10
Reporterevdenis 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in VersionFrama-C 16-Sulfur 
Summary0002303: E-ACSL generates functions definitions without argument-names
DescriptionTest: 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; }
Steps To Reproduceframa-c -main test2 -e-acsl-prepare -rte -rte-precond ./argument_names.c -then -e-acsl -then-last -print
Additional InformationPossible 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
TagsNo tags attached.
Attached Filesc file icon argument_names.c [^] (80 bytes) 2017-05-29 12:56 [Show Content]
patch file icon argument_names.patch [^] (961 bytes) 2017-05-29 12:57 [Show Content]

- Relationships

-  Notes
(0006469)
signoles (manager)
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.

- Issue History
Date Modified Username Field Change
2017-05-29 12:56 evdenis New Issue
2017-05-29 12:56 evdenis Status new => assigned
2017-05-29 12:56 evdenis Assigned To => signoles
2017-05-29 12:56 evdenis File Added: argument_names.c
2017-05-29 12:57 evdenis File Added: argument_names.patch
2017-05-29 13:36 signoles Assigned To signoles => kvorobyov
2017-10-24 17:42 signoles Assigned To kvorobyov => signoles
2017-10-25 16:00 signoles Note Added: 0006469
2017-10-25 16:00 signoles Status assigned => resolved
2017-10-25 16:00 signoles Fixed in Version => Frama-C 16-Sulfur
2017-10-25 16:00 signoles Resolution open => fixed
2017-12-06 09:10 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker