Skip to content
Snippets Groups Projects
Commit 38d3796d authored by Tristan Le Gall's avatar Tristan Le Gall
Browse files

Merge branch 'jan/alias-global-vars' into 'master' 

[alias] take into account global variable definitions

See merge request frama-c/frama-c!4727
parents f53ce904 1be619e0
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2085 additions and 1062 deletions
src/plugins/alias/src/analysis.ml
+ 57
− 30
View file @ 38d3796d
......@@ -66,6 +66,9 @@ module Stmt_table = struct
type value = data
end
(* Abstract state after taking into account all global variable definitions *)
let initial_state = ref @@ Some Abstract_state.empty
let warn_unsupported_explicit_pointer pp_obj obj loc =
Options.warning ~source:(fst loc) ~wkey:Options.Warn.unsupported_address
"unsupported feature: explicit pointer address: %a; analysis may be unsound" pp_obj obj
......@@ -82,7 +85,31 @@ let rec do_init (lv:lval) (init:init) state =
| CompoundInit (_, l) ->
List.fold_left (fun state (o, init) -> do_init (Cil.addOffsetLval o lv) init state) state l
let doFunction f = !function_compute_ref f
let pp_abstract_state_opt ?(debug=false) fmt v =
match v with
| None -> Format.fprintf fmt "⊥"
| Some a -> Abstract_state.pretty ~debug fmt a
let analyse_global_var v initinfo st =
match initinfo.init with
| None -> st
| Some init ->
Options.feedback ~level:3
"@[analysing global variable definiton:@ @[%a@]@ =@ @[%a@];@]"
Printer.pp_varinfo v
Printer.pp_initinfo initinfo;
let result = do_init (Var v, NoOffset) init st in
Options.feedback ~level:3
"@[May-aliases after global variable definition@;<2>@[%a@]@;<2>are@;<2>@[%a@]@]"
Printer.pp_varinfo v
(pp_abstract_state_opt ~debug:false) result;
Options.debug ~level:3
"@[May-alias graph after global variable definition@;<2>@[%a@]@;<2>is@;<4>@[%a@]@]"
Printer.pp_varinfo v
(pp_abstract_state_opt ~debug:true) result;
result
let analyse_function f = !function_compute_ref f
let do_function_call (stmt:stmt) state (res : lval option) (ef : exp) (args: exp list) loc =
let is_malloc (s:string) : bool =
......@@ -101,7 +128,9 @@ let do_function_call (stmt:stmt) state (res : lval option) (ef : exp) (args: exp
Some a
end
| _ -> (* general case *)
let get_function kf = try Function_table.find kf with Not_found -> doFunction kf in
let get_function kf =
try Function_table.find kf
with Not_found -> analyse_function kf in
let summaries =
match Kernel_function.get_called ef with
| Some kf when Kernel_function.is_main kf -> []
......@@ -150,11 +179,6 @@ let analyse_instr (s:stmt) (i:instr) (a:Abstract_state.t option) : Abstract_stat
"unsupported feature: assembler code; skipping";
a
let pp_abstract_state_opt ?(debug=false) fmt v =
match v with
| None -> Format.fprintf fmt "⊥"
| Some a -> Abstract_state.pretty ~debug fmt a
let do_instr (s:stmt) (i:instr) (a:Abstract_state.t option) : Abstract_state.t option =
Options.feedback ~level:3 "@[analysing instruction:@ %a@]" Printer.pp_stmt s;
let result = analyse_instr s i a in
......@@ -213,26 +237,27 @@ let do_stmt (a: Abstract_state.t) (s:stmt) : Abstract_state.t =
| _ -> a
let analyse_function (kf:kernel_function) =
if not @@ Kernel_function.has_definition kf then None else begin
Options.feedback ~level:2 "analysing function: %a" Kernel_function.pretty kf;
let first_stmt =
try Kernel_function.find_first_stmt kf
with Kernel_function.No_Statement -> assert false
in
T.StmtStartData.add first_stmt (Some Abstract_state.empty);
F.compute [first_stmt];
let return_stmt = Kernel_function.find_return kf in
try Stmt_table.find return_stmt
with Not_found ->
let source, _ = Kernel_function.get_location kf in
Options.warning ~source ~wkey:Options.Warn.no_return_stmt
"function %a does not return; analysis may be unsound"
Kernel_function.pretty kf;
Some Abstract_state.empty
end
let doFunction (kf:kernel_function) =
let final_state = analyse_function kf in
let final_state =
if not @@ Kernel_function.has_definition kf then None else
let () =
Options.feedback ~level:2 "analysing function: %a"
Kernel_function.pretty kf
in
let first_stmt =
try Kernel_function.find_first_stmt kf
with Kernel_function.No_Statement -> assert false
in
T.StmtStartData.add first_stmt !initial_state;
F.compute [first_stmt];
let return_stmt = Kernel_function.find_return kf in
try Stmt_table.find return_stmt
with Not_found ->
let source, _ = Kernel_function.get_location kf in
Options.warning ~source ~wkey:Options.Warn.no_return_stmt
"function %a does not return; analysis may be unsound"
Kernel_function.pretty kf;
!initial_state
in
let level = if Kernel_function.is_main kf then 1 else 2 in
final_state |> Option.iter (fun s ->
Options.feedback ~level "@[May-aliases at the end of function %a:@ @[%a@]"
......@@ -262,7 +287,7 @@ let doFunction (kf:kernel_function) =
Function_table.add kf result;
result
let () = function_compute_ref := doFunction
let () = function_compute_ref := analyse_function
let make_summary (state:Abstract_state.t) (kf:kernel_function) =
try begin match Function_table.find kf with
......@@ -270,7 +295,7 @@ let make_summary (state:Abstract_state.t) (kf:kernel_function) =
| None -> Options.fatal "not implemented"
end
with Not_found ->
begin match doFunction kf with
begin match analyse_function kf with
| Some s -> (state, s)
| None -> Options.fatal "not implemented"
end
......@@ -299,7 +324,8 @@ let print_function_table_elt fmt kf s : unit =
let compute () =
Ast.compute ();
Globals.Functions.iter (fun kf -> ignore @@ doFunction kf);
initial_state := Globals.Vars.fold_in_file_order analyse_global_var (Some Abstract_state.empty);
Globals.Functions.iter (fun kf -> ignore @@ analyse_function kf);
computed_flag := true;
if Options.ShowStmtTable.get () then
Stmt_table.iter (print_stmt_table_elt Format.std_formatter);
......@@ -308,6 +334,7 @@ let compute () =
let clear () =
computed_flag := false;
initial_state := Some Abstract_state.empty;
Stmt_table.clear ()
let get_state_before_stmt stmt =
......
src/plugins/alias/tests/basic/assignment3.c
+ 2
− 4
View file @ 38d3796d
// address assignment
// {a, c} are aliased
int main () {
int b=0, *a=&b, *c=&b;
int *a=0, b=0, *c=0;
a = &b;
c = &b;
int main () {
return 0;
}
src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+ 11
− 16
View file @ 38d3796d
[kernel] Parsing assignment3.c (with preprocessing)
[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
[alias] analysing global variable definiton: b = 0;
[alias] May-aliases after global variable definition b are <none>
[alias] May-alias graph after global variable definition b is <empty>
[alias] analysing global variable definiton: a = & b;
[alias] May-aliases after global variable definition a are <none>
[alias] May-alias graph after global variable definition a is
0:{ a } → 1:{ b }
[alias] analysing global variable definiton: c = & b;
[alias] May-aliases after global variable definition c are { a; c }
[alias] May-alias graph after global variable definition c is
0:{ a } → 5:{ b } 4:{ c } → 5:{ b }
[alias] analysing function: main
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are { a; c }
[alias] May-alias graph after instruction __retres = 0; is
......
src/plugins/alias/tests/basic/oracle/function2.res.oracle
+ 60
− 25
View file @ 38d3796d
[kernel] Parsing function2.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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] May-aliases after instruction int *a = (int *)0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *a = (int *)0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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] May-aliases after instruction int *b = (int *)0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *b = (int *)0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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] May-aliases after instruction int *res = (int *)0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *res = (int *)0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[alias] analysing instruction: res = (int *)malloc((size_t)size);
[alias] May-aliases after instruction res = (int *)malloc((size_t)size); are
<none>
{ __fc_random48_counter; __fc_p_random48_counter }
[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>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ res } → 5:{ }
[alias] May-aliases at the end of function my_malloc:
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph at the end of function my_malloc:
0:{ res } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ res } → 5:{ }
[alias] Summary of function my_malloc:
formals: size returns: res state: <none>
[alias] May-aliases after instruction a = my_malloc(2); are <none>
formals: size returns: res
state: { __fc_random48_counter; __fc_p_random48_counter }
[alias] May-aliases after instruction a = my_malloc(2); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction a = my_malloc(2); is
4:{ a } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
12:{ a } → 11:{ }
[alias] analysing instruction: b = my_malloc(3);
[alias] May-aliases after instruction b = my_malloc(3); are <none>
[alias] May-aliases after instruction b = my_malloc(3); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction b = my_malloc(3); is
4:{ a } → 3:{ } 8:{ b } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
12:{ a } → 11:{ } 20:{ b } → 19:{ }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are <none>
[alias] May-aliases after instruction __retres = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[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>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
12:{ a } → 11:{ } 20:{ b } → 19:{ }
[alias] May-aliases at the end of function main:
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph at the end of function main:
4:{ a } → 3:{ } 8:{ b } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
12:{ a } → 11:{ } 20:{ b } → 19:{ }
[alias] Summary of function main:
formals: returns: __retres state: <none>
formals: returns: __retres
state: { __fc_random48_counter; __fc_p_random48_counter }
[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-aliases after instruction int *res = (int *)0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *res = (int *)0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[alias] May-aliases at the end of function my_malloc:
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph at the end of function my_malloc:
0:{ res } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ res } → 5:{ }
[alias] Summary of function my_malloc:
formals: size returns: res state: <none>
formals: size returns: res
state: { __fc_random48_counter; __fc_p_random48_counter }
[alias] Analysis complete
src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
+ 43
− 15
View file @ 38d3796d
[kernel] Parsing while_for1.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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] May-aliases after instruction int *s = (int *)0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *s = (int *)0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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] May-aliases after instruction int idx = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int idx = 0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 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-aliases after instruction s = (int *)malloc((size_t)idx); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction s = (int *)malloc((size_t)idx); is
0:{ s } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ s } → 5:{ }
[alias] analysing instruction: idx ++;
[alias] May-aliases after instruction idx ++; are <none>
[alias] May-alias graph after instruction idx ++; is 0:{ s } → 1:{ }
[alias] May-aliases after instruction idx ++; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction idx ++; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ s } → 5:{ }
[alias] analysing instruction: s = (int *)malloc((size_t)idx);
[alias] May-aliases after instruction s = (int *)malloc((size_t)idx); are <none>
[alias] May-aliases after instruction s = (int *)malloc((size_t)idx); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction s = (int *)malloc((size_t)idx); is
0:{ s } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ s } → 5:{ }
[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-aliases after instruction __retres = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction __retres = 0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ s } → 5:{ }
[alias] May-aliases at the end of function main:
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph at the end of function main:
0:{ s } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ s } → 5:{ }
[alias] Summary of function main:
formals: returns: __retres state: <none>
formals: returns: __retres
state: { __fc_random48_counter; __fc_p_random48_counter }
[alias] Analysis complete
src/plugins/alias/tests/fixed_bugs/oracle/arrays.res.oracle
+ 53
− 21
View file @ 38d3796d
[kernel] Parsing arrays.c (with preprocessing)
[alias] analysing global variable definiton: __fc_p_fopen = __fc_fopen;
[alias] May-aliases after global variable definition __fc_p_fopen are
{ __fc_fopen; __fc_p_fopen }
[alias] May-alias graph after global variable definition __fc_p_fopen is
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
[alias] analysing global variable definiton: __fc_p_tmpnam = __fc_tmpnam;
[alias] May-aliases after global variable definition __fc_p_tmpnam are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
[alias] May-alias graph after global variable definition __fc_p_tmpnam is
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ }
[alias] analysing function: main
[alias] analysing instruction: t[0] = a;
[alias] May-aliases after instruction t[0] = a; are { a; t[0..] }
[alias] May-aliases after instruction t[0] = a; are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { a; t[0..] }
[alias] May-alias graph after instruction t[0] = a; is
0:{ t } → 1:{ a } 1:{ a } → 2:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 8:{ t } → 9:{ a }
9:{ a } → 10:{ }
[alias] analysing instruction: z = & t;
[alias] May-aliases after instruction z = & t; are
{ *z; t } { (*z)[0..]; a; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { *z; t }
{ (*z)[0..]; a; t[0..] }
[alias] May-alias graph after instruction z = & t; is
5:{ z } → 6:{ t } 6:{ t } → 7:{ a } 7:{ a } → 8:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 13:{ z } → 14:{ t }
14:{ t } → 15:{ a } 15:{ a } → 16:{ }
[alias] analysing instruction: q = z;
[alias] May-aliases after instruction q = z; are
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ *z; *q; t } { (*z)[0..]; (*q)[0..]; a; t[0..] }
[alias] May-alias graph after instruction q = z; is
10:{ z; q } → 11:{ t } 11:{ t } → 12:{ a } 12:{ a } → 13:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 18:{ z; q } → 19:{ t }
19:{ t } → 20:{ a } 20:{ a } → 21:{ }
[alias] analysing instruction: b = (*(z + 0))[0];
[alias] May-aliases after instruction b = (*(z + 0))[0]; are
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; t[0..] }
[alias] May-alias graph after instruction b = (*(z + 0))[0]; is
10:{ z; q } → 11:{ t } 11:{ t } → 14:{ a; b } 14:{ a; b } → 15:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 18:{ z; q } → 19:{ t }
19:{ t } → 22:{ a; b } 22:{ a; b } → 23:{ }
[alias] analysing instruction: n = (*(q + 0))[0];
[alias] May-aliases after instruction n = (*(q + 0))[0]; are
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
[alias] May-alias graph after instruction n = (*(q + 0))[0]; is
10:{ z; q } → 11:{ t } 11:{ t } → 16:{ a; b; n }
16:{ a; b; n } → 17:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 18:{ z; q } → 19:{ t }
19:{ t } → 24:{ a; b; n } 24:{ a; b; n } → 25:{ }
[alias] analysing instruction: printf("%d\n%d\n",a == b,a == n);
[alias:undefined:fn] arrays.c:17: Warning: function printf has no definition
[alias] May-aliases after instruction printf("%d\n%d\n",a == b,a == n); are
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
[alias] May-alias graph after instruction printf("%d\n%d\n",a == b,a == n); is
10:{ z; q } → 11:{ t } 11:{ t } → 16:{ a; b; n }
16:{ a; b; n } → 17:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 18:{ z; q } → 19:{ t }
19:{ t } → 24:{ a; b; n } 24:{ a; b; n } → 25:{ }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
[alias] May-alias graph after instruction __retres = 0; is
10:{ z; q } → 11:{ t } 11:{ t } → 16:{ a; b; n }
16:{ a; b; n } → 17:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 18:{ z; q } → 19:{ t }
19:{ t } → 24:{ a; b; n } 24:{ a; b; n } → 25:{ }
[alias] May-aliases at the end of function main:
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
[alias] May-alias graph at the end of function main:
10:{ z; q } → 11:{ t } 11:{ t } → 16:{ a; b; n }
16:{ a; b; n } → 17:{ }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 18:{ z; q } → 19:{ t }
19:{ t } → 24:{ a; b; n } 24:{ a; b; n } → 25:{ }
[alias] Summary of function main:
formals: returns: __retres
state: { z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
state: { __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
{ z; q } { *z; *q; t } { (*z)[0..]; (*q)[0..]; a; b; n; t[0..] }
[alias] Analysis complete
src/plugins/alias/tests/fixed_bugs/oracle/records.res.oracle
+ 58
− 23
View file @ 38d3796d
[kernel] Parsing records.c (with preprocessing)
[alias] analysing global variable definiton: __fc_p_fopen = __fc_fopen;
[alias] May-aliases after global variable definition __fc_p_fopen are
{ __fc_fopen; __fc_p_fopen }
[alias] May-alias graph after global variable definition __fc_p_fopen is
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
[alias] analysing global variable definiton: __fc_p_tmpnam = __fc_tmpnam;
[alias] May-aliases after global variable definition __fc_p_tmpnam are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
[alias] May-alias graph after global variable definition __fc_p_tmpnam is
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ }
[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] May-aliases after instruction a = & x; are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
[alias] May-alias graph after instruction a = & x; is
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 8:{ a } → 9:{ x }
[alias] analysing instruction: t.field = a;
[alias] May-aliases after instruction t.field = a; are { a; t.field }
[alias] May-aliases after instruction t.field = a; are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { a; t.field }
[alias] May-alias graph after instruction t.field = a; is
4:{ t } -field→ 5:{ a } 5:{ a } → 1:{ x }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 12:{ t } -field→ 13:{ a }
13:{ a } → 9:{ x }
[alias] analysing instruction: z = & t;
[alias] May-aliases after instruction z = & t; are { z->field; a; t.field }
[alias] May-aliases after instruction z = & t; are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
{ z->field; a; t.field }
[alias] May-alias graph after instruction z = & t; is
5:{ a } → 1:{ x } 6:{ z } → 7:{ t } 7:{ t } -field→ 5:{ a }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 13:{ a } → 9:{ x }
14:{ z } → 15:{ t } 15:{ t } -field→ 13:{ a }
[alias] analysing instruction: q = z;
[alias] May-aliases after instruction q = z; are
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
{ z->field; q->field; a; t.field } { z; q }
[alias] May-alias graph after instruction q = z; is
5:{ a } → 1:{ x } 9:{ z; q } → 10:{ t } 10:{ t } -field→ 5:{ a }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 13:{ a } → 9:{ x }
17:{ z; q } → 18:{ t } 18:{ t } -field→ 13:{ a }
[alias] analysing instruction: b = z->field;
[alias] May-aliases after instruction b = z->field; are
{ z; q } { z->field; q->field; a; b; t.field }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ z->field; q->field; a; b; t.field }
[alias] May-alias graph after instruction b = z->field; is
9:{ z; q } → 10:{ t } 10:{ t } -field→ 11:{ a; b }
11:{ a; b } → 12:{ x }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 17:{ z; q } → 18:{ t }
18:{ t } -field→ 19:{ a; b } 19:{ a; b } → 20:{ x }
[alias] analysing instruction: n = q->field;
[alias] May-aliases after instruction n = q->field; are
{ z; q } { z->field; q->field; a; b; n; t.field }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ z->field; q->field; a; b; n; t.field }
[alias] May-alias graph after instruction n = q->field; is
9:{ z; q } → 10:{ t } 10:{ t } -field→ 13:{ a; b; n }
13:{ a; b; n } → 14:{ x }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 17:{ z; q } → 18:{ t }
18:{ t } -field→ 21:{ a; b; n } 21:{ a; b; n } → 22:{ x }
[alias] analysing instruction: printf("%d\n%d\n",a == b,a == n);
[alias:undefined:fn] records.c:21: Warning: function printf has no definition
[alias] May-aliases after instruction printf("%d\n%d\n",a == b,a == n); are
{ z; q } { z->field; q->field; a; b; n; t.field }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ z->field; q->field; a; b; n; t.field }
[alias] May-alias graph after instruction printf("%d\n%d\n",a == b,a == n); is
9:{ z; q } → 10:{ t } 10:{ t } -field→ 13:{ a; b; n }
13:{ a; b; n } → 14:{ x }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 17:{ z; q } → 18:{ t }
18:{ t } -field→ 21:{ a; b; n } 21:{ a; b; n } → 22:{ x }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are
{ z; q } { z->field; q->field; a; b; n; t.field }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ z->field; q->field; a; b; n; t.field }
[alias] May-alias graph after instruction __retres = 0; is
9:{ z; q } → 10:{ t } 10:{ t } -field→ 13:{ a; b; n }
13:{ a; b; n } → 14:{ x }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 17:{ z; q } → 18:{ t }
18:{ t } -field→ 21:{ a; b; n } 21:{ a; b; n } → 22:{ x }
[alias] May-aliases at the end of function main:
{ z; q } { z->field; q->field; a; b; n; t.field }
{ __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam } { z; q }
{ z->field; q->field; a; b; n; t.field }
[alias] May-alias graph at the end of function main:
9:{ z; q } → 10:{ t } 10:{ t } -field→ 13:{ a; b; n }
13:{ a; b; n } → 14:{ x }
0:{ __fc_fopen; __fc_p_fopen } → 1:{ }
4:{ __fc_tmpnam; __fc_p_tmpnam } → 5:{ } 17:{ z; q } → 18:{ t }
18:{ t } -field→ 21:{ a; b; n } 21:{ a; b; n } → 22:{ x }
[alias] Summary of function main:
formals: returns: __retres
state: { z; q } { z->field; q->field; a; b; n; t.field }
state: { __fc_fopen; __fc_p_fopen } { __fc_tmpnam; __fc_p_tmpnam }
{ z; q } { z->field; q->field; a; b; n; t.field }
[alias] Analysis complete
src/plugins/alias/tests/offsets/oracle/array3.res.oracle
+ 38
− 13
View file @ 38d3796d
[kernel] Parsing array3.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[alias] analysing function: main
[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>
int *x = malloc((unsigned long)4 * sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction
int *x = malloc((unsigned long)4 * sizeof(int)); is 0:{ x } → 1:{ }
int *x = malloc((unsigned long)4 * sizeof(int)); is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ x } → 5:{ }
[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>
int *y = malloc((unsigned long)4 * sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction
int *y = malloc((unsigned long)4 * sizeof(int)); is
0:{ x } → 1:{ } 2:{ y } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ x } → 5:{ } 6:{ y } → 7:{ }
[alias] analysing instruction: x = mat[0];
[alias] May-aliases after instruction x = mat[0]; are { mat[0..]; x }
[alias] May-aliases after instruction x = mat[0]; are
{ __fc_random48_counter; __fc_p_random48_counter } { mat[0..]; x }
[alias] May-alias graph after instruction x = mat[0]; is
0:{ x } → 1:{ } 2:{ y } → 3:{ } 4:{ mat } → 0:{ x }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ x } → 5:{ } 6:{ y } → 7:{ } 8:{ mat } → 4:{ x }
[alias] analysing instruction: y = mat[1];
[alias] May-aliases after instruction y = mat[1]; are { mat[0..]; x; y }
[alias] May-aliases after instruction y = mat[1]; are
{ __fc_random48_counter; __fc_p_random48_counter } { mat[0..]; x; y }
[alias] May-alias graph after instruction y = mat[1]; is
2:{ x; y } → 3:{ } 4:{ mat } → 2:{ x; y }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ x; y } → 7:{ } 8:{ mat } → 6:{ x; y }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are { mat[0..]; x; y }
[alias] May-aliases after instruction __retres = 0; are
{ __fc_random48_counter; __fc_p_random48_counter } { mat[0..]; x; y }
[alias] May-alias graph after instruction __retres = 0; is
2:{ x; y } → 3:{ } 4:{ mat } → 2:{ x; y }
[alias] May-aliases at the end of function main: { mat[0..]; x; y }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ x; y } → 7:{ } 8:{ mat } → 6:{ x; y }
[alias] May-aliases at the end of function main:
{ __fc_random48_counter; __fc_p_random48_counter } { mat[0..]; x; y }
[alias] May-alias graph at the end of function main:
2:{ x; y } → 3:{ } 4:{ mat } → 2:{ x; y }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ x; y } → 7:{ } 8:{ mat } → 6:{ x; y }
[alias] Summary of function main:
formals: returns: __retres state: { mat[0..]; x; y }
formals: returns: __retres
state: { __fc_random48_counter; __fc_p_random48_counter } { mat[0..]; x; y }
[alias] Analysis complete
src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
+ 111
− 66
View file @ 38d3796d
[kernel] Parsing nested1.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[alias] analysing instruction: tab_y[0] = & x1;
[alias] May-aliases after instruction tab_y[0] = & x1; are <none>
[alias] May-aliases after instruction tab_y[0] = & x1; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction tab_y[0] = & x1; is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1 }
[alias] analysing instruction: tab_y[1] = & x2;
[alias] May-aliases after instruction tab_y[1] = & x2; are <none>
[alias] May-aliases after instruction tab_y[1] = & x2; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction tab_y[1] = & x2; is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ 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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_2_t *z1 = malloc(sizeof(st_2_t));
is 0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_2_t *z2 = malloc(sizeof(st_2_t));
is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
9:{ z2 } → 10:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
13:{ z2 } → 14:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_3_t *t = malloc(sizeof(st_3_t)); is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
9:{ z2 } → 10:{ } 11:{ t } → 12:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
13:{ z2 } → 14:{ } 15:{ t } → 16:{ }
[alias] analysing instruction: int *a = malloc(sizeof(int));
[alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none>
[alias] May-aliases after instruction int *a = malloc(sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
13:{ z2 } → 14:{ } 15:{ t } → 16:{ } 17:{ a } → 18:{ }
[alias] analysing instruction: int *b = malloc(sizeof(int));
[alias] May-aliases after instruction int *b = malloc(sizeof(int)); are <none>
[alias] May-aliases after instruction int *b = malloc(sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *b = malloc(sizeof(int)); is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
15:{ b } → 16:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
13:{ z2 } → 14:{ } 15:{ t } → 16:{ } 17:{ a } → 18:{ }
19:{ b } → 20:{ }
[alias] analysing instruction: *a = 0;
[alias] May-aliases after instruction *a = 0; are <none>
[alias] May-aliases after instruction *a = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction *a = 0; is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
15:{ b } → 16:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
13:{ z2 } → 14:{ } 15:{ t } → 16:{ } 17:{ a } → 18:{ }
19:{ b } → 20:{ }
[alias] analysing instruction: *b = 5;
[alias] May-aliases after instruction *b = 5; are <none>
[alias] May-aliases after instruction *b = 5; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction *b = 5; is
0:{ tab_y } → 1:{ } 1:{ } → 2:{ x1; x2 } 7:{ z1 } → 8:{ }
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
15:{ b } → 16:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 5:{ } 5:{ } → 6:{ x1; x2 } 11:{ z1 } → 12:{ }
13:{ z2 } → 14:{ } 15:{ t } → 16:{ } 17:{ a } → 18:{ }
19:{ b } → 20:{ }
[alias] analysing instruction: z1->s = (struct struct_1_t *)tab_y[0];
[alias] May-aliases after instruction z1->s = (struct struct_1_t *)tab_y[0]; are
{ z1->s; tab_y[0..] }
{ __fc_random48_counter; __fc_p_random48_counter } { z1->s; tab_y[0..] }
[alias] May-alias graph after instruction z1->s = (struct struct_1_t *)tab_y[0];
is
0:{ tab_y } → 17:{ } 7:{ z1 } → 8:{ } 8:{ } -s→ 17:{ }
9:{ z2 } → 10:{ } 11:{ t } → 12:{ } 13:{ a } → 14:{ }
15:{ b } → 16:{ } 17:{ } → 2:{ x1; x2 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 21:{ } 11:{ z1 } → 12:{ } 12:{ } -s→ 21:{ }
13:{ z2 } → 14:{ } 15:{ t } → 16:{ } 17:{ a } → 18:{ }
19:{ b } → 20:{ } 21:{ } → 6:{ x1; x2 }
[alias] analysing instruction: z2->s = (struct struct_1_t *)tab_y[1];
[alias] May-aliases after instruction z2->s = (struct struct_1_t *)tab_y[1]; are
{ __fc_random48_counter; __fc_p_random48_counter }
{ z1->s; z2->s; tab_y[0..] }
[alias] May-alias graph after instruction z2->s = (struct struct_1_t *)tab_y[1];
is
0:{ tab_y } → 18:{ } 7:{ z1 } → 8:{ } 8:{ } -s→ 18:{ }
9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ } 11:{ t } → 12:{ }
13:{ a } → 14:{ } 15:{ b } → 16:{ } 18:{ } → 2:{ x1; x2 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 11:{ z1 } → 12:{ } 12:{ } -s→ 22:{ }
13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ } 15:{ t } → 16:{ }
17:{ a } → 18:{ } 19:{ b } → 20:{ } 22:{ } → 6:{ x1; x2 }
[alias] analysing instruction: z1->c = a;
[alias] May-aliases after instruction z1->c = a; are
{ __fc_random48_counter; __fc_p_random48_counter }
{ z1->s; z2->s; tab_y[0..] } { z1->c; a }
[alias] May-alias graph after instruction z1->c = a; is
0:{ tab_y } → 18:{ } 7:{ z1 } → 8:{ } 8:{ } -s→ 18:{ }
8:{ } -c→ 19:{ a } 9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ }
11:{ t } → 12:{ } 15:{ b } → 16:{ } 18:{ } → 2:{ x1; x2 }
19:{ a } → 14:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 11:{ z1 } → 12:{ } 12:{ } -s→ 22:{ }
12:{ } -c→ 23:{ a } 13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ }
15:{ t } → 16:{ } 19:{ b } → 20:{ } 22:{ } → 6:{ x1; x2 }
23:{ a } → 18:{ }
[alias] analysing instruction: z2->c = b;
[alias] May-aliases after instruction z2->c = b; are
{ __fc_random48_counter; __fc_p_random48_counter }
{ z1->s; z2->s; tab_y[0..] } { z1->c; a } { z2->c; b }
[alias] May-alias graph after instruction z2->c = b; is
0:{ tab_y } → 18:{ } 7:{ z1 } → 8:{ } 8:{ } -s→ 18:{ }
8:{ } -c→ 19:{ a } 9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ }
10:{ } -c→ 20:{ b } 11:{ t } → 12:{ } 18:{ } → 2:{ x1; x2 }
19:{ a } → 14:{ } 20:{ b } → 16:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 11:{ z1 } → 12:{ } 12:{ } -s→ 22:{ }
12:{ } -c→ 23:{ a } 13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ }
14:{ } -c→ 24:{ b } 15:{ t } → 16:{ } 22:{ } → 6:{ x1; x2 }
23:{ a } → 18:{ } 24:{ b } → 20:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z1;
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are
{ __fc_random48_counter; __fc_p_random48_counter }
{ (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; a } { z2->c; b }
[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z1; is
0:{ tab_y } → 18:{ } 8:{ } -s→ 18:{ } 8:{ } -c→ 19:{ a }
9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ } 10:{ } -c→ 20:{ b }
11:{ t } → 12:{ } 12:{ } -t→ 21:{ z1 } 18:{ } → 2:{ x1; x2 }
19:{ a } → 14:{ } 20:{ b } → 16:{ } 21:{ z1 } → 8:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 12:{ } -s→ 22:{ } 12:{ } -c→ 23:{ a }
13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ } 14:{ } -c→ 24:{ b }
15:{ t } → 16:{ } 16:{ } -t→ 25:{ z1 } 22:{ } → 6:{ x1; x2 }
23:{ a } → 18:{ } 24:{ b } → 20:{ } 25:{ z1 } → 12:{ }
[alias] analysing instruction: t->d = a;
[alias] May-aliases after instruction t->d = a; are
{ __fc_random48_counter; __fc_p_random48_counter }
{ (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { z2->c; b }
[alias] May-alias graph after instruction t->d = a; is
0:{ tab_y } → 18:{ } 8:{ } -s→ 18:{ } 8:{ } -c→ 22:{ a }
9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ } 10:{ } -c→ 20:{ b }
11:{ t } → 12:{ } 12:{ } -t→ 21:{ z1 } 12:{ } -d→ 22:{ a }
18:{ } → 2:{ x1; x2 } 20:{ b } → 16:{ } 21:{ z1 } → 8:{ }
22:{ a } → 14:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 12:{ } -s→ 22:{ } 12:{ } -c→ 26:{ a }
13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ } 14:{ } -c→ 24:{ b }
15:{ t } → 16:{ } 16:{ } -t→ 25:{ z1 } 16:{ } -d→ 26:{ a }
22:{ } → 6:{ x1; x2 } 24:{ b } → 20:{ } 25:{ z1 } → 12:{ }
26:{ a } → 18:{ }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
{ (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { z2->c; b }
[alias] May-alias graph after instruction __retres = 0; is
0:{ tab_y } → 18:{ } 8:{ } -s→ 18:{ } 8:{ } -c→ 22:{ a }
9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ } 10:{ } -c→ 20:{ b }
11:{ t } → 12:{ } 12:{ } -t→ 21:{ z1 } 12:{ } -d→ 22:{ a }
18:{ } → 2:{ x1; x2 } 20:{ b } → 16:{ } 21:{ z1 } → 8:{ }
22:{ a } → 14:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 12:{ } -s→ 22:{ } 12:{ } -c→ 26:{ a }
13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ } 14:{ } -c→ 24:{ b }
15:{ t } → 16:{ } 16:{ } -t→ 25:{ z1 } 16:{ } -d→ 26:{ a }
22:{ } → 6:{ x1; x2 } 24:{ b } → 20:{ } 25:{ z1 } → 12:{ }
26:{ a } → 18:{ }
[alias] May-aliases at the end of function main:
{ __fc_random48_counter; __fc_p_random48_counter }
{ (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { z2->c; b }
[alias] May-alias graph at the end of function main:
0:{ tab_y } → 18:{ } 8:{ } -s→ 18:{ } 8:{ } -c→ 22:{ a }
9:{ z2 } → 10:{ } 10:{ } -s→ 18:{ } 10:{ } -c→ 20:{ b }
11:{ t } → 12:{ } 12:{ } -t→ 21:{ z1 } 12:{ } -d→ 22:{ a }
18:{ } → 2:{ x1; x2 } 20:{ b } → 16:{ } 21:{ z1 } → 8:{ }
22:{ a } → 14:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ tab_y } → 22:{ } 12:{ } -s→ 22:{ } 12:{ } -c→ 26:{ a }
13:{ z2 } → 14:{ } 14:{ } -s→ 22:{ } 14:{ } -c→ 24:{ b }
15:{ t } → 16:{ } 16:{ } -t→ 25:{ z1 } 16:{ } -d→ 26:{ a }
22:{ } → 6:{ x1; x2 } 24:{ b } → 20:{ } 25:{ z1 } → 12:{ }
26:{ a } → 18:{ }
[alias] Summary of function main:
formals: returns: __retres
state: { (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
state: { __fc_random48_counter; __fc_p_random48_counter }
{ (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { z2->c; b }
[alias] Analysis complete
src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+ 72
− 40
View file @ 38d3796d
[kernel] Parsing nested2.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x2 = {.a = 2, .b = 3}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x2 = {.a = 2, .b = 3}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_2_t *z1 = malloc(sizeof(st_2_t));
is 0:{ z1 } → 1:{ }
is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_3_t *t = malloc(sizeof(st_3_t)); is
0:{ z1 } → 1:{ } 2:{ t } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ } 6:{ t } → 7:{ }
[alias] analysing instruction: int *a = malloc(sizeof(int));
[alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none>
[alias] May-aliases after instruction int *a = malloc(sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is
0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ } 6:{ t } → 7:{ } 8:{ a } → 9:{ }
[alias] analysing instruction: *a = 0;
[alias] May-aliases after instruction *a = 0; are <none>
[alias] May-aliases after instruction *a = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction *a = 0; is
0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ } 6:{ t } → 7:{ } 8:{ a } → 9:{ }
[alias] analysing instruction: z1->s[0] = (struct struct_1_t *)(& x1);
[alias] May-aliases after instruction z1->s[0] = (struct struct_1_t *)(& x1); are
<none>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction z1->s[0] = (struct struct_1_t *)(& x1);
is
0:{ z1 } → 1:{ } 1:{ } -s→ 6:{ } 2:{ t } → 3:{ }
4:{ a } → 5:{ } 6:{ } → 7:{ } 7:{ } → 8:{ x1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ } 5:{ } -s→ 10:{ } 6:{ t } → 7:{ }
8:{ a } → 9:{ } 10:{ } → 11:{ } 11:{ } → 12:{ x1 }
[alias] analysing instruction: z1->s[1] = (struct struct_1_t *)(& x2);
[alias] May-aliases after instruction z1->s[1] = (struct struct_1_t *)(& x2); are
<none>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction z1->s[1] = (struct struct_1_t *)(& x2);
is
0:{ z1 } → 1:{ } 1:{ } -s→ 6:{ } 2:{ t } → 3:{ }
4:{ a } → 5:{ } 6:{ } → 7:{ } 7:{ } → 8:{ x1; x2 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ } 5:{ } -s→ 10:{ } 6:{ t } → 7:{ }
8:{ a } → 9:{ } 10:{ } → 11:{ } 11:{ } → 12:{ x1; x2 }
[alias] analysing instruction: z1->c = a;
[alias] May-aliases after instruction z1->c = a; are { z1->c; a }
[alias] May-aliases after instruction z1->c = a; are
{ __fc_random48_counter; __fc_p_random48_counter } { z1->c; a }
[alias] May-alias graph after instruction z1->c = a; is
0:{ z1 } → 1:{ } 1:{ } -s→ 6:{ } 1:{ } -c→ 12:{ a }
2:{ t } → 3:{ } 6:{ } → 7:{ } 7:{ } → 8:{ x1; x2 }
12:{ a } → 5:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ z1 } → 5:{ } 5:{ } -s→ 10:{ } 5:{ } -c→ 16:{ a }
6:{ t } → 7:{ } 10:{ } → 11:{ } 11:{ } → 12:{ x1; x2 }
16:{ a } → 9:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z1;
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are
{ t->t; z1 } { (t->t)->c; z1->c; a } { (t->t)->s; z1->s }
{ (t->t)->s[0..]; z1->s[0..] }
{ __fc_random48_counter; __fc_p_random48_counter } { t->t; z1 }
{ (t->t)->c; z1->c; a } { (t->t)->s; z1->s } { (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z1; is
1:{ } -s→ 6:{ } 1:{ } -c→ 12:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 6:{ } → 7:{ } 7:{ } → 8:{ x1; x2 }
12:{ a } → 5:{ } 13:{ z1 } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
5:{ } -s→ 10:{ } 5:{ } -c→ 16:{ a } 6:{ t } → 7:{ }
7:{ } -t→ 17:{ z1 } 10:{ } → 11:{ } 11:{ } → 12:{ x1; x2 }
16:{ a } → 9:{ } 17:{ z1 } → 5:{ }
[alias] analysing instruction: t->d = a;
[alias] May-aliases after instruction t->d = a; are
{ t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ __fc_random48_counter; __fc_p_random48_counter } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph after instruction t->d = a; is
1:{ } -s→ 6:{ } 1:{ } -c→ 14:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 3:{ } -d→ 14:{ a } 6:{ } → 7:{ }
7:{ } → 8:{ x1; x2 } 13:{ z1 } → 1:{ } 14:{ a } → 5:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
5:{ } -s→ 10:{ } 5:{ } -c→ 18:{ a } 6:{ t } → 7:{ }
7:{ } -t→ 17:{ z1 } 7:{ } -d→ 18:{ a } 10:{ } → 11:{ }
11:{ } → 12:{ x1; x2 } 17:{ z1 } → 5:{ } 18:{ a } → 9:{ }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are
{ t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ __fc_random48_counter; __fc_p_random48_counter } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph after instruction __retres = 0; is
1:{ } -s→ 6:{ } 1:{ } -c→ 14:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 3:{ } -d→ 14:{ a } 6:{ } → 7:{ }
7:{ } → 8:{ x1; x2 } 13:{ z1 } → 1:{ } 14:{ a } → 5:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
5:{ } -s→ 10:{ } 5:{ } -c→ 18:{ a } 6:{ t } → 7:{ }
7:{ } -t→ 17:{ z1 } 7:{ } -d→ 18:{ a } 10:{ } → 11:{ }
11:{ } → 12:{ x1; x2 } 17:{ z1 } → 5:{ } 18:{ a } → 9:{ }
[alias] May-aliases at the end of function main:
{ t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ __fc_random48_counter; __fc_p_random48_counter } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ (t->t)->s[0..]; z1->s[0..] }
[alias] May-alias graph at the end of function main:
1:{ } -s→ 6:{ } 1:{ } -c→ 14:{ a } 2:{ t } → 3:{ }
3:{ } -t→ 13:{ z1 } 3:{ } -d→ 14:{ a } 6:{ } → 7:{ }
7:{ } → 8:{ x1; x2 } 13:{ z1 } → 1:{ } 14:{ a } → 5:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
5:{ } -s→ 10:{ } 5:{ } -c→ 18:{ a } 6:{ t } → 7:{ }
7:{ } -t→ 17:{ z1 } 7:{ } -d→ 18:{ a } 10:{ } → 11:{ }
11:{ } → 12:{ x1; x2 } 17:{ z1 } → 5:{ } 18:{ a } → 9:{ }
[alias] Summary of function main:
formals: returns: __retres
state: { t->t; z1 } { (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
state: { __fc_random48_counter; __fc_p_random48_counter } { t->t; z1 }
{ (t->t)->c; z1->c; t->d; a } { (t->t)->s; z1->s }
{ (t->t)->s[0..]; z1->s[0..] }
[alias] Analysis complete
src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
+ 45
− 19
View file @ 38d3796d
[kernel] Parsing structure4.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t *y1 = malloc(sizeof(st_1_t));
is 0:{ y1 } → 1:{ }
is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_2_t *z = malloc(sizeof(st_2_t)); is
0:{ y1 } → 1:{ } 2:{ z } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ } 6:{ z } → 7:{ }
[alias] analysing instruction: y1 = & x1;
[alias] May-aliases after instruction y1 = & x1; are <none>
[alias] May-aliases after instruction y1 = & x1; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction y1 = & x1; is
0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ x1 } 6:{ z } → 7:{ }
[alias] analysing instruction: z->s = (struct struct_1_t *)y1;
[alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are
{ z->s; y1 }
{ __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 }
[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is
2:{ z } → 3:{ } 3:{ } -s→ 6:{ y1 } 6:{ y1 } → 1:{ x1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ z } → 7:{ } 7:{ } -s→ 10:{ y1 } 10:{ y1 } → 5:{ x1 }
[alias] analysing instruction: z->c = 6;
[alias] May-aliases after instruction z->c = 6; are { z->s; y1 }
[alias] May-aliases after instruction z->c = 6; are
{ __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 }
[alias] May-alias graph after instruction z->c = 6; is
2:{ z } → 3:{ } 3:{ } -s→ 6:{ y1 } 6:{ y1 } → 1:{ x1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ z } → 7:{ } 7:{ } -s→ 10:{ y1 } 10:{ y1 } → 5:{ x1 }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are { z->s; y1 }
[alias] May-aliases after instruction __retres = 0; are
{ __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 }
[alias] May-alias graph after instruction __retres = 0; is
2:{ z } → 3:{ } 3:{ } -s→ 6:{ y1 } 6:{ y1 } → 1:{ x1 }
[alias] May-aliases at the end of function main: { z->s; y1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ z } → 7:{ } 7:{ } -s→ 10:{ y1 } 10:{ y1 } → 5:{ x1 }
[alias] May-aliases at the end of function main:
{ __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 }
[alias] May-alias graph at the end of function main:
2:{ z } → 3:{ } 3:{ } -s→ 6:{ y1 } 6:{ y1 } → 1:{ x1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ z } → 7:{ } 7:{ } -s→ 10:{ y1 } 10:{ y1 } → 5:{ x1 }
[alias] Summary of function main:
formals: returns: __retres state: { z->s; y1 }
formals: returns: __retres
state: { __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 }
[alias] Analysis complete
src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
+ 77
− 42
View file @ 38d3796d
[kernel] Parsing structure5.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x1 = {.a = 0, .b = 1}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x1 = {.a = 0, .b = 1}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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-aliases after instruction st_1_t x2 = {.a = 1, .b = 2}; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t x2 = {.a = 1, .b = 2}; is
<empty>
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_1_t *y1 = malloc(sizeof(st_1_t));
is 0:{ y1 } → 1:{ }
is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction st_2_t *z = malloc(sizeof(st_2_t)); is
0:{ y1 } → 1:{ } 2:{ z } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ } 6:{ z } → 7:{ }
[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>
{ __fc_random48_counter; __fc_p_random48_counter }
[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:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ } 6:{ z } → 7:{ } 8:{ t } → 9:{ }
[alias] analysing instruction: int *a = malloc(sizeof(int));
[alias] May-aliases after instruction int *a = malloc(sizeof(int)); are <none>
[alias] May-aliases after instruction int *a = malloc(sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is
0:{ y1 } → 1:{ } 2:{ z } → 3:{ } 4:{ t } → 5:{ }
6:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ } 6:{ z } → 7:{ } 8:{ t } → 9:{ }
10:{ a } → 11:{ }
[alias] analysing instruction: *a = 0;
[alias] May-aliases after instruction *a = 0; are <none>
[alias] May-aliases after instruction *a = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction *a = 0; is
0:{ y1 } → 1:{ } 2:{ z } → 3:{ } 4:{ t } → 5:{ }
6:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ } 6:{ z } → 7:{ } 8:{ t } → 9:{ }
10:{ a } → 11:{ }
[alias] analysing instruction: y1 = & x1;
[alias] May-aliases after instruction y1 = & x1; are <none>
[alias] May-aliases after instruction y1 = & x1; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction y1 = & x1; is
0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ } 4:{ t } → 5:{ }
6:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ y1 } → 5:{ x1 } 6:{ z } → 7:{ } 8:{ t } → 9:{ }
10:{ a } → 11:{ }
[alias] analysing instruction: z->s = (struct struct_1_t *)y1;
[alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are
{ z->s; y1 }
{ __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 }
[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is
2:{ z } → 3:{ } 3:{ } -s→ 10:{ y1 } 4:{ t } → 5:{ }
6:{ a } → 7:{ } 10:{ y1 } → 1:{ x1 }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ z } → 7:{ } 7:{ } -s→ 14:{ y1 } 8:{ t } → 9:{ }
10:{ a } → 11:{ } 14:{ y1 } → 5:{ x1 }
[alias] analysing instruction: z->c = a;
[alias] May-aliases after instruction z->c = a; are { z->s; y1 } { z->c; a }
[alias] May-aliases after instruction z->c = a; are
{ __fc_random48_counter; __fc_p_random48_counter } { z->s; y1 } { z->c; a }
[alias] May-alias graph after instruction z->c = a; is
2:{ z } → 3:{ } 3:{ } -s→ 10:{ y1 } 3:{ } -c→ 11:{ a }
4:{ t } → 5:{ } 10:{ y1 } → 1:{ x1 } 11:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
6:{ z } → 7:{ } 7:{ } -s→ 14:{ y1 } 7:{ } -c→ 15:{ a }
8:{ t } → 9:{ } 14:{ y1 } → 5:{ x1 } 15:{ a } → 11:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z;
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z; are
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; a }
{ __fc_random48_counter; __fc_p_random48_counter } { (t->t)->s; z->s; y1 }
{ t->t; z } { (t->t)->c; z->c; a }
[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z; is
3:{ } -s→ 10:{ y1 } 3:{ } -c→ 11:{ a } 4:{ t } → 5:{ }
5:{ } -t→ 12:{ z } 10:{ y1 } → 1:{ x1 } 11:{ a } → 7:{ }
12:{ z } → 3:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
7:{ } -s→ 14:{ y1 } 7:{ } -c→ 15:{ a } 8:{ t } → 9:{ }
9:{ } -t→ 16:{ z } 14:{ y1 } → 5:{ x1 } 15:{ a } → 11:{ }
16:{ z } → 7:{ }
[alias] analysing instruction: t->d = a;
[alias] May-aliases after instruction t->d = a; are
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; t->d; a }
{ __fc_random48_counter; __fc_p_random48_counter } { (t->t)->s; z->s; y1 }
{ t->t; z } { (t->t)->c; z->c; t->d; a }
[alias] May-alias graph after instruction t->d = a; is
3:{ } -s→ 10:{ y1 } 3:{ } -c→ 13:{ a } 4:{ t } → 5:{ }
5:{ } -t→ 12:{ z } 5:{ } -d→ 13:{ a } 10:{ y1 } → 1:{ x1 }
12:{ z } → 3:{ } 13:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
7:{ } -s→ 14:{ y1 } 7:{ } -c→ 17:{ a } 8:{ t } → 9:{ }
9:{ } -t→ 16:{ z } 9:{ } -d→ 17:{ a } 14:{ y1 } → 5:{ x1 }
16:{ z } → 7:{ } 17:{ a } → 11:{ }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; t->d; a }
{ __fc_random48_counter; __fc_p_random48_counter } { (t->t)->s; z->s; y1 }
{ t->t; z } { (t->t)->c; z->c; t->d; a }
[alias] May-alias graph after instruction __retres = 0; is
3:{ } -s→ 10:{ y1 } 3:{ } -c→ 13:{ a } 4:{ t } → 5:{ }
5:{ } -t→ 12:{ z } 5:{ } -d→ 13:{ a } 10:{ y1 } → 1:{ x1 }
12:{ z } → 3:{ } 13:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
7:{ } -s→ 14:{ y1 } 7:{ } -c→ 17:{ a } 8:{ t } → 9:{ }
9:{ } -t→ 16:{ z } 9:{ } -d→ 17:{ a } 14:{ y1 } → 5:{ x1 }
16:{ z } → 7:{ } 17:{ a } → 11:{ }
[alias] May-aliases at the end of function main:
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; t->d; a }
{ __fc_random48_counter; __fc_p_random48_counter } { (t->t)->s; z->s; y1 }
{ t->t; z } { (t->t)->c; z->c; t->d; a }
[alias] May-alias graph at the end of function main:
3:{ } -s→ 10:{ y1 } 3:{ } -c→ 13:{ a } 4:{ t } → 5:{ }
5:{ } -t→ 12:{ z } 5:{ } -d→ 13:{ a } 10:{ y1 } → 1:{ x1 }
12:{ z } → 3:{ } 13:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
7:{ } -s→ 14:{ y1 } 7:{ } -c→ 17:{ a } 8:{ t } → 9:{ }
9:{ } -t→ 16:{ z } 9:{ } -d→ 17:{ a } 14:{ y1 } → 5:{ x1 }
16:{ z } → 7:{ } 17:{ a } → 11:{ }
[alias] Summary of function main:
formals: returns: __retres
state: { (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; t->d; a }
state: { __fc_random48_counter; __fc_p_random48_counter }
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; t->d; a }
[alias] Analysis complete
src/plugins/alias/tests/real_world/oracle/function1_v2.res.oracle
+ 57
− 22
View file @ 38d3796d
[kernel] Parsing function1_v2.c (with preprocessing)
[alias] analysing global variable definiton: __fc_rand_max =
(unsigned long)2147483647;
[alias] May-aliases after global variable definition __fc_rand_max are <none>
[alias] May-alias graph after global variable definition __fc_rand_max is
<empty>
[alias] analysing global variable definiton: __fc_p_random48_counter =
__fc_random48_counter;
[alias] May-aliases after global variable definition __fc_p_random48_counter are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after global variable definition __fc_p_random48_counter
is 0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
[alias] analysing function: alias
[alias] analysing instruction: *x = *y;
[alias] May-aliases after instruction *x = *y; are { x; y } { *x; *y }
[alias] May-aliases after instruction *x = *y; are
{ __fc_random48_counter; __fc_p_random48_counter } { x; y } { *x; *y }
[alias] May-alias graph after instruction *x = *y; is
0:{ x } → 1:{ } 1:{ } → 2:{ } 3:{ y } → 1:{ }
[alias] May-aliases at the end of function alias: { x; y } { *x; *y }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ x } → 5:{ } 5:{ } → 6:{ } 7:{ y } → 5:{ }
[alias] May-aliases at the end of function alias:
{ __fc_random48_counter; __fc_p_random48_counter } { x; y } { *x; *y }
[alias] May-alias graph at the end of function alias:
0:{ x } → 1:{ } 1:{ } → 2:{ } 3:{ y } → 1:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
4:{ x } → 5:{ } 5:{ } → 6:{ } 7:{ y } → 5:{ }
[alias] Summary of function alias:
formals: x y returns: <none> state: { x; y } { *x; *y }
formals: x y returns: <none>
state: { __fc_random48_counter; __fc_p_random48_counter } { x; y }
{ *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-aliases after instruction int *a = malloc(sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *a = malloc(sizeof(int)); is
6:{ a } → 7:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a } → 11:{ }
[alias] analysing instruction: *a = 0;
[alias] May-aliases after instruction *a = 0; are <none>
[alias] May-alias graph after instruction *a = 0; is 6:{ a } → 7:{ }
[alias] May-aliases after instruction *a = 0; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction *a = 0; is
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a } → 11:{ }
[alias] analysing instruction: int *b = malloc(sizeof(int));
[alias] May-aliases after instruction int *b = malloc(sizeof(int)); are <none>
[alias] May-aliases after instruction int *b = malloc(sizeof(int)); are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction int *b = malloc(sizeof(int)); is
6:{ a } → 7:{ } 8:{ b } → 9:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a } → 11:{ } 12:{ b } → 13:{ }
[alias] analysing instruction: *b = 42;
[alias] May-aliases after instruction *b = 42; are <none>
[alias] May-aliases after instruction *b = 42; are
{ __fc_random48_counter; __fc_p_random48_counter }
[alias] May-alias graph after instruction *b = 42; is
6:{ a } → 7:{ } 8:{ b } → 9:{ }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a } → 11:{ } 12:{ b } → 13:{ }
[alias] analysing instruction: alias(& a,& b);
[alias] May-aliases after instruction alias(& a,& b); are { a; b }
[alias] May-aliases after instruction alias(& a,& b); are
{ __fc_random48_counter; __fc_p_random48_counter } { a; b }
[alias] May-alias graph after instruction alias(& a,& b); is
6:{ a; b } → 7:{ } 14:{ } → 6:{ a; b } 15:{ } → 6:{ a; b }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a; b } → 11:{ } 22:{ } → 10:{ a; b } 23:{ } → 10:{ a; b }
[alias] analysing instruction: *a = 7;
[alias] May-aliases after instruction *a = 7; are { a; b }
[alias] May-aliases after instruction *a = 7; are
{ __fc_random48_counter; __fc_p_random48_counter } { a; b }
[alias] May-alias graph after instruction *a = 7; is
6:{ a; b } → 7:{ } 14:{ } → 6:{ a; b } 15:{ } → 6:{ a; b }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a; b } → 11:{ } 22:{ } → 10:{ a; b } 23:{ } → 10:{ a; b }
[alias] analysing instruction: __retres = 0;
[alias] May-aliases after instruction __retres = 0; are { a; b }
[alias] May-aliases after instruction __retres = 0; are
{ __fc_random48_counter; __fc_p_random48_counter } { a; b }
[alias] May-alias graph after instruction __retres = 0; is
6:{ a; b } → 7:{ } 14:{ } → 6:{ a; b } 15:{ } → 6:{ a; b }
[alias] May-aliases at the end of function main: { a; b }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a; b } → 11:{ } 22:{ } → 10:{ a; b } 23:{ } → 10:{ a; b }
[alias] May-aliases at the end of function main:
{ __fc_random48_counter; __fc_p_random48_counter } { a; b }
[alias] May-alias graph at the end of function main:
6:{ a; b } → 7:{ } 14:{ } → 6:{ a; b } 15:{ } → 6:{ a; b }
0:{ __fc_random48_counter; __fc_p_random48_counter } → 1:{ }
10:{ a; b } → 11:{ } 22:{ } → 10:{ a; b } 23:{ } → 10:{ a; b }
[alias] Summary of function main:
formals: returns: __retres state: { a; b }
formals: returns: __retres
state: { __fc_random48_counter; __fc_p_random48_counter } { a; b }
[alias] Analysis complete
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment