DRIVER: TVLA Initialization... Blast 2.0. Copyright 2005 Regents of the University of California at Berkeley This program contains Foci, Copyright 2003 Cadence Berkeley Laboratories, Cadence Design Systems. All rights reserved. Begin Parsing files: list.c Initializing CIL Putting in initializer __BLAST_initialize_list.c Finished Parsing Begin Building CFA Initializing BLAST Encountered function exit Finished converting function exit Encountered function main ********* function call: __BLAST_initialize_list.cQuery : (a@main == 0=>false) Query : (a@main == 0=>false) querying exp: (a@main == 0=>false) convertToSimplifySyntax exp = (a@main == 0=>false) Simplify: (IMPLIES (EQ v1 0) FALSE) list.c:53: Warning: Return statement with a value in function returning void Forking Simplify process... (Adding axioms) (BG_PUSH (FORALL (x y) (EQ (select (addrOf x y) 0) x))) (BG_PUSH (FORALL (x y d1) (IMPLIES (EQ (foffset x d1) (foffset y d1)) (EQ x y)))) (BG_PUSH (FORALL (x y) (NEQ (addrOf x y) 0))) (BG_PUSH (FORALL (x y) (EQ (* (Div x y) y) x )) ) (BG_PUSH (FORALL (x) (NEQ (_STRINGCONSTANT x) 0 ))) done! Simplify : in isValid Simplify says: > > > > > > 1: Invalid. false Query : (a@main != 0=>false) querying exp: (a@main != 0=>false) convertToSimplifySyntax exp = (a@main != 0=>false) Simplify: (IMPLIES (NEQ v1 0) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 2: Invalid. false ********* function call: exitQuery : (t@main == 0=>false) querying exp: (t@main == 0=>false) convertToSimplifySyntax exp = (t@main == 0=>false) Simplify: (IMPLIES (EQ v1 0) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 3: Invalid. false Query : (t@main != 0=>false) querying exp: (t@main != 0=>false) convertToSimplifySyntax exp = (t@main != 0=>false) Simplify: (IMPLIES (NEQ v1 0) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 4: Invalid. false ********* function call: exitQuery : (t@main == 0=>false) querying exp: (t@main == 0=>false) convertToSimplifySyntax exp = (t@main == 0=>false) Simplify: (IMPLIES (EQ v1 0) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 5: Invalid. false Query : (t@main != 0=>false) querying exp: (t@main != 0=>false) convertToSimplifySyntax exp = (t@main != 0=>false) Simplify: (IMPLIES (NEQ v1 0) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 6: Invalid. false ********* function call: exitQuery : (* (p@main ).h == 1=>false) querying exp: (* (p@main ).h == 1=>false) convertToSimplifySyntax exp = (* (p@main ).h == 1=>false) Simplify: (IMPLIES (EQ (select (select v2 0) v1) 1) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 7: Invalid. false Query : (* (p@main ).h != 1=>false) querying exp: (* (p@main ).h != 1=>false) convertToSimplifySyntax exp = (* (p@main ).h != 1=>false) Simplify: (IMPLIES (NEQ (select (select v2 0) v1) 1) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 8: Invalid. false Query : (* (p@main ).h == 2=>false) querying exp: (* (p@main ).h == 2=>false) convertToSimplifySyntax exp = (* (p@main ).h == 2=>false) Simplify: (IMPLIES (EQ (select (select v2 0) v1) 2) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 9: Invalid. false Query : (* (p@main ).h != 2=>false) querying exp: (* (p@main ).h != 2=>false) convertToSimplifySyntax exp = (* (p@main ).h != 2=>false) Simplify: (IMPLIES (NEQ (select (select v2 0) v1) 2) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 10: Invalid. false Query : (* (p@main ).h != 3=>false) querying exp: (* (p@main ).h != 3=>false) convertToSimplifySyntax exp = (* (p@main ).h != 3=>false) Simplify: (IMPLIES (NEQ (select (select v2 0) v1) 3) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 11: Invalid. false Query : (* (p@main ).h == 3=>false) querying exp: (* (p@main ).h == 3=>false) convertToSimplifySyntax exp = (* (p@main ).h == 3=>false) Simplify: (IMPLIES (EQ (select (select v2 0) v1) 3) FALSE) Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 12: Invalid. false Finished converting function main Encountered function __BLAST_initialize_list.c Finished converting function __BLAST_initialize_list.c Start Building Callgraph-ocp Unknown called fun: malloc Unknown called fun: malloc Unknown called fun: malloc Filling SCC info SCC 1: main SCC 2: exit SCC 3: __BLAST_initialize_list.c SCC info filled Post 1 : 2, 3 Post 2 : Post 3 : SCC sinks: 2, 3 Done Building Callgraph-ocp In output_call_paths cr Checking for cycles in the call graph. cr Done checking for cycles in the call graph. Call Graph Paths: 9 Visited functions: 3 Visited existing functions: 3 Defined functions: main exit __BLAST_initialize_list.c Loop head : (0,1) Loop head : (1,36) Loop head : (1,31) Loop head : (1,29) Loop head : (1,12) Loop head : (1,10) Finished Building CFA Printing System Description Functions are: __BLAST_initialize_list.c exit main Function: __BLAST_initialize_list.c Formals: [] Labels: Location: Location: id=2#1 src="list.c"; line=0 Attributes: Outgoing edges: Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial) Ingoing edges: Location: Location: id=2#0 (Artificial) Attributes: Outgoing edges: Ingoing edges: Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial) Function: exit Formals: [s@exit] Labels: _EXIT: Location: id=0#1 src="list.c"; line=12 Location: Location: id=0#1 src="list.c"; line=12 Attributes: Outgoing edges: Location: id=0#1 src="list.c"; line=12---Skip---> Location: id=0#1 src="list.c"; line=12 Ingoing edges: Location: id=0#1 src="list.c"; line=12---Skip---> Location: id=0#1 src="list.c"; line=12 Function: main Formals: [] Labels: ERROR: Location: id=1#36 src="list.c"; line=51 Location: Location: id=1#1 src="list.c"; line=0 Attributes: Outgoing edges: Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) Ingoing edges: Location: Location: id=1#2 (Artificial) Attributes: Outgoing edges: Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24 Ingoing edges: Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) Location: Location: id=1#3 src="list.c"; line=24 Attributes: Outgoing edges: Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))---> Location: id=1#4 src="list.c"; line=24 Ingoing edges: Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24 Location: Location: id=1#4 src="list.c"; line=24 Attributes: Outgoing edges: Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25 Ingoing edges: Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))---> Location: id=1#4 src="list.c"; line=24 Location: Location: id=1#5 src="list.c"; line=25 Attributes: Outgoing edges: Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25 Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27 Ingoing edges: Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25 Location: Location: id=1#6 src="list.c"; line=25 Attributes: Outgoing edges: Location: id=1#6 src="list.c"; line=25---FunctionCall(exit(1))---> Location: id=1#8 (Artificial) Ingoing edges: Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25 Location: Location: id=1#8 (Artificial) Attributes: Outgoing edges: Location: id=1#8 (Artificial)---Skip--->Location: id=1#9 src="list.c"; line=27 Ingoing edges: Location: id=1#6 src="list.c"; line=25---FunctionCall(exit(1))---> Location: id=1#8 (Artificial) Location: Location: id=1#9 src="list.c"; line=27 Attributes: Outgoing edges: Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28 Ingoing edges: Location: id=1#8 (Artificial)---Skip--->Location: id=1#9 src="list.c"; line=27 Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27 Location: Location: id=1#10 src="list.c"; line=28 Attributes: Outgoing edges: Location: id=1#10 src="list.c"; line=28---Pred(true)---> Location: id=1#11 src="list.c"; line=29 Location: id=1#10 src="list.c"; line=28---Pred(true)---> Location: id=1#12 src="list.c"; line=35 Ingoing edges: Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28 Location: id=1#18 src="list.c"; line=32---Block(* (p@main ).n = t@main;p@main = * (p@main ).n;)---> Location: id=1#10 src="list.c"; line=28 Location: Location: id=1#11 src="list.c"; line=29 Attributes: Outgoing edges: Location: id=1#11 src="list.c"; line=29---Block(* (p@main ).h = 1;)---> Location: id=1#13 src="list.c"; line=30 Ingoing edges: Location: id=1#10 src="list.c"; line=28---Pred(true)---> Location: id=1#11 src="list.c"; line=29 Location: Location: id=1#13 src="list.c"; line=30 Attributes: Outgoing edges: Location: id=1#13 src="list.c"; line=30---FunctionCall(t@main = malloc(512))---> Location: id=1#14 src="list.c"; line=31 Ingoing edges: Location: id=1#11 src="list.c"; line=29---Block(* (p@main ).h = 1;)---> Location: id=1#13 src="list.c"; line=30 Location: Location: id=1#14 src="list.c"; line=31 Attributes: Outgoing edges: Location: id=1#14 src="list.c"; line=31---Pred(t@main == 0)---> Location: id=1#15 src="list.c"; line=31 Location: id=1#14 src="list.c"; line=31---Pred(t@main != 0)---> Location: id=1#18 src="list.c"; line=32 Ingoing edges: Location: id=1#13 src="list.c"; line=30---FunctionCall(t@main = malloc(512))---> Location: id=1#14 src="list.c"; line=31 Location: Location: id=1#15 src="list.c"; line=31 Attributes: Outgoing edges: Location: id=1#15 src="list.c"; line=31---FunctionCall(exit(1))---> Location: id=1#17 (Artificial) Ingoing edges: Location: id=1#14 src="list.c"; line=31---Pred(t@main == 0)---> Location: id=1#15 src="list.c"; line=31 Location: Location: id=1#17 (Artificial) Attributes: Outgoing edges: Location: id=1#17 (Artificial)---Skip--->Location: id=1#18 src="list.c"; line=32 Ingoing edges: Location: id=1#15 src="list.c"; line=31---FunctionCall(exit(1))---> Location: id=1#17 (Artificial) Location: Location: id=1#18 src="list.c"; line=32 Attributes: Outgoing edges: Location: id=1#18 src="list.c"; line=32---Block(* (p@main ).n = t@main;p@main = * (p@main ).n;)---> Location: id=1#10 src="list.c"; line=28 Ingoing edges: Location: id=1#17 (Artificial)---Skip--->Location: id=1#18 src="list.c"; line=32 Location: id=1#14 src="list.c"; line=31---Pred(t@main != 0)---> Location: id=1#18 src="list.c"; line=32 Location: Location: id=1#12 src="list.c"; line=35 Attributes: Outgoing edges: Location: id=1#12 src="list.c"; line=35---Pred(true)---> Location: id=1#20 src="list.c"; line=36 Location: id=1#12 src="list.c"; line=35---Pred(true)---> Location: id=1#21 src="list.c"; line=42 Ingoing edges: Location: id=1#10 src="list.c"; line=28---Pred(true)---> Location: id=1#12 src="list.c"; line=35 Location: id=1#27 src="list.c"; line=39---Block(* (p@main ).n = t@main;p@main = * (p@main ).n;)---> Location: id=1#12 src="list.c"; line=35 Location: Location: id=1#20 src="list.c"; line=36 Attributes: Outgoing edges: Location: id=1#20 src="list.c"; line=36---Block(* (p@main ).h = 2;)---> Location: id=1#22 src="list.c"; line=37 Ingoing edges: Location: id=1#12 src="list.c"; line=35---Pred(true)---> Location: id=1#20 src="list.c"; line=36 Location: Location: id=1#22 src="list.c"; line=37 Attributes: Outgoing edges: Location: id=1#22 src="list.c"; line=37---FunctionCall(t@main = malloc(512))---> Location: id=1#23 src="list.c"; line=38 Ingoing edges: Location: id=1#20 src="list.c"; line=36---Block(* (p@main ).h = 2;)---> Location: id=1#22 src="list.c"; line=37 Location: Location: id=1#23 src="list.c"; line=38 Attributes: Outgoing edges: Location: id=1#23 src="list.c"; line=38---Pred(t@main == 0)---> Location: id=1#24 src="list.c"; line=38 Location: id=1#23 src="list.c"; line=38---Pred(t@main != 0)---> Location: id=1#27 src="list.c"; line=39 Ingoing edges: Location: id=1#22 src="list.c"; line=37---FunctionCall(t@main = malloc(512))---> Location: id=1#23 src="list.c"; line=38 Location: Location: id=1#24 src="list.c"; line=38 Attributes: Outgoing edges: Location: id=1#24 src="list.c"; line=38---FunctionCall(exit(1))---> Location: id=1#26 (Artificial) Ingoing edges: Location: id=1#23 src="list.c"; line=38---Pred(t@main == 0)---> Location: id=1#24 src="list.c"; line=38 Location: Location: id=1#26 (Artificial) Attributes: Outgoing edges: Location: id=1#26 (Artificial)---Skip--->Location: id=1#27 src="list.c"; line=39 Ingoing edges: Location: id=1#24 src="list.c"; line=38---FunctionCall(exit(1))---> Location: id=1#26 (Artificial) Location: Location: id=1#27 src="list.c"; line=39 Attributes: Outgoing edges: Location: id=1#27 src="list.c"; line=39---Block(* (p@main ).n = t@main;p@main = * (p@main ).n;)---> Location: id=1#12 src="list.c"; line=35 Ingoing edges: Location: id=1#26 (Artificial)---Skip--->Location: id=1#27 src="list.c"; line=39 Location: id=1#23 src="list.c"; line=38---Pred(t@main != 0)---> Location: id=1#27 src="list.c"; line=39 Location: Location: id=1#21 src="list.c"; line=42 Attributes: Outgoing edges: Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46 Ingoing edges: Location: id=1#12 src="list.c"; line=35---Pred(true)---> Location: id=1#21 src="list.c"; line=42 Location: Location: id=1#29 src="list.c"; line=46 Attributes: Outgoing edges: Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47 Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48 Ingoing edges: Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46 Location: id=1#30 src="list.c"; line=47---Block(p@main = * (p@main ).n;)---> Location: id=1#29 src="list.c"; line=46 Location: Location: id=1#30 src="list.c"; line=47 Attributes: Outgoing edges: Location: id=1#30 src="list.c"; line=47---Block(p@main = * (p@main ).n;)---> Location: id=1#29 src="list.c"; line=46 Ingoing edges: Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47 Location: Location: id=1#31 src="list.c"; line=48 Attributes: Outgoing edges: Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h == 2)---> Location: id=1#33 src="list.c"; line=49 Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50 Ingoing edges: Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48 Location: id=1#33 src="list.c"; line=49---Block(p@main = * (p@main ).n;)---> Location: id=1#31 src="list.c"; line=48 Location: Location: id=1#33 src="list.c"; line=49 Attributes: Outgoing edges: Location: id=1#33 src="list.c"; line=49---Block(p@main = * (p@main ).n;)---> Location: id=1#31 src="list.c"; line=48 Ingoing edges: Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h == 2)---> Location: id=1#33 src="list.c"; line=49 Location: Location: id=1#34 src="list.c"; line=50 Attributes: Outgoing edges: Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51 Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20 Ingoing edges: Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50 Location: Location: id=1#36 src="list.c"; line=51 Attributes: Outgoing edges: Location: id=1#36 src="list.c"; line=51---Skip---> Location: id=1#36 src="list.c"; line=51 Ingoing edges: Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51 Location: id=1#36 src="list.c"; line=51---Skip---> Location: id=1#36 src="list.c"; line=51 Location: Location: id=1#37 src="list.c"; line=20 Attributes: Outgoing edges: Location: id=1#37 src="list.c"; line=20---Block(Return(0);)---> Location: id=1#0 (Artificial) Ingoing edges: Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20 Location: Location: id=1#0 (Artificial) Attributes: Outgoing edges: Ingoing edges: Location: id=1#37 src="list.c"; line=20---Block(Return(0);)---> Location: id=1#0 (Artificial) Global variables are: Lvalues are: Lval (* (p@main)).n Lval a@main Lval __BLAST_initialize_list.c Lval * (p@main) Lval (* (p@main)).h Lval tmp@main Lval p@main Lval malloc Lval __BLAST_NONDET@main Lval exit Lval t@main Attribute table Starting the alias analysis In do_bdd_alias Number of BDD variables = 4 a@main __BLAST_initialize_list.c t@main tmp@main __bddptsto_mem0 p@main __bddptsto_mem1 __bddptsto_mem2 exit main s@exit bdd_pts_to: Starting iteration. In assign_alloc ptarget is t@main In assign_alloc ptarget is t@main In assign_alloc ptarget is tmp@main In assign_alloc ptarget is t@main In assign_alloc ptarget is t@main In assign_alloc ptarget is tmp@main In assign_alloc ptarget is t@main In assign_alloc ptarget is t@main In assign_alloc ptarget is tmp@main In assign_alloc ptarget is t@main In assign_alloc ptarget is t@main In assign_alloc ptarget is tmp@main In assign_alloc ptarget is t@main In assign_alloc ptarget is t@main In assign_alloc ptarget is tmp@main In assign_alloc ptarget is t@main In assign_alloc ptarget is t@main In assign_alloc ptarget is tmp@main Number of edges (flow insensitive) 16.000000 Finished Building Aliases Finished Building Must Aliases Proc. scc--2 Compute scc_mods: 2 : 1 : exit Direct Wr:2:exit COMP MOD iter1 done COMP MOD iter2 done Proc. scc--3 Compute scc_mods: 3 : 1 : __BLAST_initialize_list.c Direct Wr:3:__BLAST_initialize_list.c COMP MOD iter1 done COMP MOD iter2 done Proc. scc--1 Compute scc_mods: 1 : 1 : main Call exit effects Call exit effects Call malloc effects Call exit effects Call malloc effects Call malloc effects Call __BLAST_initialize_list.c effects Direct Wr:1:main get_lval_aliases_iter: tmp@main Alias query for * (p@main) and tmp@main After peeling: * (p@main) and tmp@main The types are different. Hence not aliased. QueryAlias * (p@main) tmp@main (false) Alias query for a@main and tmp@main After peeling: a@main and tmp@main Alias query for t@main and tmp@main After peeling: t@main and tmp@main Alias query for (* (p@main)).h and tmp@main After peeling: (* (p@main)).h and tmp@main The types are different. Hence not aliased. QueryAlias (* (p@main)).h tmp@main (false) Alias query for tmp@main and tmp@main After peeling: tmp@main and tmp@main Alias query for __BLAST_NONDET@main and tmp@main After peeling: __BLAST_NONDET@main and tmp@main Alias query for p@main and tmp@main After peeling: p@main and tmp@main Alias query for (* (p@main)).n and tmp@main After peeling: (* (p@main)).n and tmp@main QueryAlias (* (p@main)).n tmp@main (false) Alias query for __BLAST_initialize_list.c and tmp@main After peeling: __BLAST_initialize_list.c and tmp@main Alias query for exit and tmp@main After peeling: exit and tmp@main Alias query for malloc and tmp@main After peeling: malloc and tmp@main alias set: tmp@main get_lval_aliases_iter: a@main Alias query for * (p@main) and a@main After peeling: * (p@main) and a@main The types are different. Hence not aliased. QueryAlias * (p@main) a@main (false) Alias query for a@main and a@main After peeling: a@main and a@main Alias query for t@main and a@main After peeling: t@main and a@main Alias query for (* (p@main)).h and a@main After peeling: (* (p@main)).h and a@main The types are different. Hence not aliased. QueryAlias (* (p@main)).h a@main (false) Alias query for tmp@main and a@main After peeling: tmp@main and a@main Alias query for __BLAST_NONDET@main and a@main After peeling: __BLAST_NONDET@main and a@main Alias query for p@main and a@main After peeling: p@main and a@main Alias query for (* (p@main)).n and a@main After peeling: (* (p@main)).n and a@main QueryAlias (* (p@main)).n a@main (false) Alias query for __BLAST_initialize_list.c and a@main After peeling: __BLAST_initialize_list.c and a@main Alias query for exit and a@main After peeling: exit and a@main Alias query for malloc and a@main After peeling: malloc and a@main alias set: a@main get_lval_aliases_iter: p@main Alias query for * (p@main) and p@main After peeling: * (p@main) and p@main The types are different. Hence not aliased. QueryAlias * (p@main) p@main (false) Alias query for a@main and p@main After peeling: a@main and p@main Alias query for t@main and p@main After peeling: t@main and p@main Alias query for (* (p@main)).h and p@main After peeling: (* (p@main)).h and p@main The types are different. Hence not aliased. QueryAlias (* (p@main)).h p@main (false) Alias query for tmp@main and p@main After peeling: tmp@main and p@main Alias query for __BLAST_NONDET@main and p@main After peeling: __BLAST_NONDET@main and p@main Alias query for p@main and p@main After peeling: p@main and p@main Alias query for (* (p@main)).n and p@main After peeling: (* (p@main)).n and p@main QueryAlias (* (p@main)).n p@main (false) Alias query for __BLAST_initialize_list.c and p@main After peeling: __BLAST_initialize_list.c and p@main Alias query for exit and p@main After peeling: exit and p@main Alias query for malloc and p@main After peeling: malloc and p@main alias set: p@main get_lval_aliases_iter: (* (p@main)).h Alias query for * (p@main) and (* (p@main)).h After peeling: * (p@main) and (* (p@main)).h The types are different. Hence not aliased. QueryAlias * (p@main) (* (p@main)).h (false) Alias query for a@main and (* (p@main)).h After peeling: a@main and (* (p@main)).h The types are different. Hence not aliased. QueryAlias a@main (* (p@main)).h (false) Alias query for t@main and (* (p@main)).h After peeling: t@main and (* (p@main)).h The types are different. Hence not aliased. QueryAlias t@main (* (p@main)).h (false) Alias query for (* (p@main)).h and (* (p@main)).h After peeling: (* (p@main)).h and (* (p@main)).h QueryAlias (* (p@main)).h (* (p@main)).h (false) Alias query for tmp@main and (* (p@main)).h After peeling: tmp@main and (* (p@main)).h The types are different. Hence not aliased. QueryAlias tmp@main (* (p@main)).h (false) Alias query for __BLAST_NONDET@main and (* (p@main)).h After peeling: __BLAST_NONDET@main and (* (p@main)).h Warning:Error raised in checkAliasFI!:Not_found for inputs __BLAST_NONDET@main and (* (p@main)).h QueryAlias __BLAST_NONDET@main (* (p@main)).h (false) Alias query for p@main and (* (p@main)).h After peeling: p@main and (* (p@main)).h The types are different. Hence not aliased. QueryAlias p@main (* (p@main)).h (false) Alias query for (* (p@main)).n and (* (p@main)).h After peeling: (* (p@main)).n and (* (p@main)).h The types are different. Hence not aliased. QueryAlias (* (p@main)).n (* (p@main)).h (false) Alias query for __BLAST_initialize_list.c and (* (p@main)).h After peeling: __BLAST_initialize_list.c and (* (p@main)).h The types are different. Hence not aliased. QueryAlias __BLAST_initialize_list.c (* (p@main)).h (false) Alias query for exit and (* (p@main)).h After peeling: exit and (* (p@main)).h The types are different. Hence not aliased. QueryAlias exit (* (p@main)).h (false) Alias query for malloc and (* (p@main)).h After peeling: malloc and (* (p@main)).h The types are different. Hence not aliased. QueryAlias malloc (* (p@main)).h (false) alias set: (* (p@main)).h get_lval_aliases_iter: p@main get_lval_aliases_iter: p@main get_lval_aliases_iter: p@main get_lval_aliases_iter: (* (p@main)).h get_lval_aliases_iter: t@main Alias query for * (p@main) and t@main After peeling: * (p@main) and t@main The types are different. Hence not aliased. QueryAlias * (p@main) t@main (false) Alias query for a@main and t@main After peeling: a@main and t@main Alias query for t@main and t@main After peeling: t@main and t@main Alias query for (* (p@main)).h and t@main After peeling: (* (p@main)).h and t@main The types are different. Hence not aliased. QueryAlias (* (p@main)).h t@main (false) Alias query for tmp@main and t@main After peeling: tmp@main and t@main Alias query for __BLAST_NONDET@main and t@main After peeling: __BLAST_NONDET@main and t@main Alias query for p@main and t@main After peeling: p@main and t@main Alias query for (* (p@main)).n and t@main After peeling: (* (p@main)).n and t@main QueryAlias (* (p@main)).n t@main (false) Alias query for __BLAST_initialize_list.c and t@main After peeling: __BLAST_initialize_list.c and t@main Alias query for exit and t@main After peeling: exit and t@main Alias query for malloc and t@main After peeling: malloc and t@main alias set: t@main get_lval_aliases_iter: (* (p@main)).n Alias query for * (p@main) and (* (p@main)).n After peeling: * (p@main) and (* (p@main)).n The types are different. Hence not aliased. QueryAlias * (p@main) (* (p@main)).n (false) Alias query for a@main and (* (p@main)).n After peeling: a@main and (* (p@main)).n QueryAlias a@main (* (p@main)).n (false) Alias query for t@main and (* (p@main)).n After peeling: t@main and (* (p@main)).n QueryAlias t@main (* (p@main)).n (false) Alias query for (* (p@main)).h and (* (p@main)).n After peeling: (* (p@main)).h and (* (p@main)).n The types are different. Hence not aliased. QueryAlias (* (p@main)).h (* (p@main)).n (false) Alias query for tmp@main and (* (p@main)).n After peeling: tmp@main and (* (p@main)).n QueryAlias tmp@main (* (p@main)).n (false) Alias query for __BLAST_NONDET@main and (* (p@main)).n After peeling: __BLAST_NONDET@main and (* (p@main)).n The types are different. Hence not aliased. QueryAlias __BLAST_NONDET@main (* (p@main)).n (false) Alias query for p@main and (* (p@main)).n After peeling: p@main and (* (p@main)).n QueryAlias p@main (* (p@main)).n (false) Alias query for (* (p@main)).n and (* (p@main)).n After peeling: (* (p@main)).n and (* (p@main)).n QueryAlias (* (p@main)).n (* (p@main)).n (false) Alias query for __BLAST_initialize_list.c and (* (p@main)).n After peeling: __BLAST_initialize_list.c and (* (p@main)).n The types are different. Hence not aliased. QueryAlias __BLAST_initialize_list.c (* (p@main)).n (false) Alias query for exit and (* (p@main)).n After peeling: exit and (* (p@main)).n The types are different. Hence not aliased. QueryAlias exit (* (p@main)).n (false) Alias query for malloc and (* (p@main)).n After peeling: malloc and (* (p@main)).n The types are different. Hence not aliased. QueryAlias malloc (* (p@main)).n (false) alias set: (* (p@main)).n get_lval_aliases_iter: p@main get_lval_aliases_iter: (* (p@main)).h get_lval_aliases_iter: t@main get_lval_aliases_iter: (* (p@main)).n get_lval_aliases_iter: p@main COMP MOD iter1 done COMP MOD iter2 done Done computing mods Write mods to : list.mods.gl Done writing to :list.mods.gl Write mods to : list.mods.fl Done writing to :list.mods.fl Write mods to : list.mods.mmb Done writing to :list.mods.mmb Write mods to : list.mods.ceef Done writing to :list.mods.ceef Done writing mods In add_symbolic_hooks [add_symbolic_hooks] Processing function: __BLAST_initialize_list.c [add_symbolic_hooks] Processing function: exit Done post-alias-analysis back from post_alias_analysis Unknown called fun: malloc Unknown called fun: malloc Unknown called fun: malloc Start Building Callgraph-ocp Done Building Callgraph-ocp In output_call_paths cr Checking for cycles in the call graph. cr Done checking for cycles in the call graph. Call Graph Paths: 9 Visited functions: 3 Visited existing functions: 3 Defined functions: main exit __BLAST_initialize_list.c Unknown fun : DRIVER: TVLA Initialization... DRIVER: TVLA Initialization... Initialized Abstraction SA> Initialization! SA: Add predicate sm SA: Add predicate eq SA: Add predicate isnew In Deconstruct_fc :exit(,1) In Deconstruct_fc :exit(,1) SA> Shape-alias pair found: p@main, t@main SA> Shape-alias pair found: p@main, p@main In Deconstruct_fc :malloc(,512) SA> Shape-alias pair found: t@main, Returned(NOT_IMPLEMENTED_FUNCTION) In Deconstruct_fc :malloc(,512) In Deconstruct_fc :exit(,1) In Deconstruct_fc :malloc(,512) In Deconstruct_fc :malloc(,512) SA> Shape-alias pair found: a@main, p@main SA> Shape-alias pair found: a@main, tmp@main In Deconstruct_fc :malloc(,512) SA> Shape-alias pair found: tmp@main, Returned(NOT_IMPLEMENTED_FUNCTION) In Deconstruct_fc :malloc(,512) In Deconstruct_fc :__BLAST_initialize_list.c() SA> Switching SC: old = <>; new = <(default)> SA> Restoring state from SC <(default)> UL> Shape Analysis enabled Done adding seed predicates ********** Now running the model-checker ********** Glob useful preds Glob useful preds Entering parallel_model_check init region: [AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] error region: [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Setting signal for 2000 seconds **************************************************************************** Next iteration of model-check's big while-loop 1 Now processing tree node: Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Was_Covered_To_Reprocess(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#1 src="list.c"; line=0 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Top RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Was_Covered_To_Reprocess(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) Updating the node's marking This node now looks like: Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) cfLMC enters: __BLAST_initialize_list.c In post -- arguments are: [AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In Deconstruct_fc :__BLAST_initialize_list.c() In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Top FunctionCall(__BLAST_initialize_list.c()) location (1,1) absdatapost postloc: (2,2) UL> Running post on command: UL> FunctionCall(__BLAST_initialize_list.c()) SA> Post of SA is called! SA> Post from top... starting from no information... SA> Switching SC: old = <(default)>; new = <(default)> SA> Saving state to SC <(default)> SA> Restoring state from SC <(default)> In Deconstruct_fc :__BLAST_initialize_list.c() UL> Post returning predicates: UL> And [] Writing back post region New entry point for __BLAST_initialize_list.c lift_and_propagate Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 2 Now processing tree node: Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Was_Covered_To_Reprocess(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=2#2 (Artificial) RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> [Location: id=1#1 src="list.c"; line=0]] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Was_Covered_To_Reprocess(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Updating the node's marking This node now looks like: Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:1 Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 3 Now processing tree node: Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0 tos_fname: __BLAST_initialize_list.c, tos_2_fname: main In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] SymHook(__BLAST_initialize_list.c) location (2,2) absdatapost postloc: (2,1) UL> Running post on command: UL> SymHook(__BLAST_initialize_list.c) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=2#1 src="list.c"; line=0 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> [Location: id=1#1 src="list.c"; line=0]] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) It's a new exit point for __BLAST_initialize_list.c ! |entries| = 1 New summary edges to exit node. New summary edge! Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) --> Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) by way of lift_and_propagate In Region.leq -- arguments are: (suppressed-RJ) [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] SA> TVLA: Cover result: YES SA> Cover -> YES A call site matched in lift_and_propagate. Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) Now caller has 1 children.@. Summary edge added Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 4 Now processing tree node: Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Unprocessed)) Summary Post Printing abstract data regions: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] In Deconstruct_fc :__BLAST_initialize_list.c() Target: * (sizeof(<0>)) Trivial post RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#2 (Artificial) RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Processed_Uncovered(time_stamp=4; region=[AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:1 Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 5 Now processing tree node: Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Skip location (1,2) absdatapost postloc: (1,3) UL> Running post on command: UL> Skip SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#3 src="list.c"; line=24 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Processed_Uncovered(time_stamp=5; region=[AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:1 Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 6 Now processing tree node: Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))---> Location: id=1#4 src="list.c"; line=24 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In Deconstruct_fc :tmp@main=malloc(,512) In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] FunctionCall(tmp@main = malloc(512)) location (1,3) absdatapost postloc: (1,4) UL> Running post on command: UL> FunctionCall(tmp@main = malloc(512)) SA> Post of SA is called! In Deconstruct_fc :tmp@main=malloc(,512) SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#4 src="list.c"; line=24 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Processed_Uncovered(time_stamp=6; region=[AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:1 Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 7 Now processing tree node: Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Block(a@main = tmp@main;) location (1,4) absdatapost postloc: (1,5) UL> Running post on command: UL> Block(a@main = tmp@main;) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#5 src="list.c"; line=25 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Processed_Uncovered(time_stamp=7; region=[AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:1 Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Adding the children to the set of pending unprocessed#nodes Remaining nodes:2 Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 8 Now processing tree node: Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)--->Location: id=1#9 src="list.c"; line=27 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(a@main != 0) location (1,5) absdatapost postloc: (1,9) UL> Running post on command: UL> Pred(a@main != 0) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#9 src="list.c"; line=27 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Processed_Uncovered(time_stamp=8; region=[AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:2 Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 9 Now processing tree node: Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)--->Location: id=1#10 src="list.c"; line=28 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Block(p@main = a@main;) location (1,9) absdatapost postloc: (1,10) UL> Running post on command: UL> Block(p@main = a@main;) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#10 src="list.c"; line=28 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Processed_Uncovered(time_stamp=9; region=[AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:2 Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Adding the children to the set of pending unprocessed#nodes Remaining nodes:3 Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 10 Now processing tree node: Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(true) location (1,10) absdatapost postloc: (1,12) UL> Running post on command: UL> Pred(true) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#12 src="list.c"; line=35 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Processed_Uncovered(time_stamp=10; region=[AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:3 Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Adding the children to the set of pending unprocessed#nodes Remaining nodes:4 Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 11 Now processing tree node: Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(true) location (1,12) absdatapost postloc: (1,21) UL> Running post on command: UL> Pred(true) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#21 src="list.c"; line=42 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Processed_Uncovered(time_stamp=11; region=[AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:4 Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 12 Now processing tree node: Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)--->Location: id=1#29 src="list.c"; line=46 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Block(* (p@main ).h = 3;p@main = a@main;) location (1,21) absdatapost postloc: (1,29) UL> Running post on command: UL> Block(* (p@main ).h = 3;p@main = a@main;) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#29 src="list.c"; line=46 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Processed_Uncovered(time_stamp=12; region=[AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:4 Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47, data=Data(id=17; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Adding the children to the set of pending unprocessed#nodes Remaining nodes:5 Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47, data=Data(id=17; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 13 Now processing tree node: Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(* (p@main ).h != 1) location (1,29) absdatapost postloc: (1,31) UL> Running post on command: UL> Pred(* (p@main ).h != 1) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#31 src="list.c"; line=48 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Processed_Uncovered(time_stamp=13; region=[AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:5 Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h == 2)---> Location: id=1#33 src="list.c"; line=49, data=Data(id=19; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47, data=Data(id=17; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Adding the children to the set of pending unprocessed#nodes Remaining nodes:6 Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h == 2)---> Location: id=1#33 src="list.c"; line=49, data=Data(id=19; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47, data=Data(id=17; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 14 Now processing tree node: Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(* (p@main ).h != 2) location (1,31) absdatapost postloc: (1,34) UL> Running post on command: UL> Pred(* (p@main ).h != 2) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#34 src="list.c"; line=50 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Processed_Uncovered(time_stamp=14; region=[AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Adding the children to the set of pending unprocessed#nodes Remaining nodes:6 Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h == 2)---> Location: id=1#33 src="list.c"; line=49, data=Data(id=19; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47, data=Data(id=17; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Adding the children to the set of pending unprocessed#nodes Remaining nodes:7 Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20, data=Data(id=22; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h == 2)---> Location: id=1#33 src="list.c"; line=49, data=Data(id=19; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h == 1)---> Location: id=1#30 src="list.c"; line=47, data=Data(id=17; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#20 src="list.c"; line=36, data=Data(id=14; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#11 src="list.c"; line=29, data=Data(id=12; kind=Node; mark=Unprocessed)) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main == 0)---> Location: id=1#6 src="list.c"; line=25, data=Data(id=9; kind=Node; mark=Unprocessed)) Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 15 Now processing tree node: Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20, data=Data(id=22; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(* (p@main ).h == 3) location (1,34) absdatapost postloc: (1,37) UL> Running post on command: UL> Pred(* (p@main ).h == 3) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#37 src="list.c"; line=20 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#37 src="list.c"; line=20 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: Bottom In Region.is_empty -- argument is: Bottom No error found at this node Let's test whether this node is covered findExactCov found no exact coverer In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#37 src="list.c"; line=20 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] This node is not covered Constructing its successor children... This node looks like: (before updating) Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20, data=Data(id=22; kind=Node; mark=Unprocessed)) Updating the node's marking This node now looks like: Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h == 3)---> Location: id=1#37 src="list.c"; line=20, data=Data(id=22; kind=Node; mark=Processed_Uncovered(time_stamp=15; region=[AtomicRegion: Location: id=1#37 src="list.c"; line=20 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) It's a new exit point for main ! |entries| = 1 New summary edges to exit node. New summary edge! Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) --> Node(edge=Location: id=1#37 src="list.c"; line=20---Block(Return(0);)---> Location: id=1#0 (Artificial), data=Data(id=23; kind=Exit; mark=Processed_Uncovered(time_stamp=16; region=[AtomicRegion: Location: id=1#37 src="list.c"; line=20 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) by way of Summary edge added Updating the currently reached region Here: addCov **************************************************************************** Next iteration of model-check's big while-loop 16 Now processing tree node: Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Unprocessed)) In post -- arguments are: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51 tos_fname: __BLAST_DUMMY_FUNCTION, tos_2_fname: __BLAST_DUMMY_FUNCTION In abstract_data_post GRAF_SAIDI_POST -- arguments are: AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Pred(* (p@main ).h != 3) location (1,34) absdatapost postloc: (1,36) UL> Running post on command: UL> Pred(* (p@main ).h != 3) SA> Post of SA is called! SA> No action has been scheduled for this post! UL> Post returning predicates: UL> And [] Writing back post region RGN> Processed node's region: RGN> [AtomicRegion: RGN> Location: id=1#36 src="list.c"; line=51 RGN> AbstrDatRgn: RGN> Predicates: [...] RGN> Lattice: RGN> Lattice = RGN> shape class of function (default) RGN> %n = {} RGN> %p = { RGN> } RGN> Stack = RGN> RGN> Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] RGN> RGN> Stack: RGN> []] RGN> In Region.cap -- arguments are: [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: Everystack ] Error region at this node: [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.is_empty -- argument is: [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Error found : checking validity. Error at depth13 Error node: 21 Error found at this node Testing whether this error is a real one path_to_root: Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Processed_Was_Covered_To_Reprocess(time_stamp=17; region=[AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Processed_Uncovered(time_stamp=14; region=[AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Processed_Uncovered(time_stamp=13; region=[AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Processed_Uncovered(time_stamp=12; region=[AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Processed_Uncovered(time_stamp=11; region=[AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Processed_Uncovered(time_stamp=10; region=[AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Processed_Uncovered(time_stamp=9; region=[AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Processed_Uncovered(time_stamp=8; region=[AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Processed_Uncovered(time_stamp=7; region=[AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Processed_Uncovered(time_stamp=6; region=[AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Processed_Uncovered(time_stamp=5; region=[AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Processed_Uncovered(time_stamp=4; region=[AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) path_to_root: Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) path_to_root terminates; no matching call site Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Processed_Uncovered(time_stamp=4; region=[AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Processed_Uncovered(time_stamp=5; region=[AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Processed_Uncovered(time_stamp=6; region=[AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Processed_Uncovered(time_stamp=7; region=[AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Processed_Uncovered(time_stamp=8; region=[AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Processed_Uncovered(time_stamp=9; region=[AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Processed_Uncovered(time_stamp=10; region=[AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Processed_Uncovered(time_stamp=11; region=[AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Processed_Uncovered(time_stamp=12; region=[AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Processed_Uncovered(time_stamp=13; region=[AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Processed_Uncovered(time_stamp=14; region=[AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Processed_Was_Covered_To_Reprocess(time_stamp=17; region=[AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Expanding a summary edge Node: Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Node: Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Done expanding. Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Processed_Uncovered(time_stamp=4; region=[AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Processed_Uncovered(time_stamp=5; region=[AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Processed_Uncovered(time_stamp=6; region=[AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Processed_Uncovered(time_stamp=7; region=[AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Processed_Uncovered(time_stamp=8; region=[AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Processed_Uncovered(time_stamp=9; region=[AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Processed_Uncovered(time_stamp=10; region=[AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Processed_Uncovered(time_stamp=11; region=[AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Processed_Uncovered(time_stamp=12; region=[AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Processed_Uncovered(time_stamp=13; region=[AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Processed_Uncovered(time_stamp=14; region=[AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Processed_Was_Covered_To_Reprocess(time_stamp=17; region=[AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) r_path Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Node(edge=SUMMARY Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))), data=Data(id=5; kind=Node; mark=Processed_Uncovered(time_stamp=4; region=[AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Processed_Uncovered(time_stamp=5; region=[AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Processed_Uncovered(time_stamp=6; region=[AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Processed_Uncovered(time_stamp=7; region=[AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Processed_Uncovered(time_stamp=8; region=[AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Processed_Uncovered(time_stamp=9; region=[AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Processed_Uncovered(time_stamp=10; region=[AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Processed_Uncovered(time_stamp=11; region=[AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Processed_Uncovered(time_stamp=12; region=[AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Processed_Uncovered(time_stamp=13; region=[AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Processed_Uncovered(time_stamp=14; region=[AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Processed_Was_Covered_To_Reprocess(time_stamp=17; region=[AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) block_analyze_trace In block_a_t:14 Projected lengths: pre_reg_l 14 post_reg_l 14 op_l 14 BNum: 0 Pre reg: [AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] OP: Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) Post reg: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] BNum: 1 Pre reg: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] OP: Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0 Post reg: [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] BNum: 2 Pre reg: [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] OP: Location: id=2#1 src="list.c"; line=0---Block(Return(0);)--->Location: id=2#0 (Artificial) Post reg: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 3 Pre reg: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24 Post reg: [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 4 Pre reg: [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))---> Location: id=1#4 src="list.c"; line=24 Post reg: [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 5 Pre reg: [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25 Post reg: [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 6 Pre reg: [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)--->Location: id=1#9 src="list.c"; line=27 Post reg: [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 7 Pre reg: [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)--->Location: id=1#10 src="list.c"; line=28 Post reg: [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 8 Pre reg: [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35 Post reg: [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 9 Pre reg: [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42 Post reg: [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 10 Pre reg: [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)--->Location: id=1#29 src="list.c"; line=46 Post reg: [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 11 Pre reg: [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48 Post reg: [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 12 Pre reg: [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50 Post reg: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] BNum: 13 Pre reg: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] OP: Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51 Post reg: [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] block_a_t: building blocks start bs_reset Call __BLAST_initialize_list.c Return In load_lv_table In Deconstruct_fc :__BLAST_initialize_list.c() In Deconstruct_fc :__BLAST_initialize_list.c() Funcall assignment Symvars: Adding to lv_table: Adding Fields In Deconstruct_fc :tmp@main=malloc(,512) In Deconstruct_fc :tmp@main=malloc(,512) Funcall assignment Symvars: Adding to lv_table: Adding Fields Adding to lv_table: tmp@main Adding Fields Adding to lv_table: a@main Adding Fields Adding to lv_table: a@main Adding Fields Adding to lv_table: Adding Fields Adding to lv_table: Adding Fields Adding to lv_table: Adding Fields Adding to lv_table: a@main Adding Fields Adding to lv_table: (* (p@main)).h Adding Fields h Adding stamp field: all? true :h Adding to lv_table: (* (p@main)).h Adding Fields h Adding to lv_table: (* (p@main)).h Adding Fields h cons_folder !posn = 13 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Pred(* (p@main ).h != 3) Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51 plvmap: now normalize plvmap: now normalize bs_assert: <<* ( ), 1>.h, 1> != 3 simplify_assume sstk:0 convertToSimplifySyntax exp = <<* ( ), 1>.h, 1> != 3 Simplify Assuming: (NEQ chlval1 3) Done Assume bs_assert: true simplify_assume sstk:1 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > 13: Invalid. false Contra ? false bs_pop simplify_pnf sstk:2 Simplify Popping done pop_pnf cons_folder !posn = 12 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Pred(* (p@main ).h != 2) Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50 plvmap: now normalize plvmap: now normalize bs_assert: <<* ( ), 1>.h, 1> != 2 simplify_assume sstk:1 convertToSimplifySyntax exp = <<* ( ), 1>.h, 1> != 2 Simplify Assuming: (NEQ chlval1 2) Done Assume bs_assert: true simplify_assume sstk:2 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 14: Invalid. false Contra ? false bs_pop simplify_pnf sstk:3 Simplify Popping done pop_pnf cons_folder !posn = 11 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Pred(* (p@main ).h != 1) Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48 plvmap: now normalize plvmap: now normalize bs_assert: <<* ( ), 1>.h, 1> != 1 simplify_assume sstk:2 convertToSimplifySyntax exp = <<* ( ), 1>.h, 1> != 1 Simplify Assuming: (NEQ chlval1 1) Done Assume bs_assert: true simplify_assume sstk:3 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 15: Invalid. false Contra ? false bs_pop simplify_pnf sstk:4 Simplify Popping done pop_pnf cons_folder !posn = 10 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Block(* (p@main ).h = 3;p@main = a@main;) Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)--->Location: id=1#29 src="list.c"; line=46 Frames: 1, 0 Must aliases of p@main are Alias pushed candidates: p@main Formals : Aliases in scope of p@main : p@main check field : h , true , true check field : n , false , true Exp closure: cld = 3, e = p@main, clos = p@main, * (p@main), (* (p@main)).h Frames: 1, 0 Must aliases of (* (p@main)).h are Alias pushed candidates: (* (p@main)).h Formals : Aliases in scope of (* (p@main)).h : (* (p@main)).h Exp closure: cld = 3, e = (* (p@main)).h, clos = (* (p@main)).h Warning:bad arg to lv_of_expr3 plvmap: now normalize bs_assert: And [<<* ( ), 2_>.h, 3_> == 3, == , <* ( ), 1> == <* ( ), 1>, <<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>] simplify_assume sstk:3 convertToSimplifySyntax exp = And [<<* ( ), 2_>.h, 3_> == 3, == , <* ( ), 1> == <* ( ), 1>, <<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>] Simplify Assuming: (AND (EQ chlval1 chlval7) (AND (EQ chlval6 chlval5) (AND (EQ chlval4 chlval3) (AND (EQ chlval2 3) TRUE)))) Done Assume bs_assert: true simplify_assume sstk:4 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 16: Invalid. false Contra ? false bs_pop simplify_pnf sstk:5 Simplify Popping done pop_pnf cons_folder !posn = 9 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Pred(true) Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42 plvmap: now normalize plvmap: now normalize bs_assert: true simplify_assume sstk:4 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:5 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 17: Invalid. false Contra ? false bs_pop simplify_pnf sstk:6 Simplify Popping done pop_pnf cons_folder !posn = 8 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Pred(true) Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35 plvmap: now normalize plvmap: now normalize bs_assert: true simplify_assume sstk:5 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:6 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 18: Invalid. false Contra ? false bs_pop simplify_pnf sstk:7 Simplify Popping done pop_pnf cons_folder !posn = 7 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Block(p@main = a@main;) Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)--->Location: id=1#10 src="list.c"; line=28 Frames: 1, 0 Must aliases of p@main are Alias pushed candidates: p@main Formals : Aliases in scope of p@main : p@main plvmap: now normalize bs_assert: And [<<* ( ), 2_>.h, 4_> == <<* ( ), 1>.h, 1>, <* ( ), 2_> == <* ( ), 1>, == ] simplify_assume sstk:6 convertToSimplifySyntax exp = And [<<* ( ), 2_>.h, 4_> == <<* ( ), 1>.h, 1>, <* ( ), 2_> == <* ( ), 1>, == ] Simplify Assuming: (AND (EQ chlval10 chlval3) (AND (EQ chlval9 chlval5) (AND (EQ chlval8 chlval7) TRUE))) Done Assume bs_assert: true simplify_assume sstk:7 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 19: Invalid. false Contra ? false bs_pop simplify_pnf sstk:8 Simplify Popping done pop_pnf cons_folder !posn = 6 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Pred(a@main != 0) Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)--->Location: id=1#9 src="list.c"; line=27 plvmap: now normalize plvmap: now normalize bs_assert: != 0 simplify_assume sstk:7 convertToSimplifySyntax exp = != 0 Simplify Assuming: (NEQ chlval3 0) Done Assume bs_assert: true simplify_assume sstk:8 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 20: Invalid. false Contra ? false bs_pop simplify_pnf sstk:9 Simplify Popping done pop_pnf cons_folder !posn = 5 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Block(a@main = tmp@main;) Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25 Frames: 1, 0 Must aliases of a@main are Alias pushed candidates: a@main Formals : Aliases in scope of a@main : a@main check field : h , true , true check field : n , false , true Exp closure: cld = 3, e = a@main, clos = a@main, * (a@main), (* (a@main)).h plvmap: now normalize bs_assert: And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] simplify_assume sstk:8 convertToSimplifySyntax exp = And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] Simplify Assuming: (AND (EQ chlval3 chlval13) (AND (EQ chlval5 chlval12) (AND (EQ chlval7 chlval11) TRUE))) Done Assume bs_assert: true simplify_assume sstk:9 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 21: Invalid. false Contra ? false bs_pop simplify_pnf sstk:10 Simplify Popping done pop_pnf cons_folder !posn = 4 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] FunctionCall(tmp@main = malloc(512)) Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))---> Location: id=1#4 src="list.c"; line=24 In Deconstruct_fc :tmp@main=malloc(,512) In Deconstruct_fc :tmp@main=malloc(,512) Funcall assignment Symvars: asgn_list is: tmp@main = ; Frames: 1, 0 Must aliases of tmp@main are Alias pushed candidates: tmp@main Formals : Aliases in scope of tmp@main : tmp@main check field : h , true , true check field : n , false , true Exp closure: cld = 3, e = tmp@main, clos = tmp@main, * (tmp@main), (* (tmp@main)).h Warning:bad arg to lv_of_expr bwpred is : And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] plvmap: now normalize bs_assert: And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] simplify_assume sstk:9 convertToSimplifySyntax exp = And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] Simplify Assuming: (AND (EQ chlval13 chlval16) (AND (EQ chlval12 chlval15) (AND (EQ chlval11 chlval14) TRUE))) Done Assume bs_assert: true simplify_assume sstk:10 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 22: Invalid. false Contra ? false bs_pop simplify_pnf sstk:11 Simplify Popping done pop_pnf cons_folder !posn = 3 In block_concrete_data_pre -- arguments are: fname is main [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Skip Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24 plvmap: now normalize bs_assert: true simplify_assume sstk:10 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:11 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 23: Invalid. false Contra ? false bs_pop simplify_pnf sstk:12 Simplify Popping done pop_pnf cons_folder !posn = 2 In block_concrete_data_pre -- arguments are: fname is __BLAST_initialize_list.c [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Block(Return(0);) Location: id=2#1 src="list.c"; line=0---Block(Return(0);)--->Location: id=2#0 (Artificial) block c_ Pre: Hit isReturn Ingoing edges : Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) Now matching... Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) In Deconstruct_fc :__BLAST_initialize_list.c() rt is * (sizeof(<0>)) fname is __BLAST_initialize_list.c Frames: 1, 0 WP of return In asgn_of_return In copy_back_asgns plvmap: now normalize bs_assert: true simplify_assume sstk:11 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:12 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 24: Invalid. false Contra ? false bs_pop simplify_pnf sstk:13 Simplify Popping done pop_pnf cons_folder !posn = 1 In block_concrete_data_pre -- arguments are: fname is __BLAST_initialize_list.c [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] SymHook(__BLAST_initialize_list.c) Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0 Hook-plug: plvmap: now normalize bs_assert: true simplify_assume sstk:12 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:13 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 25: Invalid. false Contra ? false bs_pop simplify_pnf sstk:14 Simplify Popping done pop_pnf cons_folder !posn = 0 In block_concrete_data_pre -- arguments are: fname is __BLAST_initialize_list.c [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] FunctionCall(__BLAST_initialize_list.c()) Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial) In Deconstruct_fc :__BLAST_initialize_list.c() In Deconstruct_fc :__BLAST_initialize_list.c() Funcall assignment Symvars: asgn_list is: Frames: 2, 1, 0 bwpred is : true plvmap: now normalize bs_assert: true simplify_assume sstk:13 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:14 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 26: Invalid. false Contra ? false bs_pop simplify_pnf sstk:15 Simplify Popping done pop_pnf bs_reset simplify_pop sstk:14 Simplify Popping Done pop simplify_pop sstk:13 Simplify Popping Done pop simplify_pop sstk:12 Simplify Popping Done pop simplify_pop sstk:11 Simplify Popping Done pop simplify_pop sstk:10 Simplify Popping Done pop simplify_pop sstk:9 Simplify Popping Done pop simplify_pop sstk:8 Simplify Popping Done pop simplify_pop sstk:7 Simplify Popping Done pop simplify_pop sstk:6 Simplify Popping Done pop simplify_pop sstk:5 Simplify Popping Done pop simplify_pop sstk:4 Simplify Popping Done pop simplify_pop sstk:3 Simplify Popping Done pop simplify_pop sstk:2 Simplify Popping Done pop simplify_pop sstk:1 Simplify Popping Done pop THE CONSTRAINTS ARE: true true true true And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] != 0 And [<<* ( ), 2_>.h, 4_> == <<* ( ), 1>.h, 1>, <* ( ), 2_> == <* ( ), 1>, == ] true true And [<<* ( ), 2_>.h, 3_> == 3, == , <* ( ), 1> == <* ( ), 1>, <<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>] <<* ( ), 1>.h, 1> != 1 <<* ( ), 1>.h, 1> != 2 <<* ( ), 1>.h, 1> != 3 END CONSTRAINTS block_a_t: building blocks end get_useful_blocks: size =14 0 :: 0: FunctionCall(__BLAST_initialize_list.c()) :: -1 -1 :: -1: SymHook(__BLAST_initialize_list.c) :: 0 0 :: 0: Block(Return(0);) :: -1 -1 :: -1: Skip :: 24 24 :: 24: FunctionCall(tmp@main = malloc(512 , )) :: 24 24 :: 24: Block(a@main = tmp@main;) :: 25 25 :: 25: Pred(a@main != 0) :: 27 27 :: 27: Block(p@main = a@main;) :: 28 28 :: 28: Pred(true) :: 35 35 :: 35: Pred(true) :: 42 42 :: 42: Block(* (p@main ).h = 3;p@main = a@main;) :: 46 46 :: 46: Pred(* (p@main ).h != 1) :: 48 48 :: 48: Pred(* (p@main ).h != 2) :: 50 50 :: 50: Pred(* (p@main ).h != 3) :: 51 Assert end condition bs_assert: true simplify_assume sstk:0 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:1 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > > > > > > > > > > > > > > > 27: Invalid. false Contra ? false pos = 13 bs_pop simplify_pnf sstk:2 Simplify Popping done pop_pnf bs_assert: <<* ( ), 1>.h, 1> != 3 simplify_assume sstk:1 convertToSimplifySyntax exp = <<* ( ), 1>.h, 1> != 3 Simplify Assuming: (NEQ chlval1 3) Done Assume bs_assert: true simplify_assume sstk:2 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 28: Invalid. false Contra ? false pos = 12 bs_pop simplify_pnf sstk:3 Simplify Popping done pop_pnf bs_assert: <<* ( ), 1>.h, 1> != 2 simplify_assume sstk:2 convertToSimplifySyntax exp = <<* ( ), 1>.h, 1> != 2 Simplify Assuming: (NEQ chlval1 2) Done Assume bs_assert: true simplify_assume sstk:3 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 29: Invalid. false Contra ? false pos = 11 bs_pop simplify_pnf sstk:4 Simplify Popping done pop_pnf bs_assert: <<* ( ), 1>.h, 1> != 1 simplify_assume sstk:3 convertToSimplifySyntax exp = <<* ( ), 1>.h, 1> != 1 Simplify Assuming: (NEQ chlval1 1) Done Assume bs_assert: true simplify_assume sstk:4 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 30: Invalid. false Contra ? false pos = 10 bs_pop simplify_pnf sstk:5 Simplify Popping done pop_pnf bs_assert: And [<<* ( ), 2_>.h, 3_> == 3, == , <* ( ), 1> == <* ( ), 1>, <<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>] simplify_assume sstk:4 convertToSimplifySyntax exp = And [<<* ( ), 2_>.h, 3_> == 3, == , <* ( ), 1> == <* ( ), 1>, <<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>] Simplify Assuming: (AND (EQ chlval1 chlval7) (AND (EQ chlval6 chlval5) (AND (EQ chlval4 chlval3) (AND (EQ chlval2 3) TRUE)))) Done Assume bs_assert: true simplify_assume sstk:5 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 31: Invalid. false Contra ? false pos = 9 bs_pop simplify_pnf sstk:6 Simplify Popping done pop_pnf bs_assert: true simplify_assume sstk:5 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:6 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 32: Invalid. false Contra ? false pos = 8 bs_pop simplify_pnf sstk:7 Simplify Popping done pop_pnf bs_assert: true simplify_assume sstk:6 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:7 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 33: Invalid. false Contra ? false pos = 7 bs_pop simplify_pnf sstk:8 Simplify Popping done pop_pnf bs_assert: And [<<* ( ), 2_>.h, 4_> == <<* ( ), 1>.h, 1>, <* ( ), 2_> == <* ( ), 1>, == ] simplify_assume sstk:7 convertToSimplifySyntax exp = And [<<* ( ), 2_>.h, 4_> == <<* ( ), 1>.h, 1>, <* ( ), 2_> == <* ( ), 1>, == ] Simplify Assuming: (AND (EQ chlval10 chlval3) (AND (EQ chlval9 chlval5) (AND (EQ chlval8 chlval7) TRUE))) Done Assume bs_assert: true simplify_assume sstk:8 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 34: Invalid. false Contra ? false pos = 6 bs_pop simplify_pnf sstk:9 Simplify Popping done pop_pnf bs_assert: != 0 simplify_assume sstk:8 convertToSimplifySyntax exp = != 0 Simplify Assuming: (NEQ chlval3 0) Done Assume bs_assert: true simplify_assume sstk:9 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 35: Invalid. false Contra ? false pos = 5 bs_pop simplify_pnf sstk:10 Simplify Popping done pop_pnf bs_assert: And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] simplify_assume sstk:9 convertToSimplifySyntax exp = And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] Simplify Assuming: (AND (EQ chlval3 chlval13) (AND (EQ chlval5 chlval12) (AND (EQ chlval7 chlval11) TRUE))) Done Assume bs_assert: true simplify_assume sstk:10 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 36: Invalid. false Contra ? false pos = 4 bs_pop simplify_pnf sstk:11 Simplify Popping done pop_pnf bs_assert: And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] simplify_assume sstk:10 convertToSimplifySyntax exp = And [<<* ( ), 1>.h, 1> == <<* ( ), 1>.h, 1>, <* ( ), 1> == <* ( ), 1>, == ] Simplify Assuming: (AND (EQ chlval13 chlval16) (AND (EQ chlval12 chlval15) (AND (EQ chlval11 chlval14) TRUE))) Done Assume bs_assert: true simplify_assume sstk:11 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 37: Invalid. false Contra ? false pos = 3 bs_pop simplify_pnf sstk:12 Simplify Popping done pop_pnf bs_assert: true simplify_assume sstk:11 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:12 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 38: Invalid. false Contra ? false pos = 2 bs_pop simplify_pnf sstk:13 Simplify Popping done pop_pnf bs_assert: true simplify_assume sstk:12 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:13 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 39: Invalid. false Contra ? false pos = 1 bs_pop simplify_pnf sstk:14 Simplify Popping done pop_pnf bs_assert: true simplify_assume sstk:13 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:14 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 40: Invalid. false Contra ? false pos = 0 bs_pop simplify_pnf sstk:15 Simplify Popping done pop_pnf bs_assert: true simplify_assume sstk:14 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume bs_assert: true simplify_assume sstk:15 convertToSimplifySyntax exp = true Simplify Assuming: TRUE Done Assume simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > > > > 41: Invalid. false Contra ? false simplify check contra querying exp: false convertToSimplifySyntax exp = false Simplify: FALSE Simplify : in isValid Simplify says: Simplify : in isValid Simplify says: > 42: Invalid. false Contra ? false bs_reset simplify_pop sstk:16 Simplify Popping Done pop simplify_pop sstk:15 Simplify Popping Done pop simplify_pop sstk:14 Simplify Popping Done pop simplify_pop sstk:13 Simplify Popping Done pop simplify_pop sstk:12 Simplify Popping Done pop simplify_pop sstk:11 Simplify Popping Done pop simplify_pop sstk:10 Simplify Popping Done pop simplify_pop sstk:9 Simplify Popping Done pop simplify_pop sstk:8 Simplify Popping Done pop simplify_pop sstk:7 Simplify Popping Done pop simplify_pop sstk:6 Simplify Popping Done pop simplify_pop sstk:5 Simplify Popping Done pop simplify_pop sstk:4 Simplify Popping Done pop simplify_pop sstk:3 Simplify Popping Done pop simplify_pop sstk:2 Simplify Popping Done pop simplify_pop sstk:1 Simplify Popping Done pop No useful blocks found! get_useful_blocks done. [BAT] Done setting arrays for cutting #block sets = 0 [BAT] Calling refiner [BAT] Done refiner Leaving block_a_t refine from -1 bs_reset Non-trivial functions0 SA REFINEMENT SAYS THAT THIS COUNTEREXAMPLE IS NOT SPURIOUS Expanding a summary edge Node: Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Node: Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Path: Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Path: Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Path: Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Path: Node(edge=Location: id=2#2 (Artificial)---SymHook(__BLAST_initialize_list.c)---> Location: id=2#1 src="list.c"; line=0, data=Data(id=3; kind=Node; mark=Processed_Uncovered(time_stamp=2; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) Path: Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=5; kind=Node; mark=Processed_Uncovered(time_stamp=4; region=[AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#2 (Artificial)---Skip--->Location: id=1#3 src="list.c"; line=24, data=Data(id=6; kind=Node; mark=Processed_Uncovered(time_stamp=5; region=[AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#3 src="list.c"; line=24---FunctionCall(tmp@main = malloc(512))--->Location: id=1#4 src="list.c"; line=24, data=Data(id=7; kind=Node; mark=Processed_Uncovered(time_stamp=6; region=[AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#4 src="list.c"; line=24---Block(a@main = tmp@main;)---> Location: id=1#5 src="list.c"; line=25, data=Data(id=8; kind=Node; mark=Processed_Uncovered(time_stamp=7; region=[AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#5 src="list.c"; line=25---Pred(a@main != 0)---> Location: id=1#9 src="list.c"; line=27, data=Data(id=10; kind=Node; mark=Processed_Uncovered(time_stamp=8; region=[AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#9 src="list.c"; line=27---Block(p@main = a@main;)---> Location: id=1#10 src="list.c"; line=28, data=Data(id=11; kind=Node; mark=Processed_Uncovered(time_stamp=9; region=[AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#10 src="list.c"; line=28---Pred(true)--->Location: id=1#12 src="list.c"; line=35, data=Data(id=13; kind=Node; mark=Processed_Uncovered(time_stamp=10; region=[AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#12 src="list.c"; line=35---Pred(true)--->Location: id=1#21 src="list.c"; line=42, data=Data(id=15; kind=Node; mark=Processed_Uncovered(time_stamp=11; region=[AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#21 src="list.c"; line=42---Block(* (p@main ).h = 3;p@main = a@main;)---> Location: id=1#29 src="list.c"; line=46, data=Data(id=16; kind=Node; mark=Processed_Uncovered(time_stamp=12; region=[AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#29 src="list.c"; line=46---Pred(* (p@main ).h != 1)---> Location: id=1#31 src="list.c"; line=48, data=Data(id=18; kind=Node; mark=Processed_Uncovered(time_stamp=13; region=[AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#31 src="list.c"; line=48---Pred(* (p@main ).h != 2)---> Location: id=1#34 src="list.c"; line=50, data=Data(id=20; kind=Node; mark=Processed_Uncovered(time_stamp=14; region=[AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) Path: Node(edge=Location: id=1#34 src="list.c"; line=50---Pred(* (p@main ).h != 3)---> Location: id=1#36 src="list.c"; line=51, data=Data(id=21; kind=Node; mark=Processed_Was_Covered_To_Reprocess(time_stamp=17; region=[AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) In Deconstruct_fc :__BLAST_initialize_list.c() In Deconstruct_fc :__BLAST_initialize_list.c() In Deconstruct_fc :tmp@main=malloc(,512) The following are suspect funs: malloc The following are skipped funs: Depth of tree: 14 Function summaries: --- Summaries for __BLAST_initialize_list.c --- FROM Node(edge=Location: id=1#1 src="list.c"; line=0---FunctionCall(__BLAST_initialize_list.c())---> Location: id=1#2 (Artificial), data=Data(id=2; kind=Entry; mark=Processed_Uncovered(time_stamp=1; region=[AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) TO Node(edge=Location: id=2#1 src="list.c"; line=0---Block(Return(0);)---> Location: id=2#0 (Artificial), data=Data(id=4; kind=Exit; mark=Processed_Uncovered(time_stamp=3; region=[AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] ))) --- Summaries for main --- FROM Node(edge=NONE, data=Data(id=0; kind=Entry; mark=Processed_Uncovered(time_stamp=0; region=[AtomicRegion: Location: id=1#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Top Stack: []] ))) TO Node(edge=Location: id=1#37 src="list.c"; line=20---Block(Return(0);)---> Location: id=1#0 (Artificial), data=Data(id=23; kind=Exit; mark=Processed_Uncovered(time_stamp=16; region=[AtomicRegion: Location: id=1#37 src="list.c"; line=20 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] ))) In Region.concretize -- argument is: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] In Region.concretize -- argument is: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] In Region.concretize -- argument is: [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] In Region.concretize -- argument is: [AtomicRegion: Location: id=2#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] In Region.concretize -- argument is: [AtomicRegion: Location: id=2#1 src="list.c"; line=0 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: [Location: id=1#1 src="list.c"; line=0]] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#2 (Artificial) AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#3 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#4 src="list.c"; line=24 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#5 src="list.c"; line=25 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#9 src="list.c"; line=27 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#10 src="list.c"; line=28 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#12 src="list.c"; line=35 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#21 src="list.c"; line=42 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#29 src="list.c"; line=46 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#31 src="list.c"; line=48 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#34 src="list.c"; line=50 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] In Region.concretize -- argument is: [AtomicRegion: Location: id=1#36 src="list.c"; line=51 AbstrDatRgn: Predicates: [...] Lattice: Lattice = shape class of function (default) %n = {} %p = { } Stack = Callstack: [* (sizeof(<0>)) <(default)> = __BLAST_initialize_list.c()] ] Stack: []] Start trace 0 :: 0: FunctionCall(__BLAST_initialize_list.c()) :: -1 ----> -1 :: -1: SymHook(__BLAST_initialize_list.c) :: 0 ----> 0 :: 0: FunctionCall(__BLAST_initialize_list.c()) :: -1 ----> -1 :: -1: SymHook(__BLAST_initialize_list.c) :: 0 ----> 0 :: 0: Block(Return(0);) :: -1 ----> -1 :: -1: Skip :: 24 ----> 24 :: 24: FunctionCall(tmp@main = malloc(512 , )) :: 24 ----> 24 :: 24: Block(a@main = tmp@main;) :: 25 ----> 25 :: 25: Pred(a@main != 0) :: 27 ----> 27 :: 27: Block(p@main = a@main;) :: 28 ----> 28 :: 28: Pred(true) :: 35 ----> 35 :: 35: Pred(true) :: 42 ----> 42 :: 42: Block(* (p@main ).h = 3;p@main = a@main;) :: 46 ----> 46 :: 46: Pred(* (p@main ).h != 1) :: 48 ----> 48 :: 48: Pred(* (p@main ).h != 2) :: 50 ----> 50 :: 50: Pred(* (p@main ).h != 3) :: 51 End trace Start Regions ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> ---r---> End Regions Error found! The system is unsafe :-( Model checker stats: Nb iterations of outer while loop: 0 Nb iterations of reachability: 16 Nb created nodes: 0 Nb refinment processes: 0 Nb refined nodes: 0 Nb proof tree nodes: 0 Nb proof tree covered nodes: 0 Nb deleted nodes: 0 Abstractor stats: CF Abstraction Statistics Total number of summary-posts = 1 Total number of queries = 1 Total number of non-post queries = 1 PostBdd Calls = 0 Worst-case number of post queries = 0 Actual number of post queries = 0 Assume post queries = 0 Total posts = 0 Total assume posts = 0 Total cached = 0 Total foci queries = 0 Total number of alias queries = 66 Total number of cached exp_closures =6 Total number of queryAlias_cache calls = 0 Total number of queryAlias_cache hits = 0 Total number of tproj alias queries = 0 Total number of lv_rd alias queries (computed) = 0 Total number of lv_rd alias queries (cached) = 0 Max Alias Set size = 0 Total number of recomp exp_closures =4 The List of predicates: Number of predicates =0 Maximum number of predicates active together (discounting scope) = 0 Functions visited: __BLAST_initialize_list.c , main , Number of visited functions: 2 Dumping Abstraction Writing out .abs file: list.abs Maximum #preds/loc: 0 Average #preds/loc: 0 Done writing .abs file Minor Words : 4364484. Major Words : 395169. Total size of heap in words : 368640 Error found! The system is unsafe :-( Timings: TOTAL 0.220 s (1) modelCheck 0.060 s (1) Actual model check[cf] 0.060 s (1) cleanup and go 0.000 s (1) Interpolant Refine 0.000 s (1) get useful blocks 0.000 s (1) convertToSimplifySyntax 0.000 s (46) Cons folder 0.000 s (1) convertToSimplifySyntax 0.000 s (42) load lv table 0.000 s (1) make lv_stack 0.000 s (1) TVLA: cover 0.000 s (1) get_new_data 0.000 s (14) Post of shape graphs 0.000 s (13) initialize skipfun 0.000 s (2) Kill init 0.000 s (1) read initial state 0.000 s (1) read invariants 0.000 s (1) Call graph construction 0.000 s (1) Add alias override 0.000 s (1) Modifies Database 0.160 s (1) get_lval_aliases_iter 0.160 s (15) Lval iterator 0.160 s (6) get_lval_aliases_iter[scope] 0.000 s (15) Alias analysis 0.000 s (1) Build CFA: 0.000 s (1) simplify querytime 0.000 s (12) convertToSimplifySyntax 0.000 s (12) read alias pairs 0.000 s (1) read shape class 0.000 s (1) read seeds 0.000 s (1) Parse: 0.000 s (1) Error found! The system is unsafe :-( Checking manager. Opening file list.bdd Calling BddStore