let main () =
(* try *)
  Message.set_verbosity Message.Default;
  Stats.reset ();
  Options.buildOptionsDatabase ();

  
  if (Options.getValueOfBool "interactive" = true) then
    (* Shell mode. Read inputs from stdin and execute them. *)
    interactive ()
  else begin
    let reachLabel = (Options.getValueOfString "L")
    and source_files = (Options.getSourceFiles ()) in
    (* No reachLabel has been specified on the command line *)
    if(reachLabel = "") then
      begin
        Printf.printf "No error label specified!\n" ;
        exit 1
      end
    else
      () ;
    if (source_files == [])
    then
      begin
        Message.msg_string Message.Error ("Error: no input source file specified") ;
        exit 1
      end ;
    Message.msg_string Message.Normal ("Parsing files: " ^ (Misc.strList source_files)) ;
    
    Stats.time "Parse:" C_System_Descr.initialize source_files ;
    AliasAnalyzer.constructAliasDatabase () ; 
    
    if (Options.getValueOfBool "test") then
      begin
        testModelCheck 0 ; 
        exit 1 
      end 
    else () ; 
  
    (* Add the sym_var_hooks for CF reachability *)
    let error_location =
      match (C_System_Descr.get_locations_at_label reachLabel) with
        [l] -> Some l
      | [] when Options.getValueOfBool "checkRace" -> None
      | []  ->
          Message.msg_string Message.Error ("Error: label '" ^ reachLabel ^
                                            "' was not found in the source file(s)") ;
          exit 1
      | _   ->
          Message.msg_string Message.Error ("Error: label '" ^ reachLabel ^
                                            "' appears multiple times in the source file(s)") ;
          exit 1
    in
      (* Hooking up the spec *)
      (* RJ: old " stuff. eschewed. *)
      (*
        C_System_Descr.instrument_with_spec (Options.getValueOfString ")
        (Options.getValueOfString ") ;
        *)
    Message.msg_string Message.Debug "\n\n\n\n\nPrinting System Description\n\n" ;
    Message.msg_printer Message.Debug C_System_Descr.print_system () ;
(*
  if (Options.getValueOfBool ") then begin
  C_System_Descr.compute_callgraph ();
  C_System_Descr.output_callgraph " ;
  end ;
  *)
    
    Stats.time "modelCheck" modelCheck error_location ;
  end;
  let memstats = Gc.stat () in
  Message.msg_string Message.Normal ("Minor Words : "^(string_of_float memstats.Gc.minor_words)) ;
      Message.msg_string Message.Normal ("Major Words : "^(string_of_float memstats.Gc.major_words)) ;
      Message.msg_string Message.Normal ("Total size of heap in words : "^(string_of_int memstats.Gc.heap_words)) ;
      Stats.print stderr "Timings:\n"