E-ACSL generates functions definitions without argument-names

ID0002303: This issue was created automatically from Mantis Issue 2303. Further discussion may take place here.

Id	Project	Category	View	Due Date	Updated
ID0002303	Frama-C	Plug-in > E-ACSL	public	2017-05-29	2017-12-06


Reporter	evdenis	Assigned To	signoles	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C 14-Silicon	Target Version	-	Fixed in Version	Frama-C 16-Sulfur

Description :

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; }

Additional Information :

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

Steps To Reproduce :

frama-c -main test2 -e-acsl-prepare -rte -rte-precond ./argument_names.c -then -e-acsl -then-last -print

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information