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: alternating_list.c Putting in initializer __BLAST_initialize_alternating_list.c Finished Parsing Begin Building CFA Encountered function exit Finished converting function exit Encountered function main ********* function call: __BLAST_initialize_alternating_list.cForking Simplify process... done! ********* function call: exit********* function call: exit********* function call: printfFinished converting function main Encountered function __BLAST_initialize_alternating_list.c Finished converting function __BLAST_initialize_alternating_list.c Start Building Callgraph-ocp Filling SCC info SCC 1: main SCC 2: exit SCC 3: __BLAST_initialize_alternating_list.c SCC info filled 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: 7 Visited functions: 3 Visited existing functions: 3 Defined functions: main exit __BLAST_initialize_alternating_list.c Finished Building CFA Starting the alias analysis In do_bdd_alias Number of BDD variables = 4 a@main __BLAST_initialize_alternating_list.c t@main flag@main tmp@main __bddptsto_mem0 p@main __bddptsto_mem1 exit main __retres@main s@exit bdd_pts_to: Starting iteration. Number of edges (flow insensitive) 10.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_alternating_list.c Direct Wr:3:__BLAST_initialize_alternating_list.c COMP MOD iter1 done COMP MOD iter2 done Proc. scc--1 Compute scc_mods: 1 : 1 : main Direct Wr:1:main Warning:Error raised in checkAliasFI!:Not_found for inputs __BLAST_NONDET@main and (* (p@main)).h COMP MOD iter1 done COMP MOD iter2 done Done computing mods Write mods to : alternating_list.mods.gl Done writing to :alternating_list.mods.gl Write mods to : alternating_list.mods.fl Done writing to :alternating_list.mods.fl Write mods to : alternating_list.mods.mmb Done writing to :alternating_list.mods.mmb Write mods to : alternating_list.mods.ceef Done writing to :alternating_list.mods.ceef Done writing mods In add_symbolic_hooks [add_symbolic_hooks] Processing function: __BLAST_initialize_alternating_list.c [add_symbolic_hooks] Processing function: exit Done post-alias-analysis back from post_alias_analysis 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: 7 Visited functions: 3 Visited existing functions: 3 Defined functions: main exit __BLAST_initialize_alternating_list.c Unknown fun : DRIVER: TVLA Initialization... DRIVER: TVLA Initialization... Initialized Abstraction SA: Add predicate sm SA: Add predicate eq SA: Add predicate isnew UL> Shape Analysis enabled Done adding seed predicates ********** Now running the model-checker ********** Glob useful preds Glob useful preds Setting signal for 2000 seconds block_analyze_trace In block_a_t:15 Adding stamp field: all? true :h Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr3 get_useful_blocks: size =15 get_useful_blocks done. Conflicting Blocks [INF] 10 : 39: Block(* (p@main ).h = 3;p@main = a@main;flag@main = 1;) [INF] 12 : 45: Pred(flag@main == 0) [BAT] Done setting arrays for cutting [BAT] Calling refiner Symbol foci2 occurs formulas 0 and 1 UNSAT! Prover calls: 1 case splits: 0 Finished computing interpolant. Size = 9 Finished substituting simplified size: 1 Finished simplifying addPred: 0: (gui) adding predicate flag@main==1 to the system addPred: 0: (gui) adding predicate flag@main==1 to the system [BAT] Done refiner Non-trivial functions1 This is a false error (seq) Delete children of Start over again! block_analyze_trace In block_a_t:20 Adding stamp field: all? true :n Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr0 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr3 Warning:bad arg to lv_of_expr Warning:bad arg to lv_of_expr1 Location: id=1#1 src="alternating_list.c"; line=0---FunctionCall(__BLAST_initialize_alternating_list.c())---> Location: id=1#2 (Artificial) rt is * (sizeof(<0>)) fname is __BLAST_initialize_alternating_list.c get_useful_blocks: size =20 get_useful_blocks done. [BAT] Done setting arrays for cutting [BAT] Calling refiner [BAT] Done refiner Non-trivial functions1 saref_block_analyze_trace In saref_block_a_t:20 saref: Heuristically look for new shape predicates in the interpolants Symbol foci16 occurs formulas 6 and 7 UNSAT! Prover calls: 1 case splits: 0 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 2 Finished computing interpolant. Size = 9 Finished computing interpolant. Size = 9 Finished computing interpolant. Size = 6 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished computing interpolant. Size = 5 Finished substituting simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 Finished simplifying SA Refinement: New list pointer discovered: p@main SA Refinement: New list pointer discovered: a@main SA Refinement: New list node predicate discovered: (* (__$AUTO$__)).h==3 SA REFINEMENT COULD OCCUR!!! This is a false error (saref) clear_summary Delete children of Start over again! SA: Shape refinement occured: dropping already created shape classes DRIVER: TVLA Initialization... SA: Add predicate sm SA: Add predicate eq SA: Add predicate isnew TVLA: create_predicate 2, field_[n] SA: Add predicate field_n TVLA: create_instr_predicate 1, c_[n] SA: Add predicate c_n TVLA: create_predicate 1, ptsto_[p@main] SA: Add predicate pt_p@main TVLA: create_instr_predicate 1, r_[p@main,n] SA: Add predicate r_p@main,n TVLA: create_predicate 1, ptsto_[t@main] SA: Add predicate pt_t@main TVLA: create_instr_predicate 1, r_[t@main,n] SA: Add predicate r_t@main,n TVLA: create_predicate 1, ptsto_[tmp@main] SA: Add predicate pt_tmp@main TVLA: create_instr_predicate 1, r_[tmp@main,n] SA: Add predicate r_tmp@main,n TVLA: create_predicate 1, ptsto_[a@main] SA: Add predicate pt_a@main TVLA: create_instr_predicate 1, r_[a@main,n] SA: Add predicate r_a@main,n TVLA: create_predicate 1, content(\__$AUTO$__. (* (__$AUTO$__)).h==3) SA: Add predicate \__$AUTO$__.(* (__$AUTO$__)).h==3 While loop tick: 100 : Funcs: 1 block_analyze_trace In block_a_t:21 Warning:bad arg to lv_of_expr0 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr3 Warning:bad arg to lv_of_expr Warning:bad arg to lv_of_expr0 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr Warning:bad arg to lv_of_expr1 Location: id=1#1 src="alternating_list.c"; line=0---FunctionCall(__BLAST_initialize_alternating_list.c())---> Location: id=1#2 (Artificial) rt is * (sizeof(<0>)) fname is __BLAST_initialize_alternating_list.c get_useful_blocks: size =21 get_useful_blocks done. [BAT] Done setting arrays for cutting [BAT] Calling refiner [BAT] Done refiner Non-trivial functions1 saref_block_analyze_trace In saref_block_a_t:21 saref: Heuristically look for new shape predicates in the interpolants Symbol foci44 occurs formulas 6 and 7 UNSAT! Prover calls: 8 case splits: 0 Finished computing interpolant. Size = 16 Finished computing interpolant. Size = 16 Finished computing interpolant. Size = 16 Finished computing interpolant. Size = 16 Finished computing interpolant. Size = 16 Finished computing interpolant. Size = 16 Finished computing interpolant. Size = 23 Finished computing interpolant. Size = 23 Finished computing interpolant. Size = 23 Finished computing interpolant. Size = 23 Finished computing interpolant. Size = 23 Finished computing interpolant. Size = 28 Finished computing interpolant. Size = 35 Finished computing interpolant. Size = 35 Finished computing interpolant. Size = 32 Finished computing interpolant. Size = 33 Finished computing interpolant. Size = 29 Finished computing interpolant. Size = 29 Finished computing interpolant. Size = 29 Finished computing interpolant. Size = 29 Finished substituting simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 3 simplified size: 5 simplified size: 5 simplified size: 5 simplified size: 5 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 Finished simplifying SA Refinement: New list node predicate discovered: (* (__$AUTO$__)).h==1 SA REFINEMENT COULD OCCUR!!! This is a false error (saref) clear_summary Delete children of Start over again! SA: Shape refinement occured: dropping already created shape classes DRIVER: TVLA Initialization... SA: Add predicate sm SA: Add predicate eq SA: Add predicate isnew TVLA: pseudo_create_predicate field_[n] SA: Add predicate field_n TVLA: pseudo_create_instr_predicate c_[n] SA: Add predicate c_n TVLA: pseudo_create_predicate ptsto_[t@main] SA: Add predicate pt_t@main TVLA: pseudo_create_instr_predicate r_[t@main,n] SA: Add predicate r_t@main,n TVLA: pseudo_create_predicate ptsto_[a@main] SA: Add predicate pt_a@main TVLA: pseudo_create_instr_predicate r_[a@main,n] SA: Add predicate r_a@main,n TVLA: pseudo_create_predicate ptsto_[tmp@main] SA: Add predicate pt_tmp@main TVLA: pseudo_create_instr_predicate r_[tmp@main,n] SA: Add predicate r_tmp@main,n TVLA: pseudo_create_predicate ptsto_[p@main] SA: Add predicate pt_p@main TVLA: pseudo_create_instr_predicate r_[p@main,n] SA: Add predicate r_p@main,n TVLA: create_predicate 1, content(\__$AUTO$__. (* (__$AUTO$__)).h==1) SA: Add predicate \__$AUTO$__.(* (__$AUTO$__)).h==1 TVLA: pseudo_create_predicate content(\__$AUTO$__. (* (__$AUTO$__)).h==3) SA: Add predicate \__$AUTO$__.(* (__$AUTO$__)).h==3 block_analyze_trace In block_a_t:32 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr0 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr3 Warning:bad arg to lv_of_expr Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr2 Warning:bad arg to lv_of_expr Warning:bad arg to lv_of_expr0 Warning:bad arg to lv_of_expr1 Warning:bad arg to lv_of_expr Warning:bad arg to lv_of_expr1 Location: id=1#1 src="alternating_list.c"; line=0---FunctionCall(__BLAST_initialize_alternating_list.c())---> Location: id=1#2 (Artificial) rt is * (sizeof(<0>)) fname is __BLAST_initialize_alternating_list.c get_useful_blocks: size =32 get_useful_blocks done. [BAT] Done setting arrays for cutting [BAT] Calling refiner [BAT] Done refiner Non-trivial functions1 saref_block_analyze_trace In saref_block_a_t:32 saref: Heuristically look for new shape predicates in the interpolants Symbol foci85 occurs formulas 6 and 7 UNSAT! Prover calls: 20 case splits: 0 Finished computing interpolant. Size = 58 Finished computing interpolant. Size = 58 Finished computing interpolant. Size = 58 Finished computing interpolant. Size = 58 Finished computing interpolant. Size = 58 Finished computing interpolant. Size = 58 Finished computing interpolant. Size = 65 Finished computing interpolant. Size = 65 Finished computing interpolant. Size = 65 Finished computing interpolant. Size = 65 Finished computing interpolant. Size = 65 Finished computing interpolant. Size = 65 Finished computing interpolant. Size = 72 Finished computing interpolant. Size = 72 Finished computing interpolant. Size = 82 Finished computing interpolant. Size = 80 Finished computing interpolant. Size = 78 Finished computing interpolant. Size = 82 Finished computing interpolant. Size = 89 Finished computing interpolant. Size = 87 Finished computing interpolant. Size = 76 Finished computing interpolant. Size = 72 Finished computing interpolant. Size = 64 Finished computing interpolant. Size = 64 Finished computing interpolant. Size = 64 Finished computing interpolant. Size = 64 Finished computing interpolant. Size = 64 Finished computing interpolant. Size = 62 Finished computing interpolant. Size = 63 Finished computing interpolant. Size = 63 Finished computing interpolant. Size = 63 Finished substituting simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 4 simplified size: 4 simplified size: 6 simplified size: 6 simplified size: 6 simplified size: 7 simplified size: 12 simplified size: 12 simplified size: 9 simplified size: 9 simplified size: 3 simplified size: 3 simplified size: 3 simplified size: 3 simplified size: 3 simplified size: 1 simplified size: 1 simplified size: 1 simplified size: 1 Finished simplifying SA Refinement: New list node predicate discovered: (* (__$AUTO$__)).h==2 SA REFINEMENT COULD OCCUR!!! This is a false error (saref) clear_summary Delete children of Start over again! SA: Shape refinement occured: dropping already created shape classes DRIVER: TVLA Initialization... SA: Add predicate sm SA: Add predicate eq SA: Add predicate isnew TVLA: pseudo_create_predicate field_[n] SA: Add predicate field_n TVLA: pseudo_create_instr_predicate c_[n] SA: Add predicate c_n TVLA: pseudo_create_predicate ptsto_[t@main] SA: Add predicate pt_t@main TVLA: pseudo_create_instr_predicate r_[t@main,n] SA: Add predicate r_t@main,n TVLA: pseudo_create_predicate ptsto_[a@main] SA: Add predicate pt_a@main TVLA: pseudo_create_instr_predicate r_[a@main,n] SA: Add predicate r_a@main,n TVLA: pseudo_create_predicate ptsto_[tmp@main] SA: Add predicate pt_tmp@main TVLA: pseudo_create_instr_predicate r_[tmp@main,n] SA: Add predicate r_tmp@main,n TVLA: pseudo_create_predicate ptsto_[p@main] SA: Add predicate pt_p@main TVLA: pseudo_create_instr_predicate r_[p@main,n] SA: Add predicate r_p@main,n TVLA: create_predicate 1, content(\__$AUTO$__. (* (__$AUTO$__)).h==2) SA: Add predicate \__$AUTO$__.(* (__$AUTO$__)).h==2 TVLA: pseudo_create_predicate content(\__$AUTO$__. (* (__$AUTO$__)).h==1) SA: Add predicate \__$AUTO$__.(* (__$AUTO$__)).h==1 TVLA: pseudo_create_predicate content(\__$AUTO$__. (* (__$AUTO$__)).h==3) SA: Add predicate \__$AUTO$__.(* (__$AUTO$__)).h==3 While loop tick: 200 : Funcs: 1 block_analyze_trace In block_a_t:32 Warning:bad arg to lv_of_expr0 Warning:bad arg to lv_of_expr0 get_useful_blocks: size =32 get_useful_blocks done. Conflicting Blocks [INF] 25 : 46: Block(flag@main = 0;) [INF] 29 : 45: Pred(flag@main != 0) [BAT] Done setting arrays for cutting [BAT] Calling refiner Symbol foci146 occurs formulas 0 and 1 UNSAT! Prover calls: 0 case splits: 0 Finished computing interpolant. Size = 5 Finished substituting simplified size: 1 Finished simplifying addPred: 1: (gui) adding predicate flag@main==0 to the system addPred: 1: (gui) adding predicate flag@main==0 to the system [BAT] Done refiner Non-trivial functions1 This is a false error (seq) Delete children of Start over again! While loop tick: 300 : Funcs: 1 While loop tick: 400 : Funcs: 1 No error found. The system is safe :-) Model checker stats: Nb iterations of outer while loop: 0 Nb iterations of reachability: 440 Nb created nodes: 0 Nb refinment processes: 5 Nb refined nodes: 0 Nb proof tree nodes: 154 Nb proof tree covered nodes: 48 Nb deleted nodes: 0 Abstractor stats: CF Abstraction Statistics Total number of summary-posts = 6 Total number of queries = 681 Total number of non-post queries = 1 PostBdd Calls = 356 Worst-case number of post queries = 882 Actual number of post queries = 478 Assume post queries = 218 Total posts = 330 Total assume posts = 176 Total cached = 0 Total foci queries = 5 Total number of alias queries = 112 Total number of cached exp_closures =90 Total number of queryAlias_cache calls = 30 Total number of queryAlias_cache hits = 29 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 =10 The List of predicates: Number of predicates =2 Maximum number of predicates active together (discounting scope) = 0 Functions visited: exit , __BLAST_initialize_alternating_list.c , main , Number of visited functions: 3 Writing out .abs file: alternating_list.abs Maximum #preds/loc: 2 Average #preds/loc: 0 Done writing .abs file Minor Words : 23785751. Major Words : 1684361. Total size of heap in words : 798720 No error found. The system is safe :-) Timings: TOTAL 1.730 s (1) modelCheck 1.590 s (1) Actual model check[cf] 1.590 s (1) TVLA: merge 0.010 s (155) compute itpN 0.270 s (3) foci itpn 0.270 s (3) convertToSimplifySyntax 0.020 s (6) cleanup and go 0.000 s (5) Interpolant Refine 0.000 s (5) extract foci preds (cf) 0.000 s (2) convertToSimplifySyntax 0.000 s (24) get useful blocks 0.010 s (5) convertToSimplifySyntax 0.000 s (307) Cons folder 0.010 s (5) convertToSimplifySyntax 0.000 s (255) load lv table 0.000 s (5) make lv_stack 0.000 s (5) TVLA: cover 0.070 s (455) get_new_data 1.070 s (430) postBdd 0.030 s (356) bddForEachCube-post 0.020 s (351) simplify querytime 0.000 s (202) convertToSimplifySyntax 0.000 s (202) _check_pred 0.010 s (325) simp-a2: 0.000 s (233) simplify querytime 0.000 s (233) convertToSimplifySyntax 0.000 s (233) simp-a1: 0.010 s (233) simplify querytime 0.010 s (233) convertToSimplifySyntax 0.000 s (233) _assume 0.000 s (325) convertToSimplifySyntax 0.000 s (325) _check_Pred_list 0.000 s (325) _check_pred 0.010 s (5) simp-a2: 0.000 s (6) simplify querytime 0.000 s (6) convertToSimplifySyntax 0.000 s (6) simp-a1: 0.000 s (6) simplify querytime 0.000 s (6) convertToSimplifySyntax 0.000 s (6) _assume 0.000 s (5) convertToSimplifySyntax 0.000 s (5) _check_Pred_list 0.000 s (5) wp_diff_filter 0.000 s (356) getPossibleAliases 0.000 s (696) filter alias candidates 0.000 s (696) queryAlias 0.000 s (1) getVarsAndDerefs 0.000 s (696) mk_pred_triple 0.000 s (356) Post of shape graphs 1.010 s (306) convertToSimplifySyntax 0.090 s (6906) TVLA: merge 0.000 s (14) TVLA: run action 0.770 s (322) 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.140 s (1) get_lval_aliases_iter 0.140 s (19) Lval iterator 0.140 s (8) get_lval_aliases_iter[scope] 0.000 s (19) Alias analysis 0.000 s (1) Build CFA: 0.000 s (1) simplify querytime 0.000 s (14) convertToSimplifySyntax 0.000 s (14) 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) No error found. The system is safe :-) Checking manager. Opening file alternating_list.bdd Calling BddStore Variables: 23, Clauses: 32 Backtracks = 0, decisions = 3 Variables: 231, Clauses: 353 Backtracks = 0, decisions = 59 Variables: 231, Clauses: 391 Backtracks = 0, decisions = 35 Variables: 567, Clauses: 956 Backtracks = 0, decisions = 141 Variables: 14, Clauses: 26 Backtracks = 0, decisions = 0