Skip to content

GitLab

Commit 1bdc0cc2 authored by Julien Signoles's avatar Julien Signoles
Browse files

fix bug when combining -e-acsl-instrument and -variadic-no-translation (fix issue #88)

parent fc5d8f52
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/dup_functions.ml
View file @ 1bdc0cc2
......@@ -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 =
......
src/plugins/e-acsl/tests/special/e-acsl-instrument.c
View file @ 1bdc0cc2
/* 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);
}
src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
View file @ 1bdc0cc2
[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".
src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
View file @ 1bdc0cc2
/* 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);
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment