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
Putting in initializer __BLAST_initialize_list.c
Finished Parsing
Reading in shape class...
Shape class read.

Begin Building CFA
Encountered function exit
Finished converting function exit
Encountered function main
********* function call: __BLAST_initialize_list.c
list.c:53: Warning: Return statement with a value in function returning void
Forking Simplify process...
done!

********* function call: exit********* function call: exit********* function call: exitFinished converting function main
Encountered function __BLAST_initialize_list.c
Finished converting function __BLAST_initialize_list.c
Start Building Callgraph-ocp
Filling SCC info
SCC 1: main
SCC 2: exit
SCC 3: __BLAST_initialize_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: 9
Visited functions: 3
Visited existing functions: 3
Defined functions:
main 
exit 
__BLAST_initialize_list.c 
Finished Building CFA
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.

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
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 : 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
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: Add predicate sm
SA: Add predicate eq
SA: Add predicate isnew
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_[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_[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_[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(\x. (* (x)).h==1)
SA: Add predicate \x.(* (x)).h==1
TVLA: create_predicate 1, content(\x. (* (x)).h==2)
SA: Add predicate \x.(* (x)).h==2
TVLA: create_predicate 1, content(\x. (* (x)).h==3)
SA: Add predicate \x.(* (x)).h==3
UL> Shape Analysis enabled
Done adding seed predicates



********** Now running the model-checker **********


Glob useful preds

Glob useful preds

Setting signal for 2000 seconds
While loop tick: 100 : Funcs: 2

While loop tick: 200 : Funcs: 2



No error found.  The system is safe :-)



Model checker stats:

Nb iterations of outer while loop: 0
Nb iterations of reachability: 235
Nb created nodes: 0
Nb refinment processes: 0
Nb refined nodes: 0
Nb proof tree nodes: 223
Nb proof tree covered nodes: 76
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 =0
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 =0
The List of predicates:


Number of predicates =0 
Maximum number of predicates active together (discounting scope) = 0

Functions visited:
__BLAST_initialize_list.c , exit , main , 
Number of visited functions:  3
Writing out .abs file: list.abs
Maximum #preds/loc: 0
Average #preds/loc: 0
Done writing .abs file

Minor Words : 8125584.
Major Words : 649147.
Total size of heap in words : 552960


No error found.  The system is safe :-)

Timings:
TOTAL                          3.760 s (1)
  modelCheck                     3.600 s (1)
    Actual model check[cf]           3.590 s (1)
      TVLA: merge                    0.640 s (800)
      TVLA: cover                    0.500 s (962)
      get_new_data                   2.410 s (237)
        Post of shape graphs           2.410 s (233)
          convertToSimplifySyntax           0.060 s (7666)
          TVLA: merge                    0.010 s (11)
          TVLA: run action               2.240 s (336)
    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)


No error found.  The system is safe :-)

Checking manager.
Opening file list.bdd
Calling BddStore