diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 0deac191f99cfd33e930bb3e9e19085a1e490fc3..170c27994b15ebdbcbeefa791402180bc3f6bf22 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -227,6 +227,18 @@ type position = Before_gmp | Gmp | After_gmp | Memory_model | Code
class dup_functions_visitor prj = object (self)
inherit Visitor.frama_c_copy prj
+ val unduplicable_functions =
+ let white_list =
+ [ "__builtin_va_arg";
+ "__builtin_va_end";
+ "__builtin_va_start";
+ "__builtin_va_copy" ]
+ in
+ List.fold_left
+ (fun acc s -> Datatype.String.Set.add s acc)
+ Datatype.String.Set.empty
+ white_list
+
val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
val mutable before_memory_model = Before_gmp
val mutable new_definitions: global list = []
@@ -288,25 +300,27 @@ class dup_functions_visitor prj = object (self)
| GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
when (* duplicate a function iff: *)
not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
- (* it is not already duplicated *)
+ (* it is not already duplicated *)
+ && not (Datatype.String.Set.mem vi.vname unduplicable_functions)
+ (* it is duplicable *)
&& self#is_unvariadic_function vi (* it is not a variadic function *)
- && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
- && not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
- &&
- (let kf =
- try Globals.Functions.get vi with Not_found -> assert false
- in
- not (Functions.instrument kf)
+ && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
+ && not (Cil.is_builtin vi) (* it is not a Frama-C built-in *)
+ &&
+ (let kf =
+ try Globals.Functions.get vi with Not_found -> assert false
+ in
+ not (Functions.instrument kf)
(* either explicitely listed as to be not instrumented *)
||
(* or: *)
- (not (Cil.is_empty_funspec
- (Annotations.funspec ~populate:false
- (Extlib.the self#current_kf)))
+ (not (Cil.is_empty_funspec
+ (Annotations.funspec ~populate:false
+ (Extlib.the self#current_kf)))
(* it has a function contract *)
&& Functions.check kf
(* its annotations must be monitored *)))
- ->
+ ->
self#next ();
let name = Functions.RTL.mk_gen_name vi.vname in
let new_vi =
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
index cfbf3bf39c2d74923689a67c27923ef575af3e1f..b0b1206198c9e96a170c51956d467a61419b8637 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
@@ -1,9 +1,11 @@
/* run.config
- COMMENT: test option -e-acsl-instrument
+ COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
LOG: gen_@PTEST_NAME@.c
- OPT: -machdep gcc_x86_64 -e-acsl-instrument="@@all,-uninstrument1,-uninstrument2" -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva-verbose 0 -eva
+ OPT: -variadic-no-translation -machdep gcc_x86_64 -e-acsl-instrument="@@all,-uninstrument1,-uninstrument2" -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0
*/
+#include <stdarg.h>
+
int uninstrument1(int *p) {
*p = 0;
return 0;
@@ -12,7 +14,7 @@ int uninstrument1(int *p) {
/*@ requires \valid(p); */
int uninstrument2(int *p) {
{ int *q = p;
- *p = 0;
+ *p = 0;
goto L;
}
L:
@@ -27,13 +29,23 @@ int instrument1(int *p) {
/*@ requires \valid(p); */
int instrument2(int *p) {
{ int *q = p;
- *p = 0;
+ *p = 0;
goto L;
}
L:
return 0;
}
+/* test combination of -e-acsl-instrument and -variadic-no-translation;
+ see gitlab's issue #88 */
+int vol(int n, ...) {
+ va_list vl;
+ va_start(vl, n);
+ int r = va_arg(vl, int);
+ va_end(vl);
+ return 1;
+}
+
int main(void) {
int x;
int y = 0;
@@ -43,4 +55,5 @@ int main(void) {
uninstrument2(&x);
/*@ assert \initialized(&x); */
/*@ assert \initialized(&y); */
+ return vol(6, 1);
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
index efd026311297e55d8fefb674326118e6ece88624..10d0bb2429c656141ec1da23f443f176827c2075 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
@@ -1,2 +1,10 @@
[e-acsl] beginning translation.
+[kernel:annot:missing-spec] :0: Warning:
+ Neither code nor specification for function __builtin_va_arg, generating default assigns from the prototype
+[kernel:annot:missing-spec] :0: Warning:
+ Neither code nor specification for function __builtin_va_end, generating default assigns from the prototype
+[kernel:annot:missing-spec] :0: Warning:
+ Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype
+[e-acsl] tests/special/e-acsl-instrument.c:58: Warning:
+ ignoring effect of variadic function vol
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
index e98468cbadb3b87c17e376c94a59f06b3eda49f9..36e9221c01c15ab537afe24a99c8076106d6a0ea 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
@@ -1,8 +1,15 @@
/* Generated by Frama-C */
+#include "stdarg.h"
#include "stdio.h"
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
+/* compiler builtin:
+ void __builtin_va_arg(__builtin_va_list, unsigned long, void *); */
+/* compiler builtin:
+ void __builtin_va_end(__builtin_va_list); */
+/* compiler builtin:
+ void __builtin_va_start(__builtin_va_list); */
int __gen_e_acsl_uninstrument1(int *p);
int uninstrument1(int *p)
@@ -61,10 +68,23 @@ int instrument2(int *p)
return __retres;
}
-int main(void)
+int vol(int n , ...)
{
int __retres;
+ va_list vl;
+ int tmp;
+ __builtin_va_start(vl,n);
+ tmp = __builtin_va_arg (vl, int);
+ int r = tmp;
+ __builtin_va_end(vl);
+ __retres = 1;
+ return __retres;
+}
+
+int main(void)
+{
int x;
+ int tmp;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& x),(size_t)4);
int y = 0;
@@ -80,7 +100,7 @@ int main(void)
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& x),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&x)",44);
+ (char *)"main",(char *)"\\initialized(&x)",56);
}
/*@ assert \initialized(&y); */
{
@@ -88,13 +108,13 @@ int main(void)
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& y),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&y)",45);
+ (char *)"main",(char *)"\\initialized(&y)",57);
}
- __retres = 0;
+ tmp = vol(6,1);
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
__e_acsl_memory_clean();
- return __retres;
+ return tmp;
}
/*@ requires \valid(p); */
@@ -107,7 +127,7 @@ int __gen_e_acsl_instrument2(int *p)
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",
- (char *)"instrument2",(char *)"\\valid(p)",27);
+ (char *)"instrument2",(char *)"\\valid(p)",29);
}
__retres = instrument2(p);
__e_acsl_delete_block((void *)(& p));
@@ -123,7 +143,7 @@ int __gen_e_acsl_uninstrument2(int *p)
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",
- (char *)"uninstrument2",(char *)"\\valid(p)",12);
+ (char *)"uninstrument2",(char *)"\\valid(p)",14);
}
__e_acsl_sound_verdict = 0;
__retres = uninstrument2(p);