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 - 2018 MantisBT Team
Powered by Mantis Bugtracker