Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:25 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002303Frama-CPlug-in > E-ACSLpublic2017-12-06 09:10
Reporterevdenis 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon argument_names.c (80 bytes) 2017-05-29 12:56 -
    extern int test(int *);
    
    static inline int test2(int *a)
    {
       return test(a);
    }
    
    c file icon argument_names.c (80 bytes) 2017-05-29 12:56 +
  • patch file icon argument_names.patch (961 bytes) 2017-05-29 12:57 -
    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
    
    patch file icon argument_names.patch (961 bytes) 2017-05-29 12:57 +

-Relationships
+Relationships

-Notes

~0006469

signoles (manager)

Thanks for having reported this bug. It is fixed in the development version and the patch will be part of the next public release.
+Notes

-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
+Issue History