diff --git a/src/plugins/alias/tests/basic/oracle/addrof.res.oracle b/src/plugins/alias/tests/basic/oracle/addrof.res.oracle index c2b1c63088aa4f3e85059f208bcb9f968938d307..c721b21001c6ad2f68ca327d72df4754aa3fb229 100644 --- a/src/plugins/alias/tests/basic/oracle/addrof.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/addrof.res.oracle @@ -2,38 +2,16 @@ [alias] analysing function: main [alias] analysing instruction: a = & x; [alias] May-aliases after instruction a = & x; are { *a; x } -[alias] May-alias graph after instruction a = & x; is - 0:{ a } → 1:{ x } 1:{ x } → 3:{ } [alias] analysing instruction: b = & y; [alias] May-aliases after instruction b = & y; are { *a; x } { *b; y } -[alias] May-alias graph after instruction b = & y; is - 0:{ a } → 1:{ x } 1:{ x } → 3:{ } 5:{ b } → 6:{ y } - 6:{ y } → 8:{ } [alias] analysing instruction: y = & z; [alias] May-aliases after instruction y = & z; are { *a; x } { *b; y } { *(*b); *y; z } -[alias] May-alias graph after instruction y = & z; is - 0:{ a } → 1:{ x } 1:{ x } → 3:{ } 5:{ b } → 6:{ y } - 6:{ y } → 8:{ z } 8:{ z } → 11:{ } [alias] analysing instruction: *y = x; [alias] May-aliases after instruction *y = x; are { *(*b); *a; *y; x } { *b; a; y } -[alias] May-alias graph after instruction *y = x; is - 0:{ a } → 8:{ *y; x } 5:{ b } → 6:{ y } 6:{ y } → 8:{ *y; x } - 8:{ *y; x } → 3:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { *b; a; y } { *(*b); *a; *y; x; z } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a } → 1:{ *y; x; z } 1:{ *y; x; z } → 3:{ } - 5:{ b } → 6:{ y } 6:{ y } → 1:{ *y; x; z } [alias] May-aliases at the end of function main: { *b; a; y } { *(*b); *a; *y; x; z } -[alias] May-alias graph at the end of function main: - 0:{ a } → 1:{ *y; x; z } 1:{ *y; x; z } → 3:{ } - 5:{ b } → 6:{ y } 6:{ y } → 1:{ *y; x; z } -[alias] Summary of function main: - formals: - locals: a→{ *y; x; z } b→{ y } y→{ *y; x; z } x z p __retres - returns: __retres state: { *b; a; y } { *(*b); *a; *y; x; z } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle index 4c31afc87e8e5e4d692410292f68537cbb9d677a..0a62f46e5b140cf0ff68ba9f7cf44fc14c9c5491 100644 --- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle @@ -2,33 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { a; b } -[alias] May-alias graph after instruction a = b; is 0:{ a; b } → 1:{ } [alias] analysing instruction: b = c; [alias] May-aliases after instruction b = c; are { a; b; c } -[alias] May-alias graph after instruction b = c; is 0:{ a; b; c } → 1:{ } [alias] analysing instruction: a = d; [alias] May-aliases after instruction a = d; are { a; b; c; d } -[alias] May-alias graph after instruction a = d; is 0:{ a; b; c; d } → 1:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b; c; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; b; c; d } → 1:{ } [alias] May-aliases at the end of function main: { a; b; c; d } -[alias] May-alias graph at the end of function main: - 0:{ a; b; c; d } → 1:{ } -[alias] Summary of function main: - formals: locals: a b c d __retres returns: __retres - state: { a; b; c; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle index 1481782c77968432e096b4a525a333a85f548e97..02b7661040b329de9fcce9bcca780a7896a5a53a 100644 --- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle @@ -2,38 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int **a = (int **)0; [alias] May-aliases after instruction int **a = (int **)0; are <none> -[alias] May-alias graph after instruction int **a = (int **)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int **c = (int **)0; [alias] May-aliases after instruction int **c = (int **)0; are <none> -[alias] May-alias graph after instruction int **c = (int **)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: *a = b; [alias] May-aliases after instruction *a = b; are { *a; b } -[alias] May-alias graph after instruction *a = b; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 3:{ } [alias] analysing instruction: *c = d; [alias] May-aliases after instruction *c = d; are { *a; b } { *c; d } -[alias] May-alias graph after instruction *c = d; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 3:{ } 4:{ c } → 5:{ *c; d } - 5:{ *c; d } → 7:{ } [alias] analysing instruction: a = c; [alias] May-aliases after instruction a = c; are { a; c } { *a; *c; b; d } -[alias] May-alias graph after instruction a = c; is - 0:{ a; c } → 1:{ *a; *c; b; d } 1:{ *a; *c; b; d } → 3:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; c } { *a; *c; b; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; c } → 1:{ *a; *c; b; d } 1:{ *a; *c; b; d } → 3:{ } [alias] May-aliases at the end of function main: { a; c } { *a; *c; b; d } -[alias] May-alias graph at the end of function main: - 0:{ a; c } → 1:{ *a; *c; b; d } 1:{ *a; *c; b; d } → 3:{ } -[alias] Summary of function main: - formals: - locals: a→{ *a; *c; b; d } b c→{ *a; *c; b; d } d __retres - returns: __retres state: { a; c } { *a; *c; b; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle index 1a83b4c75eda9f4674f3c1a710e6061b3908e9a9..38afe15b98597c2d9d4d2753d68fc53c242b2a59 100644 --- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle @@ -2,28 +2,14 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int b = 0; [alias] May-aliases after instruction int b = 0; are <none> -[alias] May-alias graph after instruction int b = 0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: a = & b; [alias] May-aliases after instruction a = & b; are <none> -[alias] May-alias graph after instruction a = & b; is 0:{ a } → 1:{ b } [alias] analysing instruction: c = & b; [alias] May-aliases after instruction c = & b; are { a; c } -[alias] May-alias graph after instruction c = & b; is - 0:{ a } → 5:{ b } 4:{ c } → 5:{ b } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; c } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a } → 5:{ b } 4:{ c } → 5:{ b } [alias] May-aliases at the end of function main: { a; c } -[alias] May-alias graph at the end of function main: - 0:{ a } → 5:{ b } 4:{ c } → 5:{ b } -[alias] Summary of function main: - formals: locals: a→{ b } b c→{ b } __retres - returns: __retres state: { a; c } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle index e526142c5b4f21e91d3d7ee81e0071c1f423ba6a..8d9d355619779d4622cfb830c25bcebf079d70a2 100644 --- a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle @@ -2,41 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int **a = (int **)0; [alias] May-aliases after instruction int **a = (int **)0; are <none> -[alias] May-alias graph after instruction int **a = (int **)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int **c = (int **)0; [alias] May-aliases after instruction int **c = (int **)0; are <none> -[alias] May-alias graph after instruction int **c = (int **)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: *a = b; [alias] May-aliases after instruction *a = b; are { *a; b } -[alias] May-alias graph after instruction *a = b; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 3:{ } [alias] analysing instruction: *c = d; [alias] May-aliases after instruction *c = d; are { *a; b } { *c; d } -[alias] May-alias graph after instruction *c = d; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 3:{ } 4:{ c } → 5:{ *c; d } - 5:{ *c; d } → 7:{ } [alias] analysing instruction: b = d; [alias] May-aliases after instruction b = d; are { a; c } { *a; *c; b; d } -[alias] May-alias graph after instruction b = d; is - 0:{ a } → 1:{ *a; *c; b; d } 1:{ *a; *c; b; d } → 3:{ } - 4:{ c } → 1:{ *a; *c; b; d } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; c } { *a; *c; b; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a } → 1:{ *a; *c; b; d } 1:{ *a; *c; b; d } → 3:{ } - 4:{ c } → 1:{ *a; *c; b; d } [alias] May-aliases at the end of function main: { a; c } { *a; *c; b; d } -[alias] May-alias graph at the end of function main: - 0:{ a } → 1:{ *a; *c; b; d } 1:{ *a; *c; b; d } → 3:{ } - 4:{ c } → 1:{ *a; *c; b; d } -[alias] Summary of function main: - formals: - locals: a→{ *a; *c; b; d } b c→{ *a; *c; b; d } d __retres - returns: __retres state: { a; c } { *a; *c; b; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle index dbf7dc9fa16d31c8a0f740a6e7a725c32705bd77..023e852d0398703b8760d45770f1286d46c1c250 100644 --- a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle @@ -2,43 +2,20 @@ [alias] analysing function: main [alias] analysing instruction: int ***a = (int ***)0; [alias] May-aliases after instruction int ***a = (int ***)0; are <none> -[alias] May-alias graph after instruction int ***a = (int ***)0; is <empty> [alias] analysing instruction: int **b = (int **)0; [alias] May-aliases after instruction int **b = (int **)0; are <none> -[alias] May-alias graph after instruction int **b = (int **)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: *a = b; [alias] May-aliases after instruction *a = b; are { *a; b } -[alias] May-alias graph after instruction *a = b; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 3:{ } [alias] analysing instruction: *b = c; [alias] May-aliases after instruction *b = c; are { *a; b } { *(*a); *b; c } -[alias] May-alias graph after instruction *b = c; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 3:{ *b; c } - 3:{ *b; c } → 5:{ } [alias] analysing instruction: d = *(*a); [alias] May-aliases after instruction d = *(*a); are { *a; b } { *(*a); *b; c; d } -[alias] May-alias graph after instruction d = *(*a); is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 6:{ *(*a); *b; c; d } - 6:{ *(*a); *b; c; d } → 7:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { *a; b } { *(*a); *b; c; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 6:{ *(*a); *b; c; d } - 6:{ *(*a); *b; c; d } → 7:{ } [alias] May-aliases at the end of function main: { *a; b } { *(*a); *b; c; d } -[alias] May-alias graph at the end of function main: - 0:{ a } → 1:{ *a; b } 1:{ *a; b } → 6:{ *(*a); *b; c; d } - 6:{ *(*a); *b; c; d } → 7:{ } -[alias] Summary of function main: - formals: - locals: a→{ *a; b } b→{ *(*a); *b; c; d } c d __retres - returns: __retres state: { *a; b } { *(*a); *b; c; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle index 2ff8f37ad868abc5bc0a0450918f0ad672bf07e7..8a1dd1b9c580fa8fb3d77e3b216cbad020db570d 100644 --- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle @@ -2,33 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: float *c = (float *)0; [alias] May-aliases after instruction float *c = (float *)0; are <none> -[alias] May-alias graph after instruction float *c = (float *)0; is <empty> [alias] analysing instruction: float *d = (float *)0; [alias] May-aliases after instruction float *d = (float *)0; are <none> -[alias] May-alias graph after instruction float *d = (float *)0; is <empty> [alias] analysing instruction: a = (int *)c; [alias:unsafe-cast] cast1.c:10: Warning: unsafe cast from float * to int * [alias] May-aliases after instruction a = (int *)c; are { a; c } -[alias] May-alias graph after instruction a = (int *)c; is 0:{ a; c } → 1:{ } [alias] analysing instruction: d = (float *)b; [alias:unsafe-cast] cast1.c:11: Warning: unsafe cast from int * to float * [alias] May-aliases after instruction d = (float *)b; are { a; c } { b; d } -[alias] May-alias graph after instruction d = (float *)b; is - 0:{ a; c } → 1:{ } 4:{ b; d } → 5:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; c } { b; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; c } → 1:{ } 4:{ b; d } → 5:{ } [alias] May-aliases at the end of function main: { a; c } { b; d } -[alias] May-alias graph at the end of function main: - 0:{ a; c } → 1:{ } 4:{ b; d } → 5:{ } -[alias] Summary of function main: - formals: locals: a b c d __retres returns: __retres - state: { a; c } { b; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle index ede3b2e36f88bc3537ccbd4ac7ce7eca0a938110..878ffd6070b299f54c2888bf492b61e71983e5ec 100644 --- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle @@ -2,30 +2,16 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { a; b } -[alias] May-alias graph after instruction a = b; is 0:{ a; b } → 1:{ } [alias] analysing instruction: a = c; [alias] May-aliases after instruction a = c; are { a; c } -[alias] May-alias graph after instruction a = c; is 4:{ a; c } → 5:{ } [alias] analysing instruction: *a = 4; [alias] May-aliases after instruction *a = 4; are { a; b; c } -[alias] May-alias graph after instruction *a = 4; is 0:{ a; b; c } → 1:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b; c } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; b; c } → 1:{ } [alias] May-aliases at the end of function main: { a; b; c } -[alias] May-alias graph at the end of function main: - 0:{ a; b; c } → 1:{ } -[alias] Summary of function main: - formals: locals: a b c __retres returns: __retres - state: { a; b; c } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle index e89a21d4d30249677c5782f989f5a863e91d216e..74a6ebea0fc5c1ad01eeee8567b555029abb9cf8 100644 --- a/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/conditional2.res.oracle @@ -2,38 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: b = & c; [alias] May-aliases after instruction b = & c; are { *b; c } -[alias] May-alias graph after instruction b = & c; is - 0:{ b } → 1:{ c } 1:{ c } → 3:{ } [alias] analysing instruction: c = & d; [alias] May-aliases after instruction c = & d; are { *b; c } { *(*b); *c; d } -[alias] May-alias graph after instruction c = & d; is - 0:{ b } → 1:{ c } 1:{ c } → 3:{ d } 3:{ d } → 6:{ } [alias] analysing instruction: d = & e; [alias] May-aliases after instruction d = & e; are { *b; c } { *(*b); *c; d } -[alias] May-alias graph after instruction d = & e; is - 0:{ b } → 1:{ c } 1:{ c } → 3:{ d } 3:{ d } → 6:{ e } [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { *a; *b; c } { *(*a); *(*b); *c; d } { a; b } -[alias] May-alias graph after instruction a = b; is - 3:{ d } → 6:{ e } 10:{ a; b } → 11:{ c } 11:{ c } → 3:{ d } [alias] analysing instruction: a = & c; [alias] May-aliases after instruction a = & c; are { *a; *b; c } { *(*a); *(*b); *c; d } { a; b } -[alias] May-alias graph after instruction a = & c; is - 0:{ b } → 13:{ c } 3:{ d } → 6:{ e } 12:{ a } → 13:{ c } - 13:{ c } → 3:{ d } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { *a; *b; c } { *(*a); *(*b); *c; d } { a; b } -[alias] May-alias graph after instruction __retres = 0; is - 3:{ d } → 6:{ e } 10:{ a; b } → 11:{ c } 11:{ c } → 3:{ d } [alias] May-aliases at the end of function main: { *a; *b; c } { *(*a); *(*b); *c; d } { a; b } -[alias] May-alias graph at the end of function main: - 3:{ d } → 6:{ e } 10:{ a; b } → 11:{ c } 11:{ c } → 3:{ d } -[alias] Summary of function main: - formals: - locals: a→{ c } b→{ c } c→{ d } d→{ e } e __retres - returns: __retres state: { *a; *b; c } { *(*a); *(*b); *c; d } { a; b } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle index 8cc6d480f52d4b0b51617e8b844dc460ff29d0da..d91937c0431836ffc5d198eab44303805d5c6c48 100644 --- a/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/conditional3.res.oracle @@ -2,68 +2,34 @@ [alias] analysing function: main [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { a; b } -[alias] May-alias graph after instruction a = b; is 0:{ a; b } → 1:{ } [alias] analysing instruction: b = & i; [alias] May-aliases after instruction b = & i; are { a; b } { *a; *b; i } -[alias] May-alias graph after instruction b = & i; is - 0:{ a; b } → 1:{ i } 1:{ i } → 5:{ } [alias] analysing instruction: i = & x; [alias] May-aliases after instruction i = & x; are { a; b } { *a; *b; i } { *(*a); *(*b); *i; x } -[alias] May-alias graph after instruction i = & x; is - 0:{ a; b } → 1:{ i } 1:{ i } → 5:{ x } 5:{ x } → 8:{ } [alias] analysing instruction: x = & t; [alias] May-aliases after instruction x = & t; are { a; b } { *a; *b; i } { *(*a); *(*b); *i; x } { *(*(*a)); *(*(*b)); *(*i); *x; t } -[alias] May-alias graph after instruction x = & t; is - 0:{ a; b } → 1:{ i } 1:{ i } → 5:{ x } 5:{ x } → 8:{ t } - 8:{ t } → 11:{ } [alias] analysing instruction: a = c; [alias] May-aliases after instruction a = c; are { a; c } -[alias] May-alias graph after instruction a = c; is 13:{ a; c } → 14:{ } [alias] analysing instruction: c = & j; [alias] May-aliases after instruction c = & j; are { a; c } { *a; *c; j } -[alias] May-alias graph after instruction c = & j; is - 13:{ a; c } → 14:{ j } 14:{ j } → 18:{ } [alias] analysing instruction: j = & y; [alias] May-aliases after instruction j = & y; are { a; c } { *a; *c; j } { *(*a); *(*c); *j; y } -[alias] May-alias graph after instruction j = & y; is - 13:{ a; c } → 14:{ j } 14:{ j } → 18:{ y } 18:{ y } → 21:{ } [alias] analysing instruction: y = & u; [alias] May-aliases after instruction y = & u; are { a; c } { *a; *c; j } { *(*a); *(*c); *j; y } { *(*(*a)); *(*(*c)); *(*j); *y; u } -[alias] May-alias graph after instruction y = & u; is - 13:{ a; c } → 14:{ j } 14:{ j } → 18:{ y } 18:{ y } → 21:{ u } - 21:{ u } → 24:{ } [alias] analysing instruction: p = 0; [alias] May-aliases after instruction p = 0; are { a; b; c } { *a; *b; *c; i; j } { *(*a); *(*b); *(*c); *i; *j; x; y } { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u } -[alias] May-alias graph after instruction p = 0; is - 0:{ a; b; c } → 1:{ i; j } 1:{ i; j } → 5:{ x; y } - 5:{ x; y } → 8:{ t; u } 8:{ t; u } → 11:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b; c } { *a; *b; *c; i; j } { *(*a); *(*b); *(*c); *i; *j; x; y } { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; b; c } → 1:{ i; j } 1:{ i; j } → 5:{ x; y } - 5:{ x; y } → 8:{ t; u } 8:{ t; u } → 11:{ } [alias] May-aliases at the end of function main: { a; b; c } { *a; *b; *c; i; j } { *(*a); *(*b); *(*c); *i; *j; x; y } { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u } -[alias] May-alias graph at the end of function main: - 0:{ a; b; c } → 1:{ i; j } 1:{ i; j } → 5:{ x; y } - 5:{ x; y } → 8:{ t; u } 8:{ t; u } → 11:{ } -[alias] Summary of function main: - formals: - locals: a→{ i; j } b→{ i; j } c→{ i; j } i→{ x; y } j→{ x; y } - x→{ t; u } y→{ t; u } t u p __retres - returns: __retres - state: { a; b; c } { *a; *b; *c; i; j } - { *(*a); *(*b); *(*c); *i; *j; x; y } - { *(*(*a)); *(*(*b)); *(*(*c)); *(*i); *(*j); *x; *y; t; u } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/function1.res.oracle b/src/plugins/alias/tests/basic/oracle/function1.res.oracle index 53a681adaf7945cb50ed637d17ee962c903654ff..d97b433f7171289d3ffd85343bae5e419ea8ab15 100644 --- a/src/plugins/alias/tests/basic/oracle/function1.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/function1.res.oracle @@ -2,62 +2,30 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: swap(a,b); [alias] analysing function: swap [alias] analysing instruction: int *z = (int *)0; [alias] May-aliases after instruction int *z = (int *)0; are <none> -[alias] May-alias graph after instruction int *z = (int *)0; is <empty> [alias] analysing instruction: z = x; [alias] May-aliases after instruction z = x; are { x; z } -[alias] May-alias graph after instruction z = x; is 0:{ x; z } → 1:{ } [alias] analysing instruction: x = y; [alias] May-aliases after instruction x = y; are { x; y; z } -[alias] May-alias graph after instruction x = y; is 0:{ x; y; z } → 1:{ } [alias] analysing instruction: y = z; [alias] May-aliases after instruction y = z; are { x; y; z } -[alias] May-alias graph after instruction y = z; is 0:{ x; y; z } → 1:{ } [alias] May-aliases at the end of function swap: { x; y; z } -[alias] May-alias graph at the end of function swap: - 0:{ x; y; z } → 1:{ } -[alias] Summary of function swap: - formals: x y locals: z returns: <none> state: { x; y; z } [alias] May-aliases after instruction swap(a,b); are { a; b } -[alias] May-alias graph after instruction swap(a,b); is - 8:{ a } → 7:{ } 10:{ b } → 7:{ } [alias] analysing instruction: swap(c,d); [alias] May-aliases after instruction swap(c,d); are { a; b } { c; d } -[alias] May-alias graph after instruction swap(c,d); is - 8:{ a } → 7:{ } 10:{ b } → 7:{ } 14:{ c } → 13:{ } - 16:{ d } → 13:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b } { c; d } -[alias] May-alias graph after instruction __retres = 0; is - 8:{ a } → 7:{ } 10:{ b } → 7:{ } 14:{ c } → 13:{ } - 16:{ d } → 13:{ } [alias] May-aliases at the end of function main: { a; b } { c; d } -[alias] May-alias graph at the end of function main: - 8:{ a } → 7:{ } 10:{ b } → 7:{ } 14:{ c } → 13:{ } - 16:{ d } → 13:{ } -[alias] Summary of function main: - formals: locals: a b c d __retres returns: __retres - state: { a; b } { c; d } [alias] analysing function: swap [alias] analysing instruction: int *z = (int *)0; [alias] May-aliases after instruction int *z = (int *)0; are <none> -[alias] May-alias graph after instruction int *z = (int *)0; is <empty> [alias] May-aliases at the end of function swap: { x; y; z } -[alias] May-alias graph at the end of function swap: - 0:{ x; y; z } → 1:{ } -[alias] Summary of function swap: - formals: x y locals: z returns: <none> state: { x; y; z } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/function2.res.oracle b/src/plugins/alias/tests/basic/oracle/function2.res.oracle index 8a156f682a6963af147c9064e9ff2da0b9131a4d..1a770ac5390ebb5babb07ef0caabd3d4fd2c3bdd 100644 --- a/src/plugins/alias/tests/basic/oracle/function2.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/function2.res.oracle @@ -2,48 +2,23 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: a = my_malloc(2); [alias] analysing function: my_malloc [alias] analysing instruction: int *res = (int *)0; [alias] May-aliases after instruction int *res = (int *)0; are <none> -[alias] May-alias graph after instruction int *res = (int *)0; is <empty> [alias] analysing instruction: res = (int *)malloc((size_t)size); [alias] May-aliases after instruction res = (int *)malloc((size_t)size); are <none> -[alias] May-alias graph after instruction res = (int *)malloc((size_t)size); is - 0:{ res } → 1:{ } [alias] May-aliases at the end of function my_malloc: <none> -[alias] May-alias graph at the end of function my_malloc: - 0:{ res } → 1:{ } -[alias] Summary of function my_malloc: - formals: size locals: res returns: res state: <none> [alias] May-aliases after instruction a = my_malloc(2); are <none> -[alias] May-alias graph after instruction a = my_malloc(2); is - 4:{ a } → 3:{ } [alias] analysing instruction: b = my_malloc(3); [alias] May-aliases after instruction b = my_malloc(3); are <none> -[alias] May-alias graph after instruction b = my_malloc(3); is - 4:{ a } → 3:{ } 8:{ b } → 7:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is - 4:{ a } → 3:{ } 8:{ b } → 7:{ } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 4:{ a } → 3:{ } 8:{ b } → 7:{ } -[alias] Summary of function main: - formals: locals: a b __retres returns: __retres state: <none> [alias] analysing function: my_malloc [alias] analysing instruction: int *res = (int *)0; [alias] May-aliases after instruction int *res = (int *)0; are <none> -[alias] May-alias graph after instruction int *res = (int *)0; is <empty> [alias] May-aliases at the end of function my_malloc: <none> -[alias] May-alias graph at the end of function my_malloc: - 0:{ res } → 1:{ } -[alias] Summary of function my_malloc: - formals: size locals: res returns: res state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/function3.res.oracle b/src/plugins/alias/tests/basic/oracle/function3.res.oracle index 4acd78961680e393c1fe3c5297411895ab89be85..b45284aa949832888557c32e03d34fee1e6f1b6f 100644 --- a/src/plugins/alias/tests/basic/oracle/function3.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/function3.res.oracle @@ -2,56 +2,26 @@ [alias] analysing function: f1 [alias] analysing instruction: int *tmp = x; [alias] May-aliases after instruction int *tmp = x; are { x; tmp } -[alias] May-alias graph after instruction int *tmp = x; is - 0:{ x; tmp } → 1:{ } [alias] analysing instruction: x = y; [alias] May-aliases after instruction x = y; are { x; y; tmp } -[alias] May-alias graph after instruction x = y; is 0:{ x; y; tmp } → 1:{ } [alias] analysing instruction: y = tmp; [alias] May-aliases after instruction y = tmp; are { x; y; tmp } -[alias] May-alias graph after instruction y = tmp; is 0:{ x; y; tmp } → 1:{ } [alias] analysing instruction: __retres = (void *)0; [alias] May-aliases after instruction __retres = (void *)0; are { x; y; tmp } -[alias] May-alias graph after instruction __retres = (void *)0; is - 0:{ x; y; tmp } → 1:{ } [alias] May-aliases at the end of function f1: { x; y; tmp } -[alias] May-alias graph at the end of function f1: - 0:{ x; y; tmp } → 1:{ } -[alias] Summary of function f1: - formals: x y locals: tmp __retres returns: __retres - state: { x; y; tmp } [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: f1(a,b); [alias] May-aliases after instruction f1(a,b); are { a; b } -[alias] May-alias graph after instruction f1(a,b); is - 16:{ a } → 9:{ } 18:{ b } → 9:{ } [alias] analysing instruction: f1(c,d); [alias] May-aliases after instruction f1(c,d); are { a; b } { c; d } -[alias] May-alias graph after instruction f1(c,d); is - 16:{ a } → 9:{ } 18:{ b } → 9:{ } 28:{ c } → 21:{ } - 30:{ d } → 21:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b } { c; d } -[alias] May-alias graph after instruction __retres = 0; is - 16:{ a } → 9:{ } 18:{ b } → 9:{ } 28:{ c } → 21:{ } - 30:{ d } → 21:{ } [alias] May-aliases at the end of function main: { a; b } { c; d } -[alias] May-alias graph at the end of function main: - 16:{ a } → 9:{ } 18:{ b } → 9:{ } 28:{ c } → 21:{ } - 30:{ d } → 21:{ } -[alias] Summary of function main: - formals: locals: a b c d __retres returns: __retres - state: { a; b } { c; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/function4.res.oracle b/src/plugins/alias/tests/basic/oracle/function4.res.oracle index 8dbe90ab465fc2c12ddfc94ea2a4b2e31acc25e2..fb629f9683ca15d9fadde9031640b8070fa25eb5 100644 --- a/src/plugins/alias/tests/basic/oracle/function4.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/function4.res.oracle @@ -1,36 +1,17 @@ [kernel] Parsing function4.c (with preprocessing) [alias] analysing function: addr [alias] May-aliases at the end of function addr: <none> -[alias] May-alias graph at the end of function addr: - <empty> -[alias] Summary of function addr: - formals: x locals: returns: x state: <none> [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int c = 0; [alias] May-aliases after instruction int c = 0; are <none> -[alias] May-alias graph after instruction int c = 0; is <empty> [alias] analysing instruction: a = addr(& c); [alias] May-aliases after instruction a = addr(& c); are <none> -[alias] May-alias graph after instruction a = addr(& c); is - 4:{ a } → 3:{ c } 7:{ } → 3:{ c } [alias] analysing instruction: b = & c; [alias] May-aliases after instruction b = & c; are { a; b } -[alias] May-alias graph after instruction b = & c; is - 4:{ a } → 9:{ c } 7:{ } → 9:{ c } 8:{ b } → 9:{ c } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b } -[alias] May-alias graph after instruction __retres = 0; is - 4:{ a } → 9:{ c } 7:{ } → 9:{ c } 8:{ b } → 9:{ c } [alias] May-aliases at the end of function main: { a; b } -[alias] May-alias graph at the end of function main: - 4:{ a } → 9:{ c } 7:{ } → 9:{ c } 8:{ b } → 9:{ c } -[alias] Summary of function main: - formals: locals: a→{ c } b→{ c } c __retres - returns: __retres state: { a; b } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/function5.res.oracle b/src/plugins/alias/tests/basic/oracle/function5.res.oracle index c7d33151e1a9112a8c2a526607394f439bd4b5b3..53362c373d1c8f03d0e2ad4e06b1c2e4a30faea6 100644 --- a/src/plugins/alias/tests/basic/oracle/function5.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/function5.res.oracle @@ -2,43 +2,20 @@ [alias] analysing function: choice [alias] analysing instruction: int c = 0; [alias] May-aliases after instruction int c = 0; are <none> -[alias] May-alias graph after instruction int c = 0; is <empty> [alias] analysing instruction: __retres = x; [alias] May-aliases after instruction __retres = x; are { x; __retres } -[alias] May-alias graph after instruction __retres = x; is - 0:{ x; __retres } → 1:{ } [alias] analysing instruction: __retres = y; [alias] May-aliases after instruction __retres = y; are { y; __retres } -[alias] May-alias graph after instruction __retres = y; is - 4:{ y; __retres } → 5:{ } [alias] May-aliases at the end of function choice: { x; y; __retres } -[alias] May-alias graph at the end of function choice: - 0:{ x; y; __retres } → 1:{ } -[alias] Summary of function choice: - formals: x y locals: c __retres returns: __retres - state: { x; y; __retres } [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: c = choice(a,b); [alias] May-aliases after instruction c = choice(a,b); are { a; b; c } -[alias] May-alias graph after instruction c = choice(a,b); is - 10:{ c } → 9:{ } 12:{ a } → 9:{ } 14:{ b } → 9:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b; c } -[alias] May-alias graph after instruction __retres = 0; is - 10:{ c } → 9:{ } 12:{ a } → 9:{ } 14:{ b } → 9:{ } [alias] May-aliases at the end of function main: { a; b; c } -[alias] May-alias graph at the end of function main: - 10:{ c } → 9:{ } 12:{ a } → 9:{ } 14:{ b } → 9:{ } -[alias] Summary of function main: - formals: locals: a b c __retres returns: __retres - state: { a; b; c } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/function6.res.oracle b/src/plugins/alias/tests/basic/oracle/function6.res.oracle index 74f1dd62b95776d5a11a701bc27f5be540375eaf..4d8f8fa4a01fce5e95e6b5afdc4c4f24aec1c045 100644 --- a/src/plugins/alias/tests/basic/oracle/function6.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/function6.res.oracle @@ -2,54 +2,30 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: swap(a,b); [alias] analysing function: swap [alias] analysing instruction: int z = 0; [alias] May-aliases after instruction int z = 0; are <none> -[alias] May-alias graph after instruction int z = 0; is <empty> [alias] analysing instruction: z = *x; [alias] May-aliases after instruction z = *x; are <none> -[alias] May-alias graph after instruction z = *x; is <empty> [alias] analysing instruction: *x = *y; [alias] May-aliases after instruction *x = *y; are <none> -[alias] May-alias graph after instruction *x = *y; is <empty> [alias] analysing instruction: *y = z; [alias] May-aliases after instruction *y = z; are <none> -[alias] May-alias graph after instruction *y = z; is <empty> [alias] May-aliases at the end of function swap: <none> -[alias] May-alias graph at the end of function swap: - <empty> -[alias] Summary of function swap: [alias] May-aliases after instruction swap(a,b); are <none> -[alias] May-alias graph after instruction swap(a,b); is <empty> [alias] analysing instruction: swap(c,d); [alias] May-aliases after instruction swap(c,d); are <none> -[alias] May-alias graph after instruction swap(c,d); is <empty> [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is <empty> [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: a b c d __retres returns: __retres - state: <none> [alias] analysing function: swap [alias] analysing instruction: int z = 0; [alias] May-aliases after instruction int z = 0; are <none> -[alias] May-alias graph after instruction int z = 0; is <empty> [alias] May-aliases at the end of function swap: <none> -[alias] May-alias graph at the end of function swap: - <empty> -[alias] Summary of function swap: -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle index e5df545b132510deec597afaf51f5ed7af09202c..64f2826db29bf339219770a5cf558ec4f579b092 100644 --- a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle @@ -2,33 +2,18 @@ [alias] analysing function: f [alias] analysing instruction: int y = 0; [alias] May-aliases after instruction int y = 0; are <none> -[alias] May-alias graph after instruction int y = 0; is <empty> [alias] analysing instruction: *x = y; [alias] May-aliases after instruction *x = y; are <none> -[alias] May-alias graph after instruction *x = y; is <empty> [alias] May-aliases at the end of function f: <none> -[alias] May-alias graph at the end of function f: - <empty> -[alias] Summary of function f: [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: f(a); [alias] May-aliases after instruction f(a); are <none> -[alias] May-alias graph after instruction f(a); is <empty> [alias] analysing instruction: f(b); [alias] May-aliases after instruction f(b); are <none> -[alias] May-alias graph after instruction f(b); is <empty> [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is <empty> [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: a b __retres returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/loop.res.oracle b/src/plugins/alias/tests/basic/oracle/loop.res.oracle index 3bc56d48778f4936b53d3bde8985605d593e6ff3..9ef827f6daf8c1920926e31460dc19ab04c72bac 100644 --- a/src/plugins/alias/tests/basic/oracle/loop.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/loop.res.oracle @@ -2,37 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int l[1] = {0}; [alias] May-aliases after instruction int l[1] = {0}; are <none> -[alias] May-alias graph after instruction int l[1] = {0}; is <empty> [alias] analysing instruction: int *n_0 = & l[1]; [alias] May-aliases after instruction int *n_0 = & l[1]; are <none> -[alias] May-alias graph after instruction int *n_0 = & l[1]; is - 0:{ n_0 } → 1:{ l[0..] } [alias] analysing instruction: n_0 = & l[1] + 0; [alias] May-aliases after instruction n_0 = & l[1] + 0; are <none> -[alias] May-alias graph after instruction n_0 = & l[1] + 0; is - 0:{ n_0 } → 1:{ l[0..] } [alias] analysing instruction: int w = 0; [alias] May-aliases after instruction int w = 0; are <none> -[alias] May-alias graph after instruction int w = 0; is - 0:{ n_0 } → 1:{ l[0..] } [alias] analysing instruction: l[0] = *(& l[1] + 0); [alias] May-aliases after instruction l[0] = *(& l[1] + 0); are <none> -[alias] May-alias graph after instruction l[0] = *(& l[1] + 0); is - 0:{ n_0 } → 1:{ l[0..] } [alias] analysing instruction: int l[1] = {0}; [alias] May-aliases after instruction int l[1] = {0}; are <none> -[alias] May-alias graph after instruction int l[1] = {0}; is - 0:{ n_0 } → 1:{ l[0..] } [alias] analysing instruction: int *n_0 = & l[1]; [alias] May-aliases after instruction int *n_0 = & l[1]; are <none> -[alias] May-alias graph after instruction int *n_0 = & l[1]; is - 0:{ n_0 } → 1:{ l[0..] } [alias:no-return] loop.c:4: Warning: function main does not return; analysis may be unsound [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: l n_0 w __retres returns: __retres - state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle index fd9b99fe1833cbfae582d471119e770a2c048742..fdb1f8f1ce3b2bbb12c678edf124ed7295c1e1ff 100644 --- a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle @@ -2,40 +2,16 @@ [alias] analysing function: main [alias] analysing instruction: a = & x; [alias] May-aliases after instruction a = & x; are <none> -[alias] May-alias graph after instruction a = & x; is 0:{ a } → 1:{ x } [alias] analysing instruction: b = & y; [alias] May-aliases after instruction b = & y; are { *b; y } -[alias] May-alias graph after instruction b = & y; is - 0:{ a } → 1:{ x } 4:{ b } → 5:{ y } 5:{ y } → 7:{ } [alias] analysing instruction: y = & z; [alias] May-aliases after instruction y = & z; are { *b; y } -[alias] May-alias graph after instruction y = & z; is - 0:{ a } → 1:{ x } 4:{ b } → 5:{ y } 5:{ y } → 7:{ z } [alias] analysing instruction: y = & x; [alias] May-aliases after instruction y = & x; are { *b; a; y } -[alias] May-alias graph after instruction y = & x; is - 0:{ a } → 7:{ x } 4:{ b } → 5:{ y } 5:{ y } → 7:{ x } [alias] analysing instruction: c = & y; [alias] May-aliases after instruction c = & y; are { *b; *c; a; y } { b; c } -[alias] May-alias graph after instruction c = & y; is - 0:{ a } → 1:{ x; z } 4:{ b } → 13:{ y } 12:{ c } → 13:{ y } - 13:{ y } → 1:{ x; z } [alias] analysing instruction: *y = 4; [alias] May-aliases after instruction *y = 4; are { *b; *c; a; y } { b; c } -[alias] May-alias graph after instruction *y = 4; is - 0:{ a } → 1:{ x; z } 4:{ b } → 13:{ y } 12:{ c } → 13:{ y } - 13:{ y } → 1:{ x; z } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { *b; *c; a; y } { b; c } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a } → 1:{ x; z } 4:{ b } → 13:{ y } 12:{ c } → 13:{ y } - 13:{ y } → 1:{ x; z } [alias] May-aliases at the end of function main: { *b; *c; a; y } { b; c } -[alias] May-alias graph at the end of function main: - 0:{ a } → 1:{ x; z } 4:{ b } → 13:{ y } 12:{ c } → 13:{ y } - 13:{ y } → 1:{ x; z } -[alias] Summary of function main: - formals: - locals: a→{ x; z } b→{ y } c→{ y } y→{ x; z } x z p __retres - returns: __retres state: { *b; *c; a; y } { b; c } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle index 5d4e7565c296953e92026d4d6cc203263e988f2f..1d3c1881fa95b04f44b10729f9dbd1c1c045342c 100644 --- a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle @@ -2,35 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: int e = 0; [alias] May-aliases after instruction int e = 0; are <none> -[alias] May-alias graph after instruction int e = 0; is <empty> [alias] analysing instruction: case 1: a = d; [alias] May-aliases after instruction case 1: a = d; are { a; d } -[alias] May-alias graph after instruction case 1: a = d; is - 0:{ a; d } → 1:{ } [alias] analysing instruction: case 2: b = d; [alias] May-aliases after instruction case 2: b = d; are { b; d } -[alias] May-alias graph after instruction case 2: b = d; is - 4:{ b; d } → 5:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; b; d } → 1:{ } [alias] May-aliases at the end of function main: { a; b; d } -[alias] May-alias graph at the end of function main: - 0:{ a; b; d } → 1:{ } -[alias] Summary of function main: - formals: locals: a b c d e __retres returns: __retres - state: { a; b; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle b/src/plugins/alias/tests/basic/oracle/switch2.res.oracle index 35c8cb7b5d7312f2d58804c243b8c57bfb823545..8097b1a0db56aa0691de2531dcee7786e04b44f2 100644 --- a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/switch2.res.oracle @@ -2,39 +2,20 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int *d = (int *)0; [alias] May-aliases after instruction int *d = (int *)0; are <none> -[alias] May-alias graph after instruction int *d = (int *)0; is <empty> [alias] analysing instruction: int e = 0; [alias] May-aliases after instruction int e = 0; are <none> -[alias] May-alias graph after instruction int e = 0; is <empty> [alias] analysing instruction: case 1: a = d; [alias] May-aliases after instruction case 1: a = d; are { a; d } -[alias] May-alias graph after instruction case 1: a = d; is - 0:{ a; d } → 1:{ } [alias] analysing instruction: case 2: b = d; [alias] May-aliases after instruction case 2: b = d; are { b; d } -[alias] May-alias graph after instruction case 2: b = d; is - 4:{ b; d } → 5:{ } [alias] analysing instruction: default: c = d; [alias] May-aliases after instruction default: c = d; are { c; d } -[alias] May-alias graph after instruction default: c = d; is - 8:{ c; d } → 9:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b; c; d } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ a; b; c; d } → 1:{ } [alias] May-aliases at the end of function main: { a; b; c; d } -[alias] May-alias graph at the end of function main: - 0:{ a; b; c; d } → 1:{ } -[alias] Summary of function main: - formals: locals: a b c d e __retres returns: __retres - state: { a; b; c; d } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle index c389176d8e77f32afdd778d64cbf18f661460ed3..aa1b0b711b286dd90c43db7b0b53f3264a9c205a 100644 --- a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle @@ -2,27 +2,14 @@ [alias] analysing function: main [alias] analysing instruction: int *s = (int *)0; [alias] May-aliases after instruction int *s = (int *)0; are <none> -[alias] May-alias graph after instruction int *s = (int *)0; is <empty> [alias] analysing instruction: int idx = 0; [alias] May-aliases after instruction int idx = 0; are <none> -[alias] May-alias graph after instruction int idx = 0; is <empty> [alias] analysing instruction: s = (int *)malloc((size_t)idx); [alias] May-aliases after instruction s = (int *)malloc((size_t)idx); are <none> -[alias] May-alias graph after instruction s = (int *)malloc((size_t)idx); is - 0:{ s } → 1:{ } [alias] analysing instruction: idx ++; [alias] May-aliases after instruction idx ++; are <none> -[alias] May-alias graph after instruction idx ++; is 0:{ s } → 1:{ } [alias] analysing instruction: s = (int *)malloc((size_t)idx); [alias] May-aliases after instruction s = (int *)malloc((size_t)idx); are <none> -[alias] May-alias graph after instruction s = (int *)malloc((size_t)idx); is - 0:{ s } → 1:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is 0:{ s } → 1:{ } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 0:{ s } → 1:{ } -[alias] Summary of function main: - formals: locals: s idx __retres returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle index d6cd6b220b403aa05be9ad85693931f176437bb4..c7c4c865fea086d4385379cddaac3da2c9c5315d 100644 --- a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle @@ -2,23 +2,12 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { a; b } -[alias] May-alias graph after instruction a = b; is 0:{ a; b } → 1:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b } -[alias] May-alias graph after instruction __retres = 0; is 0:{ a; b } → 1:{ } [alias] May-aliases at the end of function main: { a; b } -[alias] May-alias graph at the end of function main: - 0:{ a; b } → 1:{ } -[alias] Summary of function main: - formals: locals: a b c __retres returns: __retres - state: { a; b } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle index 24560b86f6ecdc0f0141962db67bf9564f493ce3..40720eb3def4099a57c1c04e687c0d37e2a6f84e 100644 --- a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle +++ b/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle @@ -2,32 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: int *a = (int *)0; [alias] May-aliases after instruction int *a = (int *)0; are <none> -[alias] May-alias graph after instruction int *a = (int *)0; is <empty> [alias] analysing instruction: int *b = (int *)0; [alias] May-aliases after instruction int *b = (int *)0; are <none> -[alias] May-alias graph after instruction int *b = (int *)0; is <empty> [alias] analysing instruction: int *c = (int *)0; [alias] May-aliases after instruction int *c = (int *)0; are <none> -[alias] May-alias graph after instruction int *c = (int *)0; is <empty> [alias] analysing instruction: int i = 0; [alias] May-aliases after instruction int i = 0; are <none> -[alias] May-alias graph after instruction int i = 0; is <empty> [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { a; b } -[alias] May-alias graph after instruction a = b; is 0:{ a; b } → 1:{ } [alias] analysing instruction: __Cont: i ++; [alias] May-aliases after instruction __Cont: i ++; are { a; b } -[alias] May-alias graph after instruction __Cont: i ++; is 0:{ a; b } → 1:{ } [alias] analysing instruction: a = b; [alias] May-aliases after instruction a = b; are { a; b } -[alias] May-alias graph after instruction a = b; is 0:{ a; b } → 1:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b } -[alias] May-alias graph after instruction __retres = 0; is 0:{ a; b } → 1:{ } [alias] May-aliases at the end of function main: { a; b } -[alias] May-alias graph at the end of function main: - 0:{ a; b } → 1:{ } -[alias] Summary of function main: - formals: locals: a b c i __retres returns: __retres - state: { a; b } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle index 443ae47d1426c2a135603d828f7b5a1ed1bec5f1..3f911591f73e9f1c9f616f3a128b0651af18d00c 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/empty_nodes.res.oracle @@ -2,34 +2,13 @@ [alias] analysing function: f [alias] analysing instruction: *y = t + (*y - *x); [alias] May-aliases after instruction *y = t + (*y - *x); are { *y; t } -[alias] May-alias graph after instruction *y = t + (*y - *x); is - 0:{ y } → 1:{ *y; t } 1:{ *y; t } → 3:{ } [alias] analysing instruction: *z = t + (*z - *x); [alias] May-aliases after instruction *z = t + (*z - *x); are { *y; *z; t } { y; z } -[alias] May-alias graph after instruction *z = t + (*z - *x); is - 0:{ y } → 5:{ *y; *z; t } 4:{ z } → 5:{ *y; *z; t } - 5:{ *y; *z; t } → 3:{ } [alias] analysing instruction: *x = t; [alias] May-aliases after instruction *x = t; are { *x; *y; *z; t } { x; y; z } -[alias] May-alias graph after instruction *x = t; is - 0:{ y } → 7:{ *x; *y; *z; t } 4:{ z } → 7:{ *x; *y; *z; t } - 6:{ x } → 7:{ *x; *y; *z; t } 7:{ *x; *y; *z; t } → 3:{ } [alias] May-aliases at the end of function f: { *x; *y; *z; t } { x; y; z } -[alias] May-alias graph at the end of function f: - 0:{ y } → 7:{ *x; *y; *z; t } 4:{ z } → 7:{ *x; *y; *z; t } - 6:{ x } → 7:{ *x; *y; *z; t } 7:{ *x; *y; *z; t } → 3:{ } -[alias] Summary of function f: - formals: x→{ *x; *y; *z; t } y→{ *x; *y; *z; t } z→{ *x; *y; *z; t } - locals: t returns: <none> state: { *x; *y; *z; t } { x; y; z } [alias] analysing function: g [alias] analysing instruction: f(a,a,a); [alias] May-aliases after instruction f(a,a,a); are <none> -[alias] May-alias graph after instruction f(a,a,a); is - 15:{ } → 11:{ } 16:{ a } → 15:{ } [alias] May-aliases at the end of function g: <none> -[alias] May-alias graph at the end of function g: - 15:{ } → 11:{ } 16:{ a } → 15:{ } -[alias] Summary of function g: - formals: a locals: returns: <none> state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle index e612a89c586a0fdc111c28b02c52ef3676a94c20..fd9878fef65bf1ea35de5b51eef9ccfe7b40d5a0 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/gzip124.res.oracle @@ -2,29 +2,14 @@ [alias] analysing function: main [alias] analysing instruction: short tmp_0 = (short)0; [alias] May-aliases after instruction short tmp_0 = (short)0; are <none> -[alias] May-alias graph after instruction short tmp_0 = (short)0; is <empty> [alias] analysing instruction: *(& prev[1] + 0) = tmp_0; [alias] May-aliases after instruction *(& prev[1] + 0) = tmp_0; are <none> -[alias] May-alias graph after instruction *(& prev[1] + 0) = tmp_0; is <empty> [alias] analysing instruction: prev[0] = (short)0; [alias] May-aliases after instruction prev[0] = (short)0; are <none> -[alias] May-alias graph after instruction prev[0] = (short)0; is <empty> [alias] analysing instruction: p = & prev[1] + (int)*p; [alias] May-aliases after instruction p = & prev[1] + (int)*p; are <none> -[alias] May-alias graph after instruction p = & prev[1] + (int)*p; is - 0:{ p } → 1:{ prev[0..] } [alias] analysing instruction: p = & prev[*p]; [alias] May-aliases after instruction p = & prev[*p]; are <none> -[alias] May-alias graph after instruction p = & prev[*p]; is - 4:{ p } → 5:{ prev[0..] } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is - 0:{ p } → 1:{ prev[0..] } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 0:{ p } → 1:{ prev[0..] } -[alias] Summary of function main: - formals: locals: __retres prev p→{ prev[0..] } tmp_0 - returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle index 3b78e81856d737485a0c8ebca82926b6f7ac541a..5804eca90b42b52e9398c876abd3db981aa95c13 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle @@ -4,22 +4,11 @@ [alias] analysing function: f [alias] analysing instruction: tmp = & f; [alias] May-aliases after instruction tmp = & f; are <none> -[alias] May-alias graph after instruction tmp = & f; is 0:{ tmp } → 1:{ f } [alias] analysing instruction: tmp = (void (*)(void))*((char *)(v.t)); [alias:unsafe-cast] origin.c:8: Warning: unsafe cast from char to void (*)(void) [alias:unsafe-cast] origin.c:8: Warning: unsafe cast from int * to char * [alias] May-aliases after instruction tmp = (void (*)(void))*((char *)(v.t)); are { v.t; tmp } -[alias] May-alias graph after instruction tmp = (void (*)(void))*((char *)(v.t)); - is 0:{ v.t; tmp } → 1:{ f } [alias] analysing instruction: int g = (int)tmp; [alias] May-aliases after instruction int g = (int)tmp; are { v.t; tmp } -[alias] May-alias graph after instruction int g = (int)tmp; is - 0:{ v.t; tmp } → 1:{ f } [alias] May-aliases at the end of function f: { v.t; tmp } -[alias] May-alias graph at the end of function f: - 0:{ v.t; tmp } → 1:{ f } -[alias] Summary of function f: - formals: locals: g tmp→{ f } returns: <none> - state: { v.t; tmp } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle index cc580d0c444bff7d3155cddca8ed9e5eb8085d7b..e0e7350e8bb270bc2ab56b5fba3c3e9f0c191f38 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle @@ -4,11 +4,4 @@ [alias:unsafe-cast] origin_simpl.c:9: Warning: unsafe cast from int to void * [alias:unsafe-cast] origin_simpl.c:9: Warning: unsafe cast from char * to int * [alias] May-aliases after instruction tmp = (void *)*((int *)(t)); are { t; tmp } -[alias] May-alias graph after instruction tmp = (void *)*((int *)(t)); is - 0:{ t; tmp } → 1:{ } [alias] May-aliases at the end of function f: { t; tmp } -[alias] May-alias graph at the end of function f: - 0:{ t; tmp } → 1:{ } -[alias] Summary of function f: - formals: locals: tmp returns: <none> state: { t; tmp } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle index 14786295a9e7b48d1175d80c040fe1a01f180515..bdc3f9de65441a71704fe3c6c2faf4b5d51f684b 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle @@ -1,22 +1,12 @@ [kernel] Parsing semver.c (with preprocessing) [alias] analysing function: f [alias] May-aliases at the end of function f: <none> -[alias] May-alias graph at the end of function f: - <empty> -[alias] Summary of function f: [alias] analysing function: main [alias] analysing instruction: f((int *)*("1" + 2)); [alias:unsafe-cast] semver.c:6: Warning: unsafe cast from char to int * [alias:unsupported:addr] semver.c:6: Warning: unsupported feature: explicit pointer address: (int *)*("1" + 2); analysis may be unsound [alias] May-aliases after instruction f((int *)*("1" + 2)); are <none> -[alias] May-alias graph after instruction f((int *)*("1" + 2)); is <empty> [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is <empty> [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: __retres returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle index 6718bf0c37093b6cb0a8b7222931e426c49fc5d2..7843cab155742b5e87b1d4e3c6fd67107fca9412 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle @@ -4,15 +4,6 @@ [alias:unsafe-cast] tkn-2.c:6: Warning: unsafe cast from int ** to int * [alias] tkn-2.c:6: Warning: ignoring assignment of the form: a = (int *)(& a) [alias] May-aliases after instruction a = (int *)(& a); are <none> -[alias] May-alias graph after instruction a = (int *)(& a); is - 0:{ a } → 1:{ } 2:{ } → 0:{ a } [alias] analysing instruction: __retres = *a; [alias] May-aliases after instruction __retres = *a; are <none> -[alias] May-alias graph after instruction __retres = *a; is - 0:{ a } → 1:{ } 2:{ } → 0:{ a } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 0:{ a } → 1:{ } 2:{ } → 0:{ a } -[alias] Summary of function main: - formals: locals: a __retres returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle index 901bb8dd00022ad5be9e1c51ed3063ed3c7485a6..7ea35d5b5b006eaa354b2f151d11e281fceaf470 100644 --- a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle +++ b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle @@ -3,43 +3,19 @@ [alias] analysing instruction: char *s2 = CPS_SplitWord((char *)"a"); [alias] analysing function: CPS_SplitWord [alias] May-aliases at the end of function CPS_SplitWord: <none> -[alias] May-alias graph at the end of function CPS_SplitWord: - <empty> -[alias] Summary of function CPS_SplitWord: - formals: line locals: returns: line state: <none> [alias:unsafe-cast] union_vmap.c:11: Warning: unsafe cast from char const * to char * [alias] May-aliases after instruction char *s2 = CPS_SplitWord((char *)"a"); are <none> -[alias] May-alias graph after instruction char *s2 = CPS_SplitWord((char *)"a"); - is 4:{ s2 } → 3:{ } [alias] analysing instruction: char *s3 = CPS_SplitWord((char *)"b"); [alias:unsafe-cast] union_vmap.c:12: Warning: unsafe cast from char const * to char * [alias] May-aliases after instruction char *s3 = CPS_SplitWord((char *)"b"); are <none> -[alias] May-alias graph after instruction char *s3 = CPS_SplitWord((char *)"b"); - is 4:{ s2 } → 3:{ } 8:{ s3 } → 7:{ } [alias] analysing instruction: *key = s3; [alias] May-aliases after instruction *key = s3; are { *key; s3 } -[alias] May-alias graph after instruction *key = s3; is - 4:{ s2 } → 3:{ } 10:{ key } → 11:{ *key; s3 } - 11:{ *key; s3 } → 7:{ } [alias] analysing instruction: *key = s2; [alias] May-aliases after instruction *key = s2; are { *key; s2 } -[alias] May-alias graph after instruction *key = s2; is - 8:{ s3 } → 7:{ } 12:{ key } → 13:{ *key; s2 } - 13:{ *key; s2 } → 3:{ } [alias] May-aliases at the end of function CPS_ParseKey: { *key; s2; s3 } -[alias] May-alias graph at the end of function CPS_ParseKey: - 4:{ *key; s2; s3 } → 3:{ } 10:{ key } → 4:{ *key; s2; s3 } -[alias] Summary of function CPS_ParseKey: - formals: locals: key→{ *key; s2; s3 } s2 s3 returns: <none> - state: { *key; s2; s3 } [alias] analysing function: CPS_SplitWord [alias] May-aliases at the end of function CPS_SplitWord: <none> -[alias] May-alias graph at the end of function CPS_SplitWord: - <empty> -[alias] Summary of function CPS_SplitWord: - formals: line locals: returns: line state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle b/src/plugins/alias/tests/offsets/oracle/array1.res.oracle index c821849b395c672299eb67fe8a7370d2333bcaf8..d49ca85c658d42bd0df259842d7cb3df03f4aa41 100644 --- a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/array1.res.oracle @@ -2,33 +2,16 @@ [alias] analysing function: main [alias] analysing instruction: tab[0] = 0; [alias] May-aliases after instruction tab[0] = 0; are <none> -[alias] May-alias graph after instruction tab[0] = 0; is <empty> [alias] analysing instruction: tab[1] = 1; [alias] May-aliases after instruction tab[1] = 1; are <none> -[alias] May-alias graph after instruction tab[1] = 1; is <empty> [alias] analysing instruction: tab[2] = tab[1] + 1; [alias] May-aliases after instruction tab[2] = tab[1] + 1; are <none> -[alias] May-alias graph after instruction tab[2] = tab[1] + 1; is <empty> [alias] analysing instruction: int *x = & tab[1]; [alias] May-aliases after instruction int *x = & tab[1]; are <none> -[alias] May-alias graph after instruction int *x = & tab[1]; is - 0:{ x } → 1:{ tab[0..] } [alias] analysing instruction: int *y = & tab[2]; [alias] May-aliases after instruction int *y = & tab[2]; are { x; y } -[alias] May-alias graph after instruction int *y = & tab[2]; is - 0:{ x } → 5:{ tab[0..] } 4:{ y } → 5:{ tab[0..] } [alias] analysing instruction: tab[3] = *x + *y; [alias] May-aliases after instruction tab[3] = *x + *y; are { x; y } -[alias] May-alias graph after instruction tab[3] = *x + *y; is - 0:{ x } → 5:{ tab[0..] } 4:{ y } → 5:{ tab[0..] } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { x; y } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ x } → 5:{ tab[0..] } 4:{ y } → 5:{ tab[0..] } [alias] May-aliases at the end of function main: { x; y } -[alias] May-alias graph at the end of function main: - 0:{ x } → 5:{ tab[0..] } 4:{ y } → 5:{ tab[0..] } -[alias] Summary of function main: - formals: locals: tab x→{ tab[0..] } y→{ tab[0..] } __retres - returns: __retres state: { x; y } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle index bd04a4dd06d9d89516e956e23554d1e53a41486e..69f16a022f8b05688a9a9eb66a4180354fdcf323 100644 --- a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle @@ -2,26 +2,12 @@ [alias] analysing function: main [alias] analysing instruction: mat[0][0] = 0; [alias] May-aliases after instruction mat[0][0] = 0; are <none> -[alias] May-alias graph after instruction mat[0][0] = 0; is <empty> [alias] analysing instruction: mat[0][1] = 1; [alias] May-aliases after instruction mat[0][1] = 1; are <none> -[alias] May-alias graph after instruction mat[0][1] = 1; is <empty> [alias] analysing instruction: *x = mat[1]; [alias] May-aliases after instruction *x = mat[1]; are <none> -[alias] May-alias graph after instruction *x = mat[1]; is - 0:{ x } → 1:{ *x } 1:{ *x } → 2:{ mat[0..] } [alias] analysing instruction: *y = *(*(x + 0)); [alias] May-aliases after instruction *y = *(*(x + 0)); are <none> -[alias] May-alias graph after instruction *y = *(*(x + 0)); is - 0:{ x } → 1:{ *x } 1:{ *x } → 2:{ mat[0..] } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is - 0:{ x } → 1:{ *x } 1:{ *x } → 2:{ mat[0..] } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 0:{ x } → 1:{ *x } 1:{ *x } → 2:{ mat[0..] } -[alias] Summary of function main: - formals: locals: mat x→{ *x } y __retres returns: __retres - state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle index 91e72cbb2e6998c56e637ae6a5e4541753ac06ed..86668cf831491393ecc3771a7cfb19581fa3cd00 100644 --- a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle @@ -3,30 +3,13 @@ [alias] analysing instruction: int *x = malloc((unsigned long)4 * sizeof(int)); [alias] May-aliases after instruction int *x = malloc((unsigned long)4 * sizeof(int)); are <none> -[alias] May-alias graph after instruction - int *x = malloc((unsigned long)4 * sizeof(int)); is 0:{ x } → 1:{ } [alias] analysing instruction: int *y = malloc((unsigned long)4 * sizeof(int)); [alias] May-aliases after instruction int *y = malloc((unsigned long)4 * sizeof(int)); are <none> -[alias] May-alias graph after instruction - int *y = malloc((unsigned long)4 * sizeof(int)); is - 0:{ x } → 1:{ } 2:{ y } → 3:{ } [alias] analysing instruction: x = mat[0]; [alias] May-aliases after instruction x = mat[0]; are <none> -[alias] May-alias graph after instruction x = mat[0]; is - 0:{ x } → 1:{ mat[0..] } 2:{ y } → 3:{ } [alias] analysing instruction: y = mat[1]; [alias] May-aliases after instruction y = mat[1]; are { x; y } -[alias] May-alias graph after instruction y = mat[1]; is - 0:{ x } → 3:{ mat[0..] } 2:{ y } → 3:{ mat[0..] } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { x; y } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ x } → 3:{ mat[0..] } 2:{ y } → 3:{ mat[0..] } [alias] May-aliases at the end of function main: { x; y } -[alias] May-alias graph at the end of function main: - 0:{ x } → 3:{ mat[0..] } 2:{ y } → 3:{ mat[0..] } -[alias] Summary of function main: - formals: locals: mat x→{ mat[0..] } y→{ mat[0..] } __retres - returns: __retres state: { x; y } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle index e4249a441adbca262ad33717131d29672f517128..9b588f2f8f2484f894680dae6ca6129528811125 100644 --- a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle @@ -2,32 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: tab[0] = 0; [alias] May-aliases after instruction tab[0] = 0; are <none> -[alias] May-alias graph after instruction tab[0] = 0; is <empty> [alias] analysing instruction: tab[1] = 1; [alias] May-aliases after instruction tab[1] = 1; are <none> -[alias] May-alias graph after instruction tab[1] = 1; is <empty> [alias] analysing instruction: tab[2] = tab[1] + 1; [alias] May-aliases after instruction tab[2] = tab[1] + 1; are <none> -[alias] May-alias graph after instruction tab[2] = tab[1] + 1; is <empty> [alias] analysing instruction: int x = 0; [alias] May-aliases after instruction int x = 0; are <none> -[alias] May-alias graph after instruction int x = 0; is <empty> [alias] analysing instruction: int i = 0; [alias] May-aliases after instruction int i = 0; are <none> -[alias] May-alias graph after instruction int i = 0; is <empty> [alias] analysing instruction: x = tab[i]; [alias] May-aliases after instruction x = tab[i]; are <none> -[alias] May-alias graph after instruction x = tab[i]; is <empty> [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are <none> -[alias] May-alias graph after instruction i ++; is <empty> [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is <empty> [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: tab x i __retres returns: __retres - state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle index 07d8fde2b7c278965a45dd7769a59a4d2ca6bbd1..34b8bd11975081e1acc6cd63c7d0011d1f3b57e3 100644 --- a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle @@ -2,28 +2,16 @@ [alias] analysing function: main [alias] analysing instruction: mat[0][0] = 0; [alias] May-aliases after instruction mat[0][0] = 0; are <none> -[alias] May-alias graph after instruction mat[0][0] = 0; is <empty> [alias] analysing instruction: mat[0][1] = 1; [alias] May-aliases after instruction mat[0][1] = 1; are <none> -[alias] May-alias graph after instruction mat[0][1] = 1; is <empty> [alias] analysing instruction: int i = 2; [alias] May-aliases after instruction int i = 2; are <none> -[alias] May-alias graph after instruction int i = 2; is <empty> [alias] analysing instruction: mat[1][i] = i; [alias] May-aliases after instruction mat[1][i] = i; are <none> -[alias] May-alias graph after instruction mat[1][i] = i; is <empty> [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are <none> -[alias] May-alias graph after instruction i ++; is <empty> [alias] analysing instruction: mat[1][i] = 2; [alias] May-aliases after instruction mat[1][i] = 2; are <none> -[alias] May-alias graph after instruction mat[1][i] = 2; is <empty> [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is <empty> [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: mat i __retres returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle index 225de1d34179bcc8c8ba62d337eda2675cf72d43..4193c3f90a212238b3a6f1452d58e097c1ae1bd1 100644 --- a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle @@ -2,28 +2,16 @@ [alias] analysing function: main [alias] analysing instruction: mat[0][0] = 0; [alias] May-aliases after instruction mat[0][0] = 0; are <none> -[alias] May-alias graph after instruction mat[0][0] = 0; is <empty> [alias] analysing instruction: mat[0][1] = 1; [alias] May-aliases after instruction mat[0][1] = 1; are <none> -[alias] May-alias graph after instruction mat[0][1] = 1; is <empty> [alias] analysing instruction: int i = 2; [alias] May-aliases after instruction int i = 2; are <none> -[alias] May-alias graph after instruction int i = 2; is <empty> [alias] analysing instruction: mat[i][1] = i; [alias] May-aliases after instruction mat[i][1] = i; are <none> -[alias] May-alias graph after instruction mat[i][1] = i; is <empty> [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are <none> -[alias] May-alias graph after instruction i ++; is <empty> [alias] analysing instruction: mat[i][1] = 2; [alias] May-aliases after instruction mat[i][1] = 2; are <none> -[alias] May-alias graph after instruction mat[i][1] = 2; is <empty> [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is <empty> [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - <empty> -[alias] Summary of function main: - formals: locals: mat i __retres returns: __retres state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle b/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle index 028cc235d21b74fd523e32af23854d867d6c290e..03bb4fa391eb37bfe514513400ddf19bd07f2423 100644 --- a/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/jfla_running_ex.res.oracle @@ -2,134 +2,52 @@ [alias] analysing function: jfla [alias] analysing instruction: *snd = *fst; [alias] May-aliases after instruction *snd = *fst; are <none> -[alias] May-alias graph after instruction *snd = *fst; is <empty> [alias] analysing instruction: fst = *i1; [alias] May-aliases after instruction fst = *i1; are { *i1; fst } -[alias] May-alias graph after instruction fst = *i1; is - 0:{ *i1; fst } → 1:{ } 2:{ i1 } → 0:{ *i1; fst } [alias] analysing instruction: __retres = *i2; [alias] May-aliases after instruction __retres = *i2; are { *i1; fst } { *i2; __retres } -[alias] May-alias graph after instruction __retres = *i2; is - 0:{ *i1; fst } → 1:{ } 2:{ i1 } → 0:{ *i1; fst } - 4:{ *i2; __retres } → 5:{ } 6:{ i2 } → 4:{ *i2; __retres } [alias] analysing instruction: fst = *i2; [alias] May-aliases after instruction fst = *i2; are { *i2; fst } -[alias] May-alias graph after instruction fst = *i2; is - 8:{ *i2; fst } → 9:{ } 10:{ i2 } → 8:{ *i2; fst } [alias] analysing instruction: __retres = *i1; [alias] May-aliases after instruction __retres = *i1; are { *i2; fst } { *i1; __retres } -[alias] May-alias graph after instruction __retres = *i1; is - 8:{ *i2; fst } → 9:{ } 10:{ i2 } → 8:{ *i2; fst } - 12:{ *i1; __retres } → 13:{ } 14:{ i1 } → 12:{ *i1; __retres } [alias] May-aliases at the end of function jfla: { i1; i2 } { *i1; *i2; fst; __retres } -[alias] May-alias graph at the end of function jfla: - 0:{ *i1; *i2; fst; __retres } → 1:{ } - 2:{ i1 } → 0:{ *i1; *i2; fst; __retres } - 6:{ i2 } → 0:{ *i1; *i2; fst; __retres } -[alias] Summary of function jfla: - formals: fst snd i1→{ *i1; *i2; fst; __retres } - i2→{ *i1; *i2; fst; __retres } bo - locals: __retres returns: __retres - state: { i1; i2 } { *i1; *i2; fst; __retres } [alias] analysing function: main [alias] analysing instruction: int u = 11; [alias] May-aliases after instruction int u = 11; are <none> -[alias] May-alias graph after instruction int u = 11; is <empty> [alias] analysing instruction: int v = 12; [alias] May-aliases after instruction int v = 12; are <none> -[alias] May-alias graph after instruction int v = 12; is <empty> [alias] analysing instruction: int t[3] = {0, 1, 2}; [alias] May-aliases after instruction int t[3] = {0, 1, 2}; are <none> -[alias] May-alias graph after instruction int t[3] = {0, 1, 2}; is <empty> [alias] analysing instruction: int *a = & t[1]; [alias] May-aliases after instruction int *a = & t[1]; are <none> -[alias] May-alias graph after instruction int *a = & t[1]; is - 16:{ a } → 17:{ t[0..] } [alias] analysing instruction: int *b = & u; [alias] May-aliases after instruction int *b = & u; are <none> -[alias] May-alias graph after instruction int *b = & u; is - 16:{ a } → 17:{ t[0..] } 20:{ b } → 21:{ u } [alias] analysing instruction: int *c = & v; [alias] May-aliases after instruction int *c = & v; are <none> -[alias] May-alias graph after instruction int *c = & v; is - 16:{ a } → 17:{ t[0..] } 20:{ b } → 21:{ u } 24:{ c } → 25:{ v } [alias] analysing instruction: int **x = & a; [alias] May-aliases after instruction int **x = & a; are { *x; a } -[alias] May-alias graph after instruction int **x = & a; is - 20:{ b } → 21:{ u } 24:{ c } → 25:{ v } 28:{ x } → 29:{ a } - 29:{ a } → 17:{ t[0..] } [alias] analysing instruction: int **y = & b; [alias] May-aliases after instruction int **y = & b; are { *x; a } { *y; b } -[alias] May-alias graph after instruction int **y = & b; is - 24:{ c } → 25:{ v } 28:{ x } → 29:{ a } 29:{ a } → 17:{ t[0..] } - 31:{ y } → 32:{ b } 32:{ b } → 21:{ u } [alias] analysing instruction: int **z = & c; [alias] May-aliases after instruction int **z = & c; are { *x; a } { *y; b } { *z; c } -[alias] May-alias graph after instruction int **z = & c; is - 28:{ x } → 29:{ a } 29:{ a } → 17:{ t[0..] } 31:{ y } → 32:{ b } - 32:{ b } → 21:{ u } 34:{ z } → 35:{ c } 35:{ c } → 25:{ v } [alias] analysing instruction: struct str_t s = {.fst = c, .snd = t}; [alias] May-aliases after instruction struct str_t s = {.fst = c, .snd = t}; are { *x; a } { *y; b } { *z; c; s.fst } -[alias] May-alias graph after instruction struct str_t s = {.fst = c, .snd = t}; - is - 28:{ x } → 29:{ a } 29:{ a } → 17:{ t[0..] } 31:{ y } → 32:{ b } - 32:{ b } → 21:{ u } 34:{ z } → 37:{ c; s.fst } - 37:{ c; s.fst } → 25:{ v } 38:{ s.snd } → 39:{ t } [alias] analysing instruction: struct str_t *s1 = & s; [alias] May-aliases after instruction struct str_t *s1 = & s; are { *x; a } { *y; b } { *z; c; s.fst } -[alias] May-alias graph after instruction struct str_t *s1 = & s; is - 28:{ x } → 29:{ a } 29:{ a } → 17:{ t[0..] } 31:{ y } → 32:{ b } - 32:{ b } → 21:{ u } 34:{ z } → 37:{ c; s.fst } - 37:{ c; s.fst } → 25:{ v } 38:{ s.snd } → 39:{ t } - 41:{ s1 } → 42:{ s } [alias] analysing instruction: struct str_t *s2 = & s; [alias] May-aliases after instruction struct str_t *s2 = & s; are { *x; a } { *y; b } { *z; c; s.fst } { s1; s2 } -[alias] May-alias graph after instruction struct str_t *s2 = & s; is - 28:{ x } → 29:{ a } 29:{ a } → 17:{ t[0..] } 31:{ y } → 32:{ b } - 32:{ b } → 21:{ u } 34:{ z } → 37:{ c; s.fst } - 37:{ c; s.fst } → 25:{ v } 38:{ s.snd } → 39:{ t } - 41:{ s1 } → 46:{ s } 45:{ s2 } → 46:{ s } [alias] analysing instruction: c = jfla(s1->fst,s1->snd,x,y,0); [alias] May-aliases after instruction c = jfla(s1->fst,s1->snd,x,y,0); are { *x; *y; *z; s1->fst; a; b; c; s.fst } { x; y } { s1; s2 } -[alias] May-alias graph after instruction c = jfla(s1->fst,s1->snd,x,y,0); is - 28:{ x } → 29:{ a; b } 29:{ a; b } → 17:{ u; v; t[0..] } - 31:{ y } → 29:{ a; b } 34:{ z } → 37:{ c; s.fst } - 37:{ c; s.fst } → 17:{ u; v; t[0..] } 38:{ s.snd } → 39:{ t } - 41:{ s1 } → 46:{ s } 45:{ s2 } → 46:{ s } - 55:{ s1->fst } → 17:{ u; v; t[0..] } [alias] analysing instruction: a = jfla(s2->fst,s2->snd,y,z,1); [alias] May-aliases after instruction a = jfla(s2->fst,s2->snd,y,z,1); are { *x; *y; *z; s1->fst; s2->fst; a; b; c; s.fst } { x; y; z } { s1; s2 } -[alias] May-alias graph after instruction a = jfla(s2->fst,s2->snd,y,z,1); is - 28:{ x } → 29:{ a; b; c; s.fst } - 29:{ a; b; c; s.fst } → 17:{ u; v; t[0..] } - 31:{ y } → 29:{ a; b; c; s.fst } 34:{ z } → 29:{ a; b; c; s.fst } - 38:{ s.snd } → 39:{ t } 41:{ s1 } → 46:{ s } 45:{ s2 } → 46:{ s } - 55:{ s1->fst } → 17:{ u; v; t[0..] } - 63:{ s2->fst } → 17:{ u; v; t[0..] } [alias] May-aliases at the end of function main: { *x; *y; *z; s1->fst; s2->fst; a; b; c; s.fst } { x; y; z } { s1; s2 } -[alias] May-alias graph at the end of function main: - 28:{ x } → 29:{ a; b; c; s.fst } - 29:{ a; b; c; s.fst } → 17:{ u; v; t[0..] } - 31:{ y } → 29:{ a; b; c; s.fst } 34:{ z } → 29:{ a; b; c; s.fst } - 38:{ s.snd } → 39:{ t } 41:{ s1 } → 46:{ s } 45:{ s2 } → 46:{ s } - 55:{ s1->fst } → 17:{ u; v; t[0..] } - 63:{ s2->fst } → 17:{ u; v; t[0..] } -[alias] Summary of function main: - formals: - locals: u v t a→{ u; v; t[0..] } b→{ u; v; t[0..] } - c→{ u; v; t[0..] } x→{ a; b; c; s.fst } y→{ a; b; c; s.fst } - z→{ a; b; c; s.fst } s s1→{ s } s2→{ s } - returns: <none> - state: { *x; *y; *z; s1->fst; s2->fst; a; b; c; s.fst } { x; y; z } - { s1; s2 } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle index 87b1ce12e31e680ab2fa0b9d2abba26d5d84bccf..b4f23332d9c69739cdd113c138088b4b712395d5 100644 --- a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle @@ -2,130 +2,55 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2}; [alias] May-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are <none> -[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is - <empty> [alias] analysing instruction: tab_y[0] = & x1; [alias] May-aliases after instruction tab_y[0] = & x1; are <none> -[alias] May-alias graph after instruction tab_y[0] = & x1; is - 0:{ tab_y[0..] } → 1:{ x1 } [alias] analysing instruction: tab_y[1] = & x2; [alias] May-aliases after instruction tab_y[1] = & x2; are <none> -[alias] May-alias graph after instruction tab_y[1] = & x2; is - 0:{ tab_y[0..] } → 1:{ x1; x2 } [alias] analysing instruction: st_2_t *z1 = malloc(sizeof(st_2_t)); [alias] May-aliases after instruction st_2_t *z1 = malloc(sizeof(st_2_t)); are <none> -[alias] May-alias graph after instruction st_2_t *z1 = malloc(sizeof(st_2_t)); - is 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } [alias] analysing instruction: st_2_t *z2 = malloc(sizeof(st_2_t)); [alias] May-aliases after instruction st_2_t *z2 = malloc(sizeof(st_2_t)); are <none> -[alias] May-alias graph after instruction st_2_t *z2 = malloc(sizeof(st_2_t)); - is - 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } 7:{ z2 } → 8:{ } [alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t)); [alias] May-aliases after instruction st_3_t *t = malloc(sizeof(st_3_t)); are <none> -[alias] May-alias graph after instruction st_3_t *t = malloc(sizeof(st_3_t)); is - 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } [alias] analysing instruction: int *a = malloc(sizeof(int)); [alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is - 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } 11:{ a } → 12:{ } [alias] analysing instruction: int *b = malloc(sizeof(int)); [alias] May-aliases after instruction int *b = malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction int *b = malloc(sizeof(int)); is - 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } 11:{ a } → 12:{ } - 13:{ b } → 14:{ } [alias] analysing instruction: *a = 0; [alias] May-aliases after instruction *a = 0; are <none> -[alias] May-alias graph after instruction *a = 0; is - 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } 11:{ a } → 12:{ } - 13:{ b } → 14:{ } [alias] analysing instruction: *b = 5; [alias] May-aliases after instruction *b = 5; are <none> -[alias] May-alias graph after instruction *b = 5; is - 0:{ tab_y[0..] } → 1:{ x1; x2 } 5:{ z1 } → 6:{ } - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } 11:{ a } → 12:{ } - 13:{ b } → 14:{ } [alias] analysing instruction: z1->s = (struct struct_1_t *)tab_y[0]; [alias:unsafe-cast] nested1.c:47: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction z1->s = (struct struct_1_t *)tab_y[0]; are { z1->s; tab_y[0..] } -[alias] May-alias graph after instruction z1->s = (struct struct_1_t *)tab_y[0]; - is - 5:{ z1 } → 6:{ } 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 11:{ a } → 12:{ } 13:{ b } → 14:{ } - 15:{ z1->s; tab_y[0..] } → 1:{ x1; x2 } [alias] analysing instruction: z2->s = (struct struct_1_t *)tab_y[1]; [alias:unsafe-cast] nested1.c:48: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction z2->s = (struct struct_1_t *)tab_y[1]; are { z1->s; z2->s; tab_y[0..] } -[alias] May-alias graph after instruction z2->s = (struct struct_1_t *)tab_y[1]; - is - 5:{ z1 } → 6:{ } 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 11:{ a } → 12:{ } 13:{ b } → 14:{ } - 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } [alias] analysing instruction: z1->c = a; [alias] May-aliases after instruction z1->c = a; are { z1->s; z2->s; tab_y[0..] } { z1->c; a } -[alias] May-alias graph after instruction z1->c = a; is - 5:{ z1 } → 6:{ } 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 13:{ b } → 14:{ } 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } - 17:{ z1->c; a } → 12:{ } [alias] analysing instruction: z2->c = b; [alias] May-aliases after instruction z2->c = b; are { z1->s; z2->s; tab_y[0..] } { z1->c; a } { z2->c; b } -[alias] May-alias graph after instruction z2->c = b; is - 5:{ z1 } → 6:{ } 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } - 17:{ z1->c; a } → 12:{ } 18:{ z2->c; b } → 14:{ } [alias] analysing instruction: t->t = (struct struct_2_t *)z1; [alias:unsafe-cast] nested1.c:51: Warning: unsafe cast from st_2_t * to struct struct_2_t * [alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are { z1->s; z2->s; tab_y[0..] } { t->t; z1 } { z1->c; a } { z2->c; b } -[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z1; is - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } - 17:{ z1->c; a } → 12:{ } 18:{ z2->c; b } → 14:{ } - 19:{ t->t; z1 } → 6:{ } [alias] analysing instruction: t->d = a; [alias] May-aliases after instruction t->d = a; are { z1->s; z2->s; tab_y[0..] } { t->t; z1 } { z1->c; t->d; a } { z2->c; b } -[alias] May-alias graph after instruction t->d = a; is - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } - 18:{ z2->c; b } → 14:{ } 19:{ t->t; z1 } → 6:{ } - 20:{ z1->c; t->d; a } → 12:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { z1->s; z2->s; tab_y[0..] } { t->t; z1 } { z1->c; t->d; a } { z2->c; b } -[alias] May-alias graph after instruction __retres = 0; is - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } - 18:{ z2->c; b } → 14:{ } 19:{ t->t; z1 } → 6:{ } - 20:{ z1->c; t->d; a } → 12:{ } [alias] May-aliases at the end of function main: { z1->s; z2->s; tab_y[0..] } { t->t; z1 } { z1->c; t->d; a } { z2->c; b } -[alias] May-alias graph at the end of function main: - 7:{ z2 } → 8:{ } 9:{ t } → 10:{ } - 16:{ z1->s; z2->s; tab_y[0..] } → 1:{ x1; x2 } - 18:{ z2->c; b } → 14:{ } 19:{ t->t; z1 } → 6:{ } - 20:{ z1->c; t->d; a } → 12:{ } -[alias] Summary of function main: - formals: locals: x1 x2 tab_y z1 z2 t a b __retres - returns: __retres - state: { z1->s; z2->s; tab_y[0..] } { t->t; z1 } { z1->c; t->d; a } - { z2->c; b } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle index 7c472531448f5e756b19f0e4ccca5e374f37e5ee..c7e1e4080bea78a9c948d978669eb9b2da18a728 100644 --- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle @@ -2,78 +2,39 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_1_t x2 = {.a = 2, .b = 3}; [alias] May-aliases after instruction st_1_t x2 = {.a = 2, .b = 3}; are <none> -[alias] May-alias graph after instruction st_1_t x2 = {.a = 2, .b = 3}; is - <empty> [alias] analysing instruction: st_2_t *z1 = malloc(sizeof(st_2_t)); [alias] May-aliases after instruction st_2_t *z1 = malloc(sizeof(st_2_t)); are <none> -[alias] May-alias graph after instruction st_2_t *z1 = malloc(sizeof(st_2_t)); - is 0:{ z1 } → 1:{ } [alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t)); [alias] May-aliases after instruction st_3_t *t = malloc(sizeof(st_3_t)); are <none> -[alias] May-alias graph after instruction st_3_t *t = malloc(sizeof(st_3_t)); is - 0:{ z1 } → 1:{ } 2:{ t } → 3:{ } [alias] analysing instruction: int *a = malloc(sizeof(int)); [alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is - 0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ } [alias] analysing instruction: *a = 0; [alias] May-aliases after instruction *a = 0; are <none> -[alias] May-alias graph after instruction *a = 0; is - 0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ } [alias] analysing instruction: z1->s[0] = (struct struct_1_t *)(& x1); [alias:unsafe-cast] nested2.c:42: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction z1->s[0] = (struct struct_1_t *)(& x1); are <none> -[alias] May-alias graph after instruction z1->s[0] = (struct struct_1_t *)(& x1); - is - 0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ } - 6:{ z1->s[0..] } → 7:{ x1 } [alias] analysing instruction: z1->s[1] = (struct struct_1_t *)(& x2); [alias:unsafe-cast] nested2.c:43: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction z1->s[1] = (struct struct_1_t *)(& x2); are <none> -[alias] May-alias graph after instruction z1->s[1] = (struct struct_1_t *)(& x2); - is - 0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ } - 6:{ z1->s[0..] } → 7:{ x1; x2 } [alias] analysing instruction: z1->c = a; [alias] May-aliases after instruction z1->c = a; are { z1->c; a } -[alias] May-alias graph after instruction z1->c = a; is - 0:{ z1 } → 1:{ } 2:{ t } → 3:{ } - 6:{ z1->s[0..] } → 7:{ x1; x2 } 11:{ z1->c; a } → 5:{ } [alias] analysing instruction: t->t = (struct struct_2_t *)z1; [alias:unsafe-cast] nested2.c:45: Warning: unsafe cast from st_2_t * to struct struct_2_t * [alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are { t->t; z1 } { z1->c; a } -[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z1; is - 2:{ t } → 3:{ } 6:{ z1->s[0..] } → 7:{ x1; x2 } - 11:{ z1->c; a } → 5:{ } 12:{ t->t; z1 } → 1:{ } [alias] analysing instruction: t->d = a; [alias] May-aliases after instruction t->d = a; are { t->t; z1 } { z1->c; t->d; a } -[alias] May-alias graph after instruction t->d = a; is - 2:{ t } → 3:{ } 6:{ z1->s[0..] } → 7:{ x1; x2 } - 12:{ t->t; z1 } → 1:{ } 13:{ z1->c; t->d; a } → 5:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { t->t; z1 } { z1->c; t->d; a } -[alias] May-alias graph after instruction __retres = 0; is - 2:{ t } → 3:{ } 6:{ z1->s[0..] } → 7:{ x1; x2 } - 12:{ t->t; z1 } → 1:{ } 13:{ z1->c; t->d; a } → 5:{ } [alias] May-aliases at the end of function main: { t->t; z1 } { z1->c; t->d; a } -[alias] May-alias graph at the end of function main: - 2:{ t } → 3:{ } 6:{ z1->s[0..] } → 7:{ x1; x2 } - 12:{ t->t; z1 } → 1:{ } 13:{ z1->c; t->d; a } → 5:{ } -[alias] Summary of function main: - formals: locals: x1 x2 z1 t a __retres returns: __retres - state: { t->t; z1 } { z1->c; t->d; a } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle index 668bf60c584a9a158f652be25a79484f51ad5da5..b325558af323d355e913457f624f99202dc3c3bb 100644 --- a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle @@ -2,38 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_2_t y = {.a = 3, .c = 4}; [alias] May-aliases after instruction st_2_t y = {.a = 3, .c = 4}; are <none> -[alias] May-alias graph after instruction st_2_t y = {.a = 3, .c = 4}; is - <empty> [alias] analysing instruction: st_1_t *p_x = & x; [alias] May-aliases after instruction st_1_t *p_x = & x; are <none> -[alias] May-alias graph after instruction st_1_t *p_x = & x; is - 0:{ p_x } → 1:{ x } [alias] analysing instruction: st_2_t *p_y = & y; [alias] May-aliases after instruction st_2_t *p_y = & y; are <none> -[alias] May-alias graph after instruction st_2_t *p_y = & y; is - 0:{ p_x } → 1:{ x } 4:{ p_y } → 5:{ y } [alias] analysing instruction: p_x->a = 3; [alias] May-aliases after instruction p_x->a = 3; are <none> -[alias] May-alias graph after instruction p_x->a = 3; is - 0:{ p_x } → 1:{ x } 4:{ p_y } → 5:{ y } [alias] analysing instruction: p_x = (st_1_t *)p_y; [alias:unsafe-cast] structure1.c:28: Warning: unsafe cast from st_2_t * to st_1_t * [alias] May-aliases after instruction p_x = (st_1_t *)p_y; are { p_x; p_y } -[alias] May-alias graph after instruction p_x = (st_1_t *)p_y; is - 0:{ p_x; p_y } → 1:{ x; y } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { p_x; p_y } -[alias] May-alias graph after instruction __retres = 0; is - 0:{ p_x; p_y } → 1:{ x; y } [alias] May-aliases at the end of function main: { p_x; p_y } -[alias] May-alias graph at the end of function main: - 0:{ p_x; p_y } → 1:{ x; y } -[alias] Summary of function main: - formals: locals: x y p_x→{ x; y } p_y→{ x; y } __retres - returns: __retres state: { p_x; p_y } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle index 6d772d05177591e1f64bcddb250a6017bf5cc2fb..2b2f7ecd4e531f1ec02f3d115396b6b6f0de27d0 100644 --- a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle @@ -2,35 +2,18 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2}; [alias] May-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are <none> -[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is - <empty> [alias] analysing instruction: st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4}; [alias:unsafe-cast] structure2.c:21: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4}; are <none> -[alias] May-alias graph after instruction - st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4}; is - 0:{ y.s } → 1:{ x1 } [alias] analysing instruction: y.s = (struct struct_1_t *)(& x2); [alias:unsafe-cast] structure2.c:23: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction y.s = (struct struct_1_t *)(& x2); are <none> -[alias] May-alias graph after instruction y.s = (struct struct_1_t *)(& x2); is - 0:{ y.s } → 1:{ x1; x2 } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is - 0:{ y.s } → 1:{ x1; x2 } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 0:{ y.s } → 1:{ x1; x2 } -[alias] Summary of function main: - formals: locals: x1 x2 y __retres returns: __retres - state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle index 6c9609a49da5b01e47a82b3a5b946d87087c28e4..7ec86d402cb6980ff01296b3901039b234b94464 100644 --- a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle @@ -2,61 +2,32 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2}; [alias] May-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are <none> -[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is - <empty> [alias] analysing instruction: st_2_t y1 = {.s = (struct struct_1_t *)(& x1), .c = 3}; [alias:unsafe-cast] structure3.c:31: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction st_2_t y1 = {.s = (struct struct_1_t *)(& x1), .c = 3}; are <none> -[alias] May-alias graph after instruction - st_2_t y1 = {.s = (struct struct_1_t *)(& x1), .c = 3}; is - 0:{ y1.s } → 1:{ x1 } [alias] analysing instruction: st_2_t y2 = {.s = (struct struct_1_t *)(& x2), .c = 4}; [alias:unsafe-cast] structure3.c:32: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction st_2_t y2 = {.s = (struct struct_1_t *)(& x2), .c = 4}; are <none> -[alias] May-alias graph after instruction - st_2_t y2 = {.s = (struct struct_1_t *)(& x2), .c = 4}; is - 0:{ y1.s } → 1:{ x1 } 3:{ y2.s } → 4:{ x2 } [alias] analysing instruction: st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5}; [alias:unsafe-cast] structure3.c:33: Warning: unsafe cast from st_2_t * to struct struct_2_t * [alias] May-aliases after instruction st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5}; are <none> -[alias] May-alias graph after instruction - st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5}; is - 0:{ y1.s } → 1:{ x1 } 3:{ y2.s } → 4:{ x2 } 6:{ z.t } → 7:{ y1 } [alias] analysing instruction: z.t = (struct struct_2_t *)(& y2); [alias:unsafe-cast] structure3.c:35: Warning: unsafe cast from st_2_t * to struct struct_2_t * [alias] May-aliases after instruction z.t = (struct struct_2_t *)(& y2); are <none> -[alias] May-alias graph after instruction z.t = (struct struct_2_t *)(& y2); is - 0:{ y1.s } → 1:{ x1 } 3:{ y2.s } → 4:{ x2 } - 6:{ z.t } → 7:{ y1; y2 } [alias] analysing instruction: y1.c = z.d; [alias] May-aliases after instruction y1.c = z.d; are <none> -[alias] May-alias graph after instruction y1.c = z.d; is - 0:{ y1.s } → 1:{ x1 } 3:{ y2.s } → 4:{ x2 } - 6:{ z.t } → 7:{ y1; y2 } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are <none> -[alias] May-alias graph after instruction __retres = 0; is - 0:{ y1.s } → 1:{ x1 } 3:{ y2.s } → 4:{ x2 } - 6:{ z.t } → 7:{ y1; y2 } [alias] May-aliases at the end of function main: <none> -[alias] May-alias graph at the end of function main: - 0:{ y1.s } → 1:{ x1 } 3:{ y2.s } → 4:{ x2 } - 6:{ z.t } → 7:{ y1; y2 } -[alias] Summary of function main: - formals: locals: x1 x2 y1 y2 z __retres returns: __retres - state: <none> -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle index f9ca72c149dff417033109d95c9d26a7859d2d75..f4bf90f2a096810f3a34707bcf033f7acb65d88a 100644 --- a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle @@ -2,45 +2,23 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2}; [alias] May-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are <none> -[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is - <empty> [alias] analysing instruction: st_1_t *y1 = malloc(sizeof(st_1_t)); [alias] May-aliases after instruction st_1_t *y1 = malloc(sizeof(st_1_t)); are <none> -[alias] May-alias graph after instruction st_1_t *y1 = malloc(sizeof(st_1_t)); - is 0:{ y1 } → 1:{ } [alias] analysing instruction: st_2_t *z = malloc(sizeof(st_2_t)); [alias] May-aliases after instruction st_2_t *z = malloc(sizeof(st_2_t)); are <none> -[alias] May-alias graph after instruction st_2_t *z = malloc(sizeof(st_2_t)); is - 0:{ y1 } → 1:{ } 2:{ z } → 3:{ } [alias] analysing instruction: y1 = & x1; [alias] May-aliases after instruction y1 = & x1; are <none> -[alias] May-alias graph after instruction y1 = & x1; is - 0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ } [alias] analysing instruction: z->s = (struct struct_1_t *)y1; [alias:unsafe-cast] structure4.c:37: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are { z->s; y1 } -[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is - 2:{ z } → 3:{ } 6:{ z->s; y1 } → 1:{ x1 } [alias] analysing instruction: z->c = 6; [alias] May-aliases after instruction z->c = 6; are { z->s; y1 } -[alias] May-alias graph after instruction z->c = 6; is - 2:{ z } → 3:{ } 6:{ z->s; y1 } → 1:{ x1 } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { z->s; y1 } -[alias] May-alias graph after instruction __retres = 0; is - 2:{ z } → 3:{ } 6:{ z->s; y1 } → 1:{ x1 } [alias] May-aliases at the end of function main: { z->s; y1 } -[alias] May-alias graph at the end of function main: - 2:{ z } → 3:{ } 6:{ z->s; y1 } → 1:{ x1 } -[alias] Summary of function main: - formals: locals: x1 x2 y1→{ x1 } z __retres returns: __retres - state: { z->s; y1 } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle index b7ff584de851515029b8816b9c5dd870b0c6a3f8..a1ddf765fe0bbdb75a406553d196f7732dc0704a 100644 --- a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle +++ b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle @@ -2,81 +2,40 @@ [alias] analysing function: main [alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1}; [alias] May-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are <none> -[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is - <empty> [alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2}; [alias] May-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are <none> -[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is - <empty> [alias] analysing instruction: st_1_t *y1 = malloc(sizeof(st_1_t)); [alias] May-aliases after instruction st_1_t *y1 = malloc(sizeof(st_1_t)); are <none> -[alias] May-alias graph after instruction st_1_t *y1 = malloc(sizeof(st_1_t)); - is 0:{ y1 } → 1:{ } [alias] analysing instruction: st_2_t *z = malloc(sizeof(st_2_t)); [alias] May-aliases after instruction st_2_t *z = malloc(sizeof(st_2_t)); are <none> -[alias] May-alias graph after instruction st_2_t *z = malloc(sizeof(st_2_t)); is - 0:{ y1 } → 1:{ } 2:{ z } → 3:{ } [alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t)); [alias] May-aliases after instruction st_3_t *t = malloc(sizeof(st_3_t)); are <none> -[alias] May-alias graph after instruction st_3_t *t = malloc(sizeof(st_3_t)); is - 0:{ y1 } → 1:{ } 2:{ z } → 3:{ } 4:{ t } → 5:{ } [alias] analysing instruction: int *a = malloc(sizeof(int)); [alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is - 0:{ y1 } → 1:{ } 2:{ z } → 3:{ } 4:{ t } → 5:{ } - 6:{ a } → 7:{ } [alias] analysing instruction: *a = 0; [alias] May-aliases after instruction *a = 0; are <none> -[alias] May-alias graph after instruction *a = 0; is - 0:{ y1 } → 1:{ } 2:{ z } → 3:{ } 4:{ t } → 5:{ } - 6:{ a } → 7:{ } [alias] analysing instruction: y1 = & x1; [alias] May-aliases after instruction y1 = & x1; are <none> -[alias] May-alias graph after instruction y1 = & x1; is - 0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ } 4:{ t } → 5:{ } - 6:{ a } → 7:{ } [alias] analysing instruction: z->s = (struct struct_1_t *)y1; [alias:unsafe-cast] structure5.c:41: Warning: unsafe cast from st_1_t * to struct struct_1_t * [alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are { z->s; y1 } -[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is - 2:{ z } → 3:{ } 4:{ t } → 5:{ } 6:{ a } → 7:{ } - 10:{ z->s; y1 } → 1:{ x1 } [alias] analysing instruction: z->c = a; [alias] May-aliases after instruction z->c = a; are { z->s; y1 } { z->c; a } -[alias] May-alias graph after instruction z->c = a; is - 2:{ z } → 3:{ } 4:{ t } → 5:{ } 10:{ z->s; y1 } → 1:{ x1 } - 11:{ z->c; a } → 7:{ } [alias] analysing instruction: t->t = (struct struct_2_t *)z; [alias:unsafe-cast] structure5.c:43: Warning: unsafe cast from st_2_t * to struct struct_2_t * [alias] May-aliases after instruction t->t = (struct struct_2_t *)z; are { z->s; y1 } { t->t; z } { z->c; a } -[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z; is - 4:{ t } → 5:{ } 10:{ z->s; y1 } → 1:{ x1 } - 11:{ z->c; a } → 7:{ } 12:{ t->t; z } → 3:{ } [alias] analysing instruction: t->d = a; [alias] May-aliases after instruction t->d = a; are { z->s; y1 } { t->t; z } { z->c; t->d; a } -[alias] May-alias graph after instruction t->d = a; is - 4:{ t } → 5:{ } 10:{ z->s; y1 } → 1:{ x1 } - 12:{ t->t; z } → 3:{ } 13:{ z->c; t->d; a } → 7:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { z->s; y1 } { t->t; z } { z->c; t->d; a } -[alias] May-alias graph after instruction __retres = 0; is - 4:{ t } → 5:{ } 10:{ z->s; y1 } → 1:{ x1 } - 12:{ t->t; z } → 3:{ } 13:{ z->c; t->d; a } → 7:{ } [alias] May-aliases at the end of function main: { z->s; y1 } { t->t; z } { z->c; t->d; a } -[alias] May-alias graph at the end of function main: - 4:{ t } → 5:{ } 10:{ z->s; y1 } → 1:{ x1 } - 12:{ t->t; z } → 3:{ } 13:{ z->c; t->d; a } → 7:{ } -[alias] Summary of function main: - formals: locals: x1 x2 y1→{ x1 } z t a __retres - returns: __retres state: { z->s; y1 } { t->t; z } { z->c; t->d; a } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle index 8dba09dab09d56466708a915e19bd895719cb1aa..87ce913aa06f581b18353077f233d3fe2cb759a9 100644 --- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle +++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle @@ -2,340 +2,162 @@ [alias] analysing function: f1 [alias] analysing instruction: ty *tmp = x; [alias] May-aliases after instruction ty *tmp = x; are { x; tmp } -[alias] May-alias graph after instruction ty *tmp = x; is - 0:{ x; tmp } → 1:{ } [alias] analysing instruction: idata = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction idata = (double *)malloc((unsigned long)10 * sizeof(double)); are { x; tmp } -[alias] May-alias graph after instruction - idata = (double *)malloc((unsigned long)10 * sizeof(double)); is - 0:{ x; tmp } → 1:{ } 4:{ idata } → 5:{ } [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t2[0..]; idata } -[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: idx = 0; [alias] May-aliases after instruction idx = 0; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction idx = 0; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: tmp_1 = sin(*(idata + idx)); [alias:undefined:fn] example1.c:45: Warning: function sin has no definition [alias] May-aliases after instruction tmp_1 = sin(*(idata + idx)); are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction tmp_1 = sin(*(idata + idx)); is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: *(odata + idx) = 0.5 * tmp_1; [alias] May-aliases after instruction *(odata + idx) = 0.5 * tmp_1; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction *(odata + idx) = 0.5 * tmp_1; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: idx ++; [alias] May-aliases after instruction idx ++; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction idx ++; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: swap(tmp->n1); [alias] analysing function: swap [alias] analysing instruction: *n = 0; [alias] May-aliases after instruction *n = 0; are <none> -[alias] May-alias graph after instruction *n = 0; is <empty> [alias] analysing instruction: (*n) ++; [alias] May-aliases after instruction (*n) ++; are <none> -[alias] May-alias graph after instruction (*n) ++; is <empty> [alias] May-aliases at the end of function swap: <none> -[alias] May-alias graph at the end of function swap: - <empty> -[alias] Summary of function swap: [alias] May-aliases after instruction swap(tmp->n1); are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction swap(tmp->n1); is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias:no-return] example1.c:29: Warning: function f1 does not return; analysis may be unsound [alias] May-aliases at the end of function f1: <none> -[alias] May-alias graph at the end of function f1: - <empty> -[alias] Summary of function f1: - formals: x locals: tmp idata odata idx tmp_1 __retres - returns: __retres state: <none> [alias] analysing function: f2 [alias] analysing instruction: ty *tmp = x; [alias] May-aliases after instruction ty *tmp = x; are { x; tmp } -[alias] May-alias graph after instruction ty *tmp = x; is - 12:{ x; tmp } → 13:{ } [alias] analysing instruction: idata = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction idata = (double *)malloc((unsigned long)10 * sizeof(double)); are { x; tmp } -[alias] May-alias graph after instruction - idata = (double *)malloc((unsigned long)10 * sizeof(double)); is - 12:{ x; tmp } → 13:{ } 16:{ idata } → 17:{ } [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t1[0..]; idata } -[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: idx = 0; [alias] May-aliases after instruction idx = 0; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction idx = 0; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: *(odata + idx) = (double)3 * *(idata + idx) + (double)1; [alias] May-aliases after instruction *(odata + idx) = (double)3 * *(idata + idx) + (double)1; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction - *(odata + idx) = (double)3 * *(idata + idx) + (double)1; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: idx ++; [alias] May-aliases after instruction idx ++; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction idx ++; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: swap(tmp->n2); [alias] May-aliases after instruction swap(tmp->n2); are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction swap(tmp->n2); is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias:no-return] example1.c:53: Warning: function f2 does not return; analysis may be unsound [alias] May-aliases at the end of function f2: <none> -[alias] May-alias graph at the end of function f2: - <empty> -[alias] Summary of function f2: - formals: x locals: tmp idx idata odata __retres - returns: __retres state: <none> [alias] analysing function: main [alias] analysing instruction: a = (ty *)malloc(sizeof(ty)); [alias] May-aliases after instruction a = (ty *)malloc(sizeof(ty)); are <none> -[alias] May-alias graph after instruction a = (ty *)malloc(sizeof(ty)); is - 24:{ a } → 25:{ } [alias] analysing instruction: b = (ty *)malloc(sizeof(ty)); [alias] May-aliases after instruction b = (ty *)malloc(sizeof(ty)); are <none> -[alias] May-alias graph after instruction b = (ty *)malloc(sizeof(ty)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } [alias] analysing instruction: i = 0; [alias] May-aliases after instruction i = 0; are <none> -[alias] May-alias graph after instruction i = 0; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } [alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } [alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are <none> -[alias] May-alias graph after instruction i ++; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: a->n1 = (int *)malloc(sizeof(int)); [alias] May-aliases after instruction a->n1 = (int *)malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction a->n1 = (int *)malloc(sizeof(int)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } [alias] analysing instruction: a->n2 = (int *)malloc(sizeof(int)); [alias] May-aliases after instruction a->n2 = (int *)malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction a->n2 = (int *)malloc(sizeof(int)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: *(a->n1) = 1; [alias] May-aliases after instruction *(a->n1) = 1; are <none> -[alias] May-alias graph after instruction *(a->n1) = 1; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: *(a->n2) = 1; [alias] May-aliases after instruction *(a->n2) = 1; are <none> -[alias] May-alias graph after instruction *(a->n2) = 1; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: i = 0; [alias] May-aliases after instruction i = 0; are <none> -[alias] May-alias graph after instruction i = 0; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: b->t1[i] = a->t1[i]; [alias] May-aliases after instruction b->t1[i] = a->t1[i]; are { a->t1[0..]; b->t1[0..] } -[alias] May-alias graph after instruction b->t1[i] = a->t1[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 30:{ a->t2[0..] } → 31:{ } - 32:{ a->n1 } → 33:{ } 34:{ a->n2 } → 35:{ } - 36:{ a->t1[0..]; b->t1[0..] } → 29:{ } [alias] analysing instruction: b->t2[i] = a->t2[i]; [alias] May-aliases after instruction b->t2[i] = a->t2[i]; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction b->t2[i] = a->t2[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } 36:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 37:{ a->t2[0..]; b->t2[0..] } → 31:{ } [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction i ++; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } 36:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 37:{ a->t2[0..]; b->t2[0..] } → 31:{ } [alias] analysing instruction: b->t1[i] = a->t1[i]; [alias] May-aliases after instruction b->t1[i] = a->t1[i]; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction b->t1[i] = a->t1[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: b->t2[i] = a->t2[i]; [alias] May-aliases after instruction b->t2[i] = a->t2[i]; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction b->t2[i] = a->t2[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: b->n1 = a->n1; [alias] May-aliases after instruction b->n1 = a->n1; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } -[alias] May-alias graph after instruction b->n1 = a->n1; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 34:{ a->n2 } → 35:{ } - 38:{ a->n1; b->n1 } → 33:{ } [alias] analysing instruction: b->n2 = a->n2; [alias] May-aliases after instruction b->n2 = a->n2; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction b->n2 = a->n2; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] analysing instruction: f1(a); [alias] May-aliases after instruction f1(a); are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction f1(a); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] analysing instruction: f2(b); [alias] May-aliases after instruction f2(b); are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction f2(b); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction __retres = 0; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] May-aliases at the end of function main: { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph at the end of function main: - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } -[alias] Summary of function main: - formals: locals: a b i __retres returns: __retres - state: { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } - { a->n1; b->n1 } { a->n2; b->n2 } [alias] analysing function: swap [alias] May-aliases at the end of function swap: <none> -[alias] May-alias graph at the end of function swap: - <empty> -[alias] Summary of function swap: -[alias] Analysis complete diff --git a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle index 0ef7ddca0a1f36740ad078fa1157700b82d71cbe..b2e81e566d0b2dde3d0de6a27c52dce8cf3d514d 100644 --- a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle +++ b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle @@ -2,374 +2,176 @@ [alias] analysing function: f1 [alias] analysing instruction: ty *tmp = x; [alias] May-aliases after instruction ty *tmp = x; are { x; tmp } -[alias] May-alias graph after instruction ty *tmp = x; is - 0:{ x; tmp } → 1:{ } [alias] analysing instruction: idata = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction idata = (double *)malloc((unsigned long)10 * sizeof(double)); are { x; tmp } -[alias] May-alias graph after instruction - idata = (double *)malloc((unsigned long)10 * sizeof(double)); is - 0:{ x; tmp } → 1:{ } 4:{ idata } → 5:{ } [alias] analysing instruction: int i = 0; [alias] May-aliases after instruction int i = 0; are { x; tmp } -[alias] May-alias graph after instruction int i = 0; is - 0:{ x; tmp } → 1:{ } 4:{ idata } → 5:{ } [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t2[0..]; idata } -[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: idx = 0; [alias] May-aliases after instruction idx = 0; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction idx = 0; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: tmp_1 = sin(*(idata + idx)); [alias:undefined:fn] example2.c:45: Warning: function sin has no definition [alias] May-aliases after instruction tmp_1 = sin(*(idata + idx)); are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction tmp_1 = sin(*(idata + idx)); is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: *(odata + idx) = 0.5 * tmp_1; [alias] May-aliases after instruction *(odata + idx) = 0.5 * tmp_1; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction *(odata + idx) = 0.5 * tmp_1; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: idx ++; [alias] May-aliases after instruction idx ++; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction idx ++; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: swap(tmp->n1); [alias] analysing function: swap [alias] analysing instruction: *n = 0; [alias] May-aliases after instruction *n = 0; are <none> -[alias] May-alias graph after instruction *n = 0; is <empty> [alias] analysing instruction: (*n) ++; [alias] May-aliases after instruction (*n) ++; are <none> -[alias] May-alias graph after instruction (*n) ++; is <empty> [alias] May-aliases at the end of function swap: <none> -[alias] May-alias graph at the end of function swap: - <empty> -[alias] Summary of function swap: [alias] May-aliases after instruction swap(tmp->n1); are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction swap(tmp->n1); is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction i ++; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: idata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction idata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction idata = tmp->t2[*(tmp->n2)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: odata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction odata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t1[*(tmp->n1)]; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] analysing instruction: __retres = (void *)0; [alias] May-aliases after instruction __retres = (void *)0; are { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph after instruction __retres = (void *)0; is - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } [alias] May-aliases at the end of function f1: { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } -[alias] May-alias graph at the end of function f1: - 0:{ x; tmp } → 1:{ } 4:{ tmp->t2[0..]; idata } → 5:{ } - 7:{ tmp->t1[0..]; odata } → 8:{ } -[alias] Summary of function f1: - formals: x locals: tmp idata odata idx i tmp_1 __retres - returns: __retres - state: { x; tmp } { tmp->t2[0..]; idata } { tmp->t1[0..]; odata } [alias] analysing function: f2 [alias] analysing instruction: ty *tmp = x; [alias] May-aliases after instruction ty *tmp = x; are { x; tmp } -[alias] May-alias graph after instruction ty *tmp = x; is - 12:{ x; tmp } → 13:{ } [alias] analysing instruction: idata = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction idata = (double *)malloc((unsigned long)10 * sizeof(double)); are { x; tmp } -[alias] May-alias graph after instruction - idata = (double *)malloc((unsigned long)10 * sizeof(double)); is - 12:{ x; tmp } → 13:{ } 16:{ idata } → 17:{ } [alias] analysing instruction: int i = 0; [alias] May-aliases after instruction int i = 0; are { x; tmp } -[alias] May-alias graph after instruction int i = 0; is - 12:{ x; tmp } → 13:{ } 16:{ idata } → 17:{ } [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t1[0..]; idata } -[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: idx = 0; [alias] May-aliases after instruction idx = 0; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction idx = 0; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: *(odata + idx) = (double)3 * *(idata + idx) + (double)1; [alias] May-aliases after instruction *(odata + idx) = (double)3 * *(idata + idx) + (double)1; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction - *(odata + idx) = (double)3 * *(idata + idx) + (double)1; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: idx ++; [alias] May-aliases after instruction idx ++; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction idx ++; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: swap(tmp->n2); [alias] May-aliases after instruction swap(tmp->n2); are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction swap(tmp->n2); is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction i ++; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: idata = tmp->t1[*(tmp->n1)]; [alias] May-aliases after instruction idata = tmp->t1[*(tmp->n1)]; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction idata = tmp->t1[*(tmp->n1)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: odata = tmp->t2[*(tmp->n2)]; [alias] May-aliases after instruction odata = tmp->t2[*(tmp->n2)]; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction odata = tmp->t2[*(tmp->n2)]; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] analysing instruction: __retres = (void *)0; [alias] May-aliases after instruction __retres = (void *)0; are { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph after instruction __retres = (void *)0; is - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } [alias] May-aliases at the end of function f2: { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } -[alias] May-alias graph at the end of function f2: - 12:{ x; tmp } → 13:{ } 16:{ tmp->t1[0..]; idata } → 17:{ } - 19:{ tmp->t2[0..]; odata } → 20:{ } -[alias] Summary of function f2: - formals: x locals: tmp idx idata odata i __retres - returns: __retres - state: { x; tmp } { tmp->t1[0..]; idata } { tmp->t2[0..]; odata } [alias] analysing function: main [alias] analysing instruction: a = (ty *)malloc(sizeof(ty)); [alias] May-aliases after instruction a = (ty *)malloc(sizeof(ty)); are <none> -[alias] May-alias graph after instruction a = (ty *)malloc(sizeof(ty)); is - 24:{ a } → 25:{ } [alias] analysing instruction: b = (ty *)malloc(sizeof(ty)); [alias] May-aliases after instruction b = (ty *)malloc(sizeof(ty)); are <none> -[alias] May-alias graph after instruction b = (ty *)malloc(sizeof(ty)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } [alias] analysing instruction: i = 0; [alias] May-aliases after instruction i = 0; are <none> -[alias] May-alias graph after instruction i = 0; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } [alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } [alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are <none> -[alias] May-alias graph after instruction i ++; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); [alias] May-aliases after instruction a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); are <none> -[alias] May-alias graph after instruction - a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } [alias] analysing instruction: a->n1 = (int *)malloc(sizeof(int)); [alias] May-aliases after instruction a->n1 = (int *)malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction a->n1 = (int *)malloc(sizeof(int)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } [alias] analysing instruction: a->n2 = (int *)malloc(sizeof(int)); [alias] May-aliases after instruction a->n2 = (int *)malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction a->n2 = (int *)malloc(sizeof(int)); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: *(a->n1) = 1; [alias] May-aliases after instruction *(a->n1) = 1; are <none> -[alias] May-alias graph after instruction *(a->n1) = 1; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: *(a->n2) = 1; [alias] May-aliases after instruction *(a->n2) = 1; are <none> -[alias] May-alias graph after instruction *(a->n2) = 1; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: i = 0; [alias] May-aliases after instruction i = 0; are <none> -[alias] May-alias graph after instruction i = 0; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 28:{ a->t1[0..] } → 29:{ } - 30:{ a->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: b->t1[i] = a->t1[i]; [alias] May-aliases after instruction b->t1[i] = a->t1[i]; are { a->t1[0..]; b->t1[0..] } -[alias] May-alias graph after instruction b->t1[i] = a->t1[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 30:{ a->t2[0..] } → 31:{ } - 32:{ a->n1 } → 33:{ } 34:{ a->n2 } → 35:{ } - 36:{ a->t1[0..]; b->t1[0..] } → 29:{ } [alias] analysing instruction: b->t2[i] = a->t2[i]; [alias] May-aliases after instruction b->t2[i] = a->t2[i]; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction b->t2[i] = a->t2[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } 36:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 37:{ a->t2[0..]; b->t2[0..] } → 31:{ } [alias] analysing instruction: i ++; [alias] May-aliases after instruction i ++; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction i ++; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } 36:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 37:{ a->t2[0..]; b->t2[0..] } → 31:{ } [alias] analysing instruction: b->t1[i] = a->t1[i]; [alias] May-aliases after instruction b->t1[i] = a->t1[i]; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction b->t1[i] = a->t1[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: b->t2[i] = a->t2[i]; [alias] May-aliases after instruction b->t2[i] = a->t2[i]; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } -[alias] May-alias graph after instruction b->t2[i] = a->t2[i]; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 32:{ a->n1 } → 33:{ } - 34:{ a->n2 } → 35:{ } [alias] analysing instruction: b->n1 = a->n1; [alias] May-aliases after instruction b->n1 = a->n1; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } -[alias] May-alias graph after instruction b->n1 = a->n1; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 34:{ a->n2 } → 35:{ } - 38:{ a->n1; b->n1 } → 33:{ } [alias] analysing instruction: b->n2 = a->n2; [alias] May-aliases after instruction b->n2 = a->n2; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction b->n2 = a->n2; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] analysing instruction: f1(a); [alias] May-aliases after instruction f1(a); are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction f1(a); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] analysing instruction: f2(b); [alias] May-aliases after instruction f2(b); are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction f2(b); is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph after instruction __retres = 0; is - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } [alias] May-aliases at the end of function main: { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } { a->n1; b->n1 } { a->n2; b->n2 } -[alias] May-alias graph at the end of function main: - 24:{ a } → 25:{ } 26:{ b } → 27:{ } - 28:{ a->t1[0..]; b->t1[0..] } → 29:{ } - 30:{ a->t2[0..]; b->t2[0..] } → 31:{ } 38:{ a->n1; b->n1 } → 33:{ } - 39:{ a->n2; b->n2 } → 35:{ } -[alias] Summary of function main: - formals: locals: a b i __retres returns: __retres - state: { a->t1[0..]; b->t1[0..] } { a->t2[0..]; b->t2[0..] } - { a->n1; b->n1 } { a->n2; b->n2 } [alias] analysing function: swap [alias] May-aliases at the end of function swap: <none> -[alias] May-alias graph at the end of function swap: - <empty> -[alias] Summary of function swap: -[alias] Analysis complete diff --git a/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle b/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle index f1ed57eb7264c381d52b03f3f300e6b3f31c02f3..db7c9c9b91f3b8ae4c1b5469e2e76229cffbfdc6 100644 --- a/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle +++ b/src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle @@ -2,45 +2,20 @@ [alias] analysing function: alias [alias] analysing instruction: *x = *y; [alias] May-aliases after instruction *x = *y; are { x; y } -[alias] May-alias graph after instruction *x = *y; is - 0:{ x } → 1:{ *x; *y } 2:{ y } → 1:{ *x; *y } [alias] May-aliases at the end of function alias: { x; y } -[alias] May-alias graph at the end of function alias: - 0:{ x } → 1:{ *x; *y } 2:{ y } → 1:{ *x; *y } -[alias] Summary of function alias: - formals: x→{ *x; *y } y→{ *x; *y } locals: returns: <none> - state: { x; y } [alias] analysing function: main [alias] analysing instruction: int *a = malloc(sizeof(int)); [alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is - 4:{ a } → 5:{ } [alias] analysing instruction: *a = 0; [alias] May-aliases after instruction *a = 0; are <none> -[alias] May-alias graph after instruction *a = 0; is 4:{ a } → 5:{ } [alias] analysing instruction: int *b = malloc(sizeof(int)); [alias] May-aliases after instruction int *b = malloc(sizeof(int)); are <none> -[alias] May-alias graph after instruction int *b = malloc(sizeof(int)); is - 4:{ a } → 5:{ } 6:{ b } → 7:{ } [alias] analysing instruction: *b = 42; [alias] May-aliases after instruction *b = 42; are <none> -[alias] May-alias graph after instruction *b = 42; is - 4:{ a } → 5:{ } 6:{ b } → 7:{ } [alias] analysing instruction: alias(& a,& b); [alias] May-aliases after instruction alias(& a,& b); are { a; b } -[alias] May-alias graph after instruction alias(& a,& b); is - 4:{ a; b } → 5:{ } 11:{ } → 4:{ a; b } 12:{ } → 4:{ a; b } [alias] analysing instruction: *a = 7; [alias] May-aliases after instruction *a = 7; are { a; b } -[alias] May-alias graph after instruction *a = 7; is - 4:{ a; b } → 5:{ } 11:{ } → 4:{ a; b } 12:{ } → 4:{ a; b } [alias] analysing instruction: __retres = 0; [alias] May-aliases after instruction __retres = 0; are { a; b } -[alias] May-alias graph after instruction __retres = 0; is - 4:{ a; b } → 5:{ } 11:{ } → 4:{ a; b } 12:{ } → 4:{ a; b } [alias] May-aliases at the end of function main: { a; b } -[alias] May-alias graph at the end of function main: - 4:{ a; b } → 5:{ } 11:{ } → 4:{ a; b } 12:{ } → 4:{ a; b } -[alias] Summary of function main: - formals: locals: a b __retres returns: __retres state: { a; b } -[alias] Analysis complete diff --git a/src/plugins/alias/tests/test_config b/src/plugins/alias/tests/test_config index 80976f50aac4719cd461142fbf18921cc32c3768..e14c0a6d24720b60c9a29eb36a4bb4cd432e5b55 100644 --- a/src/plugins/alias/tests/test_config +++ b/src/plugins/alias/tests/test_config @@ -1,2 +1,2 @@ PLUGIN: alias -OPT: -alias -alias-verbose 3 -alias-debug 3 +OPT: -alias -alias-verbose 3