diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml index 817fae52b385f7c97a31f9f8db5874cfd4fc72b2..5db8ea3d06dc9002cce63770d7bf4366a5861e8f 100644 --- a/src/plugins/impact/register.ml +++ b/src/plugins/impact/register.ml @@ -98,52 +98,43 @@ let slice (stmts:stmt list) = Options.feedback ~level:2 "slicing done"; extracted_prj -let all_pragmas_kf l = - List.fold_left - (fun acc (s, a) -> - match a.annot_content with - | APragma (Impact_pragma IPstmt) -> s :: acc - | APragma (Impact_pragma (IPexpr _)) -> - Options.not_yet_implemented "impact pragmas: expr" - | _ -> assert false) - [] l - -let compute_pragmas () = - Ast.compute (); - let pragmas = ref [] in - let visitor = object - inherit Visitor.frama_c_inplace as super - - method! vfunc f = - pragmas := []; - super#vfunc f - - method! vstmt_aux s = - pragmas := - List.map - (fun a -> s, a) - (Annotations.code_annot ~filter:Logic_utils.is_impact_pragma s) - @ !pragmas; - Cil.DoChildren - end + +(* Register impact ACSL extension. *) +let () = + let typer typing_context loc args = + match args with + | [] -> Ext_terms [] + | _ -> typing_context.Logic_typing.error loc "Invalid impact directive" in + Acsl_extension.register_code_annot_next_both + ~plugin:"impact" "impact_stmt" typer false + +let is_impact_annot code_annot = + match code_annot.annot_content with + | AExtended (_, _, { ext_name = "impact_stmt"; }) -> true + | _ -> false + +let compute_annots () = + Ast.compute (); (* fill [pragmas] with all the pragmas of all the selected functions *) - let pragmas = - Options.Pragma.fold - (fun kf acc -> - (* Pragma option only accept defined functions. *) - let f = Kernel_function.get_definition kf in - ignore (Visitor.visitFramacFunction visitor f); - if !pragmas != [] then (kf, !pragmas) :: acc else acc) - [] + let process kf acc = + (* Pragma option only accept defined functions. *) + let fundec = Kernel_function.get_definition kf in + let has_impact_annot stmt = + let impact_annots = Annotations.code_annot ~filter:is_impact_annot stmt in + not (impact_annots = []) + in + let impact_stmts = List.filter has_impact_annot fundec.sallstmts in + if impact_stmts = [] then acc + else (kf, impact_stmts) :: acc in + let impact_stmts = Options.Pragma.fold process [] in let skip = Compute_impact.skip () in (* compute impact analyses on each kf *) let nodes = List.fold_left - (fun nodes (kf, pragmas) -> - let pragmas_stmts = all_pragmas_kf pragmas in - Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf pragmas_stmts) - ) Pdg_aux.NS.empty pragmas + (fun nodes (kf, stmts) -> + Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf stmts)) + Pdg_aux.NS.empty impact_stmts in let stmts = Compute_impact.nodes_to_stmts nodes in if Options.Slicing.get () then ignore (slice stmts); @@ -158,7 +149,7 @@ let main () = if Options.is_on () then begin Options.feedback "beginning analysis"; assert (not (Options.Pragma.is_empty ())); - ignore (compute_pragmas ()); + ignore (compute_annots ()); Options.feedback "analysis done" end let () = Boot.Main.extend main diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli index 35e476eb808dbb9e39c63d5a75ca885ab8057e1d..7a5f7aa71d11719fc2f9f310cf200a193f72987e 100644 --- a/src/plugins/impact/register.mli +++ b/src/plugins/impact/register.mli @@ -24,8 +24,8 @@ open Cil_types open Pdg_types -val compute_pragmas: (unit -> stmt list) -(** Compute the impact analysis from the impact pragma in the program. +val compute_annots: (unit -> stmt list) +(** Compute the impact analysis from the impact annotations in the program. Print and slice the results according to the parameters -impact-print and -impact-slice. @return the impacted statements *) diff --git a/tests/impact/alias.i b/tests/impact/alias.i index 1b4edfb05d19133efb9ed8b7154bdd0dce8041cd..b44ead9410983dbfead4c3b745879792ce2633d6 100644 --- a/tests/impact/alias.i +++ b/tests/impact/alias.i @@ -6,7 +6,7 @@ int P,c; /*@ requires \valid(x); */ int f(int *x) { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ int *y = x+1; *y = 4; int a = *(x+1) + 2; diff --git a/tests/impact/call.i b/tests/impact/call.i index c2c1e339205a9dc98fc5aa8120c824daafb2d343..64ee9f379f3109c3e323820713397ea59c685abe 100644 --- a/tests/impact/call.i +++ b/tests/impact/call.i @@ -1,5 +1,5 @@ /* run.config - + STDOPT: +"-impact-pragma main" STDOPT: +"-impact-pragma main2" +"-main main2" STDOPT: +"-impact-pragma main3" +"-main main3" @@ -19,7 +19,7 @@ void test (void) { /* ************************************************************************* */ void main (int x) { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ X = x; test (); } @@ -31,7 +31,7 @@ void call_test (void) { } void main2(int x) { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ X = x; call_test (); } @@ -50,7 +50,7 @@ void call_test3 (void) { } void main3(int x) { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ X = x; call_test3 (); } diff --git a/tests/impact/called.i b/tests/impact/called.i index 5971b9e56ba56310f16a6a87d08ab44032efa9a0..db29ddef5c35b53e7cb54ad4d6ce1f5a3fd281d1 100644 --- a/tests/impact/called.i +++ b/tests/impact/called.i @@ -10,7 +10,7 @@ int f(int x, int y) { X = x; return y; } void g() { int a, b, c, d; b = 0; - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ a = 0; c = f(a,b); d = X; @@ -19,7 +19,7 @@ void g() { void h() { int a, b, c, d; - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ b = 0; a = 0; c = f(a,b); diff --git a/tests/impact/depend1.i b/tests/impact/depend1.i index 6b3b3c0e81f98b48e957d7c91a12c261f46a2ae4..cb03869b56b3443e137a0b189795dd484e82b3c7 100644 --- a/tests/impact/depend1.i +++ b/tests/impact/depend1.i @@ -8,7 +8,7 @@ int find(int x) { return x; } int main() { int a = find(1); - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ int b = find(2); int c = find(b); int d = find(3); diff --git a/tests/impact/depend2.i b/tests/impact/depend2.i index dbc0a3ccc29e05e26dfcd560b3b9e550b90ce9b6..58b27ff58a5a6b0d8cc90f87f9bbf43a558f12d3 100644 --- a/tests/impact/depend2.i +++ b/tests/impact/depend2.i @@ -9,7 +9,7 @@ int apply(int x,int y) { return find(x)+y; } int main() { int a = apply(1,100); - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ int b = apply(2,200); return a+b ; } diff --git a/tests/impact/depend3.c b/tests/impact/depend3.c index 4f08af95fee341ba73e23a0ea9d8b9678c9f5ee0..1eb4778f27c352c95fffab6fa7ee004426cb1321 100644 --- a/tests/impact/depend3.c +++ b/tests/impact/depend3.c @@ -20,7 +20,7 @@ int apply(int x,int y) { return find(x); } int main() { int a = apply( 1 , 100 ); - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ int b = apply( 2 , 200 ); return a+b ; } diff --git a/tests/impact/depend4.i b/tests/impact/depend4.i index 3eefa9de01d483accb100ccfaba0368a98222b88..6368d46ea25d78f2551ed27e442f5078e6d6a14f 100644 --- a/tests/impact/depend4.i +++ b/tests/impact/depend4.i @@ -25,7 +25,7 @@ void g2() { void main () { g1(); - //@ impact pragma stmt; + //@ impact_stmt; f(); g2(); } diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i index 52b560fbce0feb000e1bab6d409c7d022216c822..e4800e4a54a63dc8382c53c845a78765e152f851 100644 --- a/tests/impact/depend5.i +++ b/tests/impact/depend5.i @@ -12,7 +12,7 @@ void f() { } void g() { - //@ impact pragma stmt; + //@ impact_stmt; d = 2; e = d; f(); @@ -24,4 +24,3 @@ void main () { a = 0; g(); } - diff --git a/tests/impact/first.i b/tests/impact/first.i index a210dbb40e83facee6309db9453cb18b6a4d027f..d99654b37d522a5149c0569d150a649479754b25 100644 --- a/tests/impact/first.i +++ b/tests/impact/first.i @@ -1,12 +1,12 @@ /* run.config - + STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact" */ int a, b, c, e, x, y, z, f, w; void impact() { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ b = a; if (c) { x = b + c; diff --git a/tests/impact/initial.i b/tests/impact/initial.i index 9c20d16edba7b176b6bd7a52742417b85e833623..2d815c5edfbe28ab08e6e8b95b6412021cca0ed1 100644 --- a/tests/impact/initial.i +++ b/tests/impact/initial.i @@ -1,6 +1,6 @@ /* run.config COMMENT: also tests the parsing of cmdline options of type string_set - STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'" + STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'" */ int x1, x2, y2, z2, x3; @@ -15,7 +15,7 @@ void f1() { void g1() { if (c) { - //@ impact pragma stmt; + //@ impact_stmt; f1(); } } @@ -42,7 +42,7 @@ void aux2() { void g2() { if (c) { - //@ impact pragma stmt; + //@ impact_stmt; f2(); if (c) aux2(); } @@ -65,7 +65,7 @@ void f3() { void g3() { - //@ impact pragma stmt; + //@ impact_stmt; f3(); if (c) { x3 = x3; diff --git a/tests/impact/loop.i b/tests/impact/loop.i index 0f8960d4aeefb17c00ffcee651ac700622ea31b8..f1c26e9d35c9a8b212f788552050f577c9f5e31f 100644 --- a/tests/impact/loop.i +++ b/tests/impact/loop.i @@ -1,5 +1,5 @@ /* run.config - + STDOPT: +"-impact-pragma loop" +"-lib-entry" +"-main loop" */ @@ -9,7 +9,7 @@ void loop () { while (c) { z = w + 1; z = y + 1; - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ x = x + 1; y = x + 1; } diff --git a/tests/impact/loop2.i b/tests/impact/loop2.i index 431ef94ee5b3e1f69e09f043b2ee85358b776721..c6ff73de8e93ab8d9da7e5f2b23ab6e5a72bdf1d 100644 --- a/tests/impact/loop2.i +++ b/tests/impact/loop2.i @@ -20,7 +20,7 @@ void f(int i) { } void main() { - //@ impact pragma stmt; + //@ impact_stmt; init (); for (int i=0; i<10; i++) { if (t[i]) // should not be selected diff --git a/tests/impact/oracle/slicing.res.oracle b/tests/impact/oracle/slicing.res.oracle index bcb4ba87e43c34bcdbab5decd6b82cb2d02298e8..07899df4b03d9d26c87033c1466749b33053b954 100644 --- a/tests/impact/oracle/slicing.res.oracle +++ b/tests/impact/oracle/slicing.res.oracle @@ -54,7 +54,7 @@ int w; void impact(void) { if (c) a = 18; - /*@ impact pragma stmt; */ + /*@ \impact::impact_stmt ; */ b = a; if (c) { x = b + c; diff --git a/tests/impact/slicing.i b/tests/impact/slicing.i index 93e008b356443eaed302408ad44e8789970de6c6..96b55a1278fbe14e152158a342acafbec2c6a62a 100644 --- a/tests/impact/slicing.i +++ b/tests/impact/slicing.i @@ -1,5 +1,5 @@ /* run.config - + STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact" +"-impact-slicing" +"-then-on 'impact slicing'" +"-print" */ @@ -7,7 +7,7 @@ int a, b, c, e, x, y, z, f, w; void impact() { if (c) a = 18; else x = 5; - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ b = a; if (c) { x = b + c; diff --git a/tests/impact/topbot.c b/tests/impact/topbot.c index 55d424eb28a3ab688027e09b4e9929c13a8ec411..60b8397b97d8746a8f39bf0101396a7a6e592e30 100644 --- a/tests/impact/topbot.c +++ b/tests/impact/topbot.c @@ -7,7 +7,7 @@ void f() { // Bottom PDG } void main(int c) { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ int x = 1; int y, z; if (c) { diff --git a/tests/impact/undef_function.i b/tests/impact/undef_function.i index 4c7dc4550ca84486e515423bcfd3501c0efc22c8..156bd3e9f53e5fbcc65413fe34c87948a25e29ae 100644 --- a/tests/impact/undef_function.i +++ b/tests/impact/undef_function.i @@ -5,7 +5,7 @@ int y; void g(int); int main() { - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ y=2; g(y); return y; diff --git a/tests/impact/variadic.i b/tests/impact/variadic.i index c08694d9de5f9448e7bd399f39ae6a6ad93bfa93..3746a648146597d01a6f6c340923d25772de986b 100644 --- a/tests/impact/variadic.i +++ b/tests/impact/variadic.i @@ -1,13 +1,13 @@ /* run.config COMMENT: also tests the parsing of cmdline options of type string_set - STDOPT: +"-impact-pragma main" +"-then -main main1 -impact-pragma='-main,+main1'" +"-then -main main2 -impact-pragma='-@all,+main2'" +"-then -main main3 -impact-pragma='+aux3,-main2'" +"-then -main main4 -impact-pragma='-aux3,+aux4'" + STDOPT: +"-impact-pragma main" +"-then -main main1 -impact-pragma='-main,+main1'" +"-then -main main2 -impact-pragma='-@all,+main2'" +"-then -main main3 -impact-pragma='+aux3,-main2'" +"-then -main main4 -impact-pragma='-aux3,+aux4'" */ int f(int, ...); int main () { int i=0; - /*@ impact pragma stmt; */ + /*@ impact_stmt; */ i++; f(i); } @@ -25,7 +25,7 @@ void g2(int x, ...); int main1() { int x = 3; - //@ impact pragma stmt; + //@ impact_stmt; g1(1, 2, 3); g1(1, 2); return y; @@ -33,7 +33,7 @@ int main1() { int main2() { int x = 3; - //@ impact pragma stmt; + //@ impact_stmt; g2(1, 2, 3); g2(1, 2); return y; @@ -47,7 +47,7 @@ void g3(int , ...); int aux3(int x, ...) { int t = 3; - //@ impact pragma stmt; + //@ impact_stmt; g1(t); g1(t); return y; @@ -60,7 +60,7 @@ int main3() { } void aux4(int x) { - //@ impact pragma stmt; + //@ impact_stmt; y = x; } diff --git a/tests/value/dead_code.i b/tests/value/dead_code.i index e0c5d2be9567894ed345ac2b6424a88f11591737..42e5d138ea89d9b291d1b7fc57e968aa3f2e11c5 100644 --- a/tests/value/dead_code.i +++ b/tests/value/dead_code.i @@ -1,8 +1,8 @@ void main(int in) { int i,j=6,k,l; - + i=10; - //@ impact pragma stmt; + i=1; L: if (i) {l= 17 ; goto OUT;} // i--;