src/abs/absCmd.c File Reference

#include "absInt.h"

Include dependency graph for absCmd.c:

Go to the source code of this file.

Functions
static int	CommandAbsCtl (Hrc_Manager_t **hmgr, int argc, char **argv)
static AbsOptions_t *	ParseAbsCtlOptions (int argc, char **argv)
static void	TimeOutHandle (int sigType)
void	Abs_Init (void)
void	Abs_End (void)
Variables
static char rcsid[]	UNUSED = "$Id: absCmd.c,v 1.37 2002/09/08 22:13:50 fabio Exp $"
static jmp_buf	timeOutEnv
static int	absTimeOut
static long	alarmLap

---

Function Documentation

void Abs_End

(

void

)

Function********************************************************************

Synopsis [End abs package]

SideEffects []

Definition at line 80 of file absCmd.c.

{
}

Here is the caller graph for this function:

void Abs_Init

(

void

)

AutomaticEnd Function********************************************************************

Synopsis [Initialize abs package]

SideEffects []

Definition at line 66 of file absCmd.c.

{
  Cmd_CommandAdd("incremental_ctl_verification", CommandAbsCtl, 0);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandAbsCtl	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

AutomaticStart

Function********************************************************************

Synopsis [Encapsulation of the incremental_ctl_verification command.]

Description [The function starts by parsing the options. After that it checks for the network structure. The ctl formulas are read and check for correctness. Once the formulas have been read, they need to be translated from the CTL representation to the operational graph representation required for the incremental algorithm. The function AbsCtlFormulaArrayTranslate performs this task. After all these points have been cleared, the timeout is programmed and the verification process starts.

Once the result has been obtained, the function prints the result as well as some execution statistics, de-allocates all the required data structures and returns.]

SideEffects []

CommandName [incremental_ctl_verification]

CommandSynopsis [Verify a set of CTL formulas by means of an incremental model checking algorithm.]

CommandArguments [\[-D <number>\] \[-e\] \[-h\] \[-n\] \ \[-s\] \[-t <seconds>\] \[-v <number>\] \[-V <number>\] \[-x\] <ctlfile>]]

CommandDescription [ Like model_check, incremental_ctl_verification verifies a set of CTL formulas. It uses a system of abstraction and incremental refinement that works for all of (fair)CTL, using over and underapproximations as appropriate. See \[1,2\] for details.

Incremental_ctl_verification (also known as Abs or Trasgo) works especially well on large systems on which mc is too slow or runs out of memory. Unlike amc, it can handle full CTL, not just the universal or existential subsets of it. Also, fairness is supported with this command, although it tends to be inefficient. Support for the mu-calculus is not yet implemented.

Before using incremental_ctl_verification, a flattened hierarchy should be present. See `help init`. Using dynamic variable reordering may be beneficial on large systems. See `help dynamic_var_ordering`.

Fairness constraints can be applied using `read_fairness', as with mc. When using incremental verification with fairness, there is no check for unfair initial states. Please be aware that if there are no fair initial states, all formulas starting with "A" will be trivially true. Mc will tell you whether you have fair initial states.

A typical use would be
incremental_ctl_verification -D2 <ctl_file>

For every formula, incremental verification will report whether it is valid or invalid, or it returns an inconclusive result. A formula is valid iff it holds for all initial states. An error trace is not provided.

For the people who are used to mc: The -r option is not supported, incremental verification always reduces the fsm with respect to individual formulas. The -c option is not supported either. There is no sharing of subformulas between different formulas.

Command options:

-D <number>

Specify extent to which don't cares are used to simplify the MDDs.

• 0: No Don't Cares used.
• 1: Use reachability information to compute the don't-care set. Reachability is performed by formula. This is different from mc, where reachability is performed only once.
• 2: Use reachability information, and minimize the transition relation with respect to the `frontier set' (aggresive minimization).

The equivalent of mc -D3 is not implemented.

-e

Compute the set of fair states (those satisfying the formula EGfair TRUE) before the verification process and use the result as care set. In certain cases this will speed up computation when fairness constraints are present. In other cases it will slow it down.

-h

Print the command usage.

-n

Try to prove the negation of every formula. In some cases it may be easier to prove the negation of a formula than the formula itself. For systems with only one initial state, a formula is true iff its negation is false. Note that for systems with multiple initial states a formula and its negation can both be false.

-s

Print a summary of statistics after the verification.

-t <secs>

Time in seconds allowed to spend in the verification. The default is infinity.

-v <number>

Specify verbosity level. Use 0 for no feedback (default), 1 for more and 2 for maximum feedback. This option can not be used in conjunction with -V.

-V <number>

Mask specifying type of information to be printed out while verifying the formulas. This allows for a finer control than -v. -V and -v cannot be used simultaneously. The mask is given as a binary number, by taking the logical or of the following binary values. One does not have to convert these numbers to decimal.

1 number of primary inputs and flip-flops

10 labeled operational graph of the formulas

100 cpu-time for the computation in each vertex

1000 cubes of the function sat for each vertex

10000 cubes of the function goalSet for each vertex

100000 vertex data structure contents after evaluation

1000000 cubes in the care set for every evaluation

10000000 size of care set for every evaluation

100000000 number of states that satisfy every sub-formula

1000000000 number of overall reachable states

10000000000 cubes for every iteration of a fixed point

100000000000 size of the BDD in each iteration in a fix-point

1000000000000 labeled operational graph in dot format

10000000000000 number of envelope states

100000000000000 number of states to be refined

1000000000000000 size of the refinement operands

10000000000000000 cubes of the refinement operands

100000000000000000 Number of latches before and after simplification

1000000000000000000 report partial progress (i.e. reach, EG(true),...)

10000000000000000000 Begin/End refinement process

100000000000000000000 Size of goal set

1000000000000000000000 cubes of the goal set

10000000000000000000000 Contents of vertex after refinement

-x

Perform the verification exactly. No approximation is done.

<ctlfile>

File containing the CTL formulas to be verified.

Related "set" options:

ctl_change_bracket <yes/no>

Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names, therefore CTL parser does the same thing. However, in some cases a user does not want to change node names in CTL parsing. Then, use this set option by giving "no". Default is "yes".

See also commands : model_check, incremental_ctl_verification

1. A. Pardo and G. Hachtel. Automatic abstraction techniques for propositional mu-calculus model checking. In 9th Conference on Computer Aided Verification (CAV'97). Springer-Verlag. Pages 12-23, 1997.

2. A. Pardo and G. Hachtel. Incremental CTL model checking using BDD subsetting. In 35th Design Automation Conference (DAC'98). pages 457-462, 1998. ]

Definition at line 264 of file absCmd.c.

{
  AbsVerificationResult_t formulaResult;
  Abs_VerificationInfo_t  *absInfo;
  AbsVertexInfo_t         *formulaPtr;
  Ctlp_Formula_t          *ctlFormula;
  AbsOptions_t            *options;
  Ntk_Network_t           *network;
  array_t                 *ctlArray;
  array_t                 *existCtlArray;
  array_t                 *fairArray;
  array_t                 *existFairArray;
  array_t                 *graphArray;
  array_t                 *resultArray;
  FILE                    *formulaFile;
  boolean                 correctSemantics;
  Fsm_Fsm_t               *fsm;
  Fsm_Fairness_t          *fairness;
  long                    cpuTime;
  int                     status;
  int                     i;
  int                     numConjuncts;

  /* Initialize some variables */
  graphArray = NIL(array_t);
  resultArray = NIL(array_t);
  options = NIL(AbsOptions_t);
  ctlArray = NIL(array_t);
  existCtlArray = NIL(array_t);
  fairArray = NIL(array_t);
  existFairArray = NIL(array_t);
  absInfo = NIL(Abs_VerificationInfo_t);

  if (bdd_get_package_name() != CUDD) {
    fprintf(vis_stderr, "** abs error : incremental_ctl_verification ");
    fprintf(vis_stderr, "is currently supported by only CUDD.\n");
    status = 1;
    goto cleanup;
  }

  error_init();

  /* Parse the options */
  options = ParseAbsCtlOptions(argc, argv);

  /* Check if there has been any error parsing the options */
  if (!options) {
    status = 1;
    goto cleanup;
  }

  /* Obtain the network */
  network = Ntk_HrcManagerReadCurrentNetwork( *hmgr );
  if ( network == NIL( Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "%s\n", error_string());
    error_init();
    status = 1;
    goto cleanup;
  }

  /* Open the file with the ctl formulas */
  formulaFile = Cmd_FileOpen(AbsOptionsReadFileName(options), "r", 
                             NIL(char *), 0);
  if (formulaFile == NIL(FILE)) {
    status = 1;
    goto cleanup;
  }

  /* Parse the formulas and close the file */
  ctlArray = Ctlp_FileParseFormulaArray(formulaFile);
  fclose(formulaFile);

  if (ctlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, 
                   "** abs error: Error while parsing CTL formulas\n");
    status = 1;
    goto cleanup;
  }

  /* Read the fairness constraints */
  fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  if (fsm != NIL(Fsm_Fsm_t)){
    fairness = Fsm_FsmReadFairnessConstraint(fsm);
    if (fairness != NIL(Fsm_Fairness_t)){
      fairArray = array_alloc(Ctlp_Formula_t *,0);
      numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(fairness, 0);
      for (i = 0; i < numConjuncts; i++) {
        ctlFormula = Fsm_FairnessReadFinallyInfFormula(fairness, 0, i);
        if ((Ctlp_FormulaReadType(ctlFormula) != Ctlp_TRUE_c) &&
            (Ctlp_FormulaReadType(ctlFormula) != Ctlp_FALSE_c)){
          array_insert_last(Ctlp_Formula_t *, fairArray, 
                            Ctlp_FormulaDup(ctlFormula));
        }
      }
      if (array_n(fairArray) == 0){
        array_free(fairArray);
        fairArray = NIL(array_t);
      }
    }
  }

  /* Verify that the formulas are semantically correct */
  correctSemantics = TRUE;

  /* Check the semantics of the temporal formulas */
  arrayForEachItem(Ctlp_Formula_t *, ctlArray, i, ctlFormula) {
    if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
      (void) fprintf(vis_stdout, 
                 "** abs error: Inconsistency detected in formula number %d.\n",
                     i);
      (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
      error_init();
      correctSemantics = FALSE;
    }
  }

  /* Check the fairness constraints */
  if (fairArray != NIL(array_t)) {
    arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlFormula) {
      if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
        (void) fprintf(vis_stdout, 
                       "** abs error: Inconsistency detected in fairness ");
        (void) fprintf(vis_stdout, "constraint number %d.\n", i);
        (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
        error_init();
        correctSemantics = FALSE;
      }
    }
  }

  /* If there is any inconsistency, do not execute the command */
  if (!correctSemantics) {
    status = 1;
    goto cleanup;
  }

  /* Replace XORs and EQs with equivalent subtrees. We insist on having
   * only monotonic operators. */
  Ctlp_FormulaArrayMakeMonotonic(ctlArray);
  Ctlp_FormulaArrayMakeMonotonic(fairArray);

  /* Translate the ctl formulas and fairness constraints to existential form */
  existCtlArray = Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
  if (fairArray != NIL(array_t)) {
    existFairArray = Ctlp_FormulaArrayConvertToExistentialFormTree(fairArray);
  }

  /* Compute the information related to the system being verified */
  absInfo = Abs_VerificationComputeInfo(network);
  if (absInfo == NIL(Abs_VerificationInfo_t)) {
    (void) fprintf(vis_stdout, "** abs error: Error computing the information required ");
    (void) fprintf(vis_stdout, "for verification.\n");
    status = 1;
    goto cleanup;
  }

  /* Store the options */
  AbsVerificationInfoSetOptions(absInfo, options);

  /* Translate the array of CTL formulas to operational graphs */
  graphArray = AbsCtlFormulaArrayTranslate(absInfo, existCtlArray, 
                                           existFairArray);

  if (graphArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, 
                   "** abs error: Error translating CTL formulas.\n");
    (void) fprintf(vis_stderr, "** abs error: Aborting command.\n");
    status = 1;
    goto cleanup;
  }

  /* Program the timeOut if pertinent */
  if (AbsOptionsReadTimeOut(options) > 0) {
    /* Set the static variables */
    absTimeOut = AbsOptionsReadTimeOut(options);
    alarmLap = util_cpu_time();

    /* Set the handler */
    (void) signal(SIGALRM, TimeOutHandle);
    (void) alarm(AbsOptionsReadTimeOut(options));
    
    /* Set the jump for the timeout */
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
                     "# ABS: Timeout occurred after %7.1f CPU seconds\n",
                     (util_cpu_time() - alarmLap)/1000.0);
      (void) fprintf(vis_stdout, "# ABS: data may be corrupted.\n");
      alarm(0);
      return 1;
    }
  }

  /* Print the graph in DOT format */
  if (AbsOptionsReadVerbosity(options) & ABS_VB_PRDOT) {
      AbsVertexPrintDot(vis_stdout, graphArray);
  }

  /* Set the cpu-time lap */
  cpuTime = util_cpu_time();

  /* Verify every formula */
  resultArray = AbsFormulaArrayVerify(absInfo, graphArray);

  /* Print out the execution time*/
  (void) fprintf(vis_stdout, "ABS: Total Verification Time: %7.1f secs\n",
                 (util_cpu_time() - cpuTime)/1000.0);
  
  /* Print out the results */
  /* RB changed this to take into account multiple initial states in negtd
     formulas */
  arrayForEachItem(AbsVerificationResult_t, resultArray, i, formulaResult) {
    (void) fprintf(vis_stdout, "# ABS: formula ");
    switch (formulaResult) {
    case trueVerification_c:
      (void) fprintf(vis_stdout, "passed --- ");
      break;
    case falseVerification_c:
      (void) fprintf(vis_stdout, "failed --- ");
      break;
    case inconclusiveVerification_c:
      (void) fprintf(vis_stdout, "undecided --- ");
    }
    if (AbsOptionsReadNegateFormula(options))
      fprintf(vis_stdout, "NOT[ ");
    Ctlp_FormulaPrint(vis_stdout, 
                      array_fetch(Ctlp_Formula_t *, ctlArray, i));
    if (AbsOptionsReadNegateFormula(options))
      fprintf(vis_stdout, " ]\n");
    else
      fprintf(vis_stdout, "\n");
  }
  
  /* Print the stats if selected by command line option */
  if (AbsOptionsReadPrintStats(options)) {
    int i;
    
    AbsStatsPrintReport(vis_stdout, AbsVerificationInfoReadStats(absInfo));
    
    (void) fprintf(vis_stdout, "# ABS: -- Command Line Options --\n");
    (void) fprintf(vis_stdout, "# ABS: ");
    for (i=0; i<argc; i++) {
      (void) fprintf(vis_stdout, "%s ", argv[i]);
    }
    (void) fprintf(vis_stdout, "\n");
  }
  
  /* Disconnect the alarm */
  alarm(0);
  
  status = 0;
  
  /* Clean up the memory and return */
  cleanup:
  if (graphArray != NIL(array_t)) {
    arrayForEachItem(AbsVertexInfo_t *, graphArray, i, formulaPtr) {
      AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), formulaPtr,
                    NIL(AbsVertexInfo_t));
    }
    array_free(graphArray);
  }
  if (resultArray != NIL(array_t)) {
    array_free(resultArray);
  }
  if (options != NIL(AbsOptions_t)) {
    AbsOptionsFree(options);
  }
  if (ctlArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(ctlArray);
  }
  if (existCtlArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(existCtlArray);
  }
  if (fairArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(fairArray);
  }
  if (existFairArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(existFairArray);
  }
  if (absInfo != NIL(Abs_VerificationInfo_t)) {
    AbsVerificationInfoFree(absInfo);
  }
  
  return status;
} /* End of CommandAbsCtl */

Here is the call graph for this function:

Here is the caller graph for this function:

static AbsOptions_t * ParseAbsCtlOptions	(	int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Parses the options given to the incremental_ctl_verification command and stores them into a structure.]

SideEffects []

SeeAlso [CommandAbsCtl]

Definition at line 563 of file absCmd.c.

{
  AbsOptions_t *result;
  char *fileName;
  boolean reachability;
  boolean envelope;
  boolean exact;
  boolean printStats;
  boolean minimizeIterate;
  boolean negateFormula;
  boolean partApprox;
  boolean DFlag, eFlag, nFlag, pFlag, sFlag, tFlag, vFlag, xFlag;
  long verbosity;
  int intVerbosity;
  int timeOut;
  int dcValue;
  int c;
  unsigned int i;

  /* Default Options */
  DFlag = eFlag = nFlag = pFlag = sFlag = tFlag = FALSE;
  vFlag = xFlag = FALSE;
  reachability = FALSE;
  envelope = FALSE;
  exact = FALSE;
  printStats = FALSE;
  minimizeIterate = FALSE;
  negateFormula = FALSE;
  partApprox = FALSE;
  verbosity = 0;
  intVerbosity = 0;
  timeOut = -1;
  dcValue = 0;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "D:ehnpst:v:V:x")) != EOF) {
    switch(c) {
      case 'D':
        dcValue = atoi(util_optarg);
        if (DFlag || (dcValue < 0) || (dcValue > 2)) {
          goto usage;
        }
        if (dcValue > 0) {
          reachability = TRUE;
        }
        if (dcValue > 1) {
          minimizeIterate = TRUE;
        }
        DFlag = TRUE;
        break;
      case 'e':
        if (eFlag) {
          goto usage;
        }
        envelope = TRUE;
        eFlag = TRUE;
        break;
      case 'h':
        goto usage;
      case 'n':
        if (nFlag) {
          goto usage;
        }
        negateFormula = TRUE;
        nFlag = TRUE;
        break;
      case 'p':
        if (pFlag) {
          goto usage;
        }
        partApprox = TRUE;
        pFlag = TRUE;
        break;
      case 's':
        if (sFlag) {
          goto usage;
        }
        printStats = TRUE;
        sFlag = TRUE;
        break;
      case 't':
        if (tFlag) {
          goto usage;
        }
        timeOut = atoi(util_optarg);
        tFlag = TRUE;
        break;
      case 'v':
        if (vFlag) {
          goto usage;
        }
        intVerbosity =  atoi(util_optarg);
        if (intVerbosity == 1){
          verbosity = 131849;
        }else if (intVerbosity == 2){
          verbosity = 8388607;
        }else{
          verbosity = 0;
        }
        vFlag = TRUE;
        break;
      case 'V':
        if (vFlag) {
          goto usage;
        }
        for(i=0;i<strlen(util_optarg)-1;i++){
          if (util_optarg[i] != '0' && util_optarg[i] != '1'){
             goto usage;
          }
        }
        verbosity =  strtol(util_optarg, NIL(char *), 2);
        vFlag = TRUE;
        break;
      case 'x':
        if (xFlag) {
          goto usage;
        }
        exact = TRUE;
        xFlag = TRUE;
        break;
      default:
        goto usage;
    }
  }

  /* Check if there is still one parameter left */
  if (argc - util_optind != 1) {
    goto usage;
  }

  /* Obtain the filename from the end of the command line */
  fileName = util_strsav(argv[util_optind]);
  
  /* Store the options  */
  result = AbsOptionsInitialize();
  
  AbsOptionsSetVerbosity(result, verbosity);
  AbsOptionsSetTimeOut(result, timeOut);
  AbsOptionsSetReachability(result, reachability);
  AbsOptionsSetEnvelope(result, envelope);
  AbsOptionsSetFileName(result, fileName);
  AbsOptionsSetExact(result, exact);
  AbsOptionsSetPrintStats(result, printStats);
  AbsOptionsSetMinimizeIterate(result, minimizeIterate);
  AbsOptionsSetNegateFormula(result, negateFormula);
  AbsOptionsSetPartApprox(result, partApprox);

  return result;

 usage:
  fprintf(vis_stderr,"usage: incremental_ctl_verification [-D <number>] [-e] [-h] [-n] [-s]\n");
  fprintf(vis_stderr,"[-t <seconds>] [-v <number>] [-V <number>] [-x] <ctlfile>\n");
  fprintf(vis_stderr,"\n");
  fprintf(vis_stderr,"Command options:\n");
  fprintf(vis_stderr,"-D <number>\n");
  fprintf(vis_stderr,"   Specify extent to which don't cares are used to simplify\n");
  fprintf(vis_stderr,"   the MDDs.\n");
  fprintf(vis_stderr,"   0: No Don't Cares used.\n");
  fprintf(vis_stderr,"   1: Use reachability information to compute the don't-care\n");
  fprintf(vis_stderr,"     set. Reachability is performed by formula. This is different from\n");
  fprintf(vis_stderr,"     mc, where reachability is performed only once.\n");
  fprintf(vis_stderr,"   2: Use reachability information, and minimize the transition relation\n");
  fprintf(vis_stderr,"     with respect to the `frontier set' (aggresive minimization).\n");
  fprintf(vis_stderr,"-e\n");
  fprintf(vis_stderr,"   Compute the set of fair states (those satisfying the formula\n");
  fprintf(vis_stderr,"   EGfair TRUE) before the verification process and use the result\n");
  fprintf(vis_stderr,"   as care set.\n");
  fprintf(vis_stderr,"-h\n");
  fprintf(vis_stderr,"   Print the command usage.\n");
  fprintf(vis_stderr,"-n\n");
  fprintf(vis_stderr,"   Try to prove the negation of every formula\n");
  fprintf(vis_stderr,"-s\n");
  fprintf(vis_stderr,"   Print a summary of statistics after the verification.\n");
  fprintf(vis_stderr,"-t <secs>\n");
  fprintf(vis_stderr,"   Time in seconds allowed to spend in the verification.\n");
  fprintf(vis_stderr,"-v <number>\n");
  fprintf(vis_stderr,"   Specify verbosity level. Use 0 for no feedback (default), 1 for\n");
  fprintf(vis_stderr,"   more and 2 for maximum feedback. This option can not be used\n");
  fprintf(vis_stderr,"   in conjunction with -V.\n");
  fprintf(vis_stderr,"-V <number>\n");
  fprintf(vis_stderr,"   Mask specifying type of information to be printed out while\n");
  fprintf(vis_stderr,"   verifying the formulas. See the help page.\n");
  fprintf(vis_stderr,"-x\n");
  fprintf(vis_stderr,"   Perform the verification exactly. No approximation is done.\n");
  fprintf(vis_stderr,"<ctlfile>\n");
  fprintf(vis_stderr,"   File containing the CTL formulas to be verified.\n");
  return NIL(AbsOptions_t);
} /* End of ParseAbsCtlOptions */

Here is the call graph for this function:

Here is the caller graph for this function:

static void TimeOutHandle

(

int

sigType

)

[static]

Function********************************************************************

Synopsis [Handle function for timeout.]

Description [This function is called when the process receives a signal of type alarm. Since alarm is set with elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire later and check if the CPU limit has been reached.]

SideEffects []

Definition at line 767 of file absCmd.c.

{
  long seconds;

  seconds = (util_cpu_time() - alarmLap) / 1000;
  
  if (seconds < absTimeOut) {
    unsigned slack;

    slack = absTimeOut - seconds;
    (void) signal(SIGALRM, TimeOutHandle);
    (void) alarm(slack);
  }
  else {
    longjmp(timeOutEnv, 1);
  }
} /* End of TimeOutHandle */

Here is the caller graph for this function:

---

Variable Documentation

int absTimeOut [static]

Definition at line 37 of file absCmd.c.

long alarmLap [static]

Definition at line 38 of file absCmd.c.

jmp_buf timeOutEnv [static]

Definition at line 36 of file absCmd.c.

char rcsid [] UNUSED = "$Id: absCmd.c,v 1.37 2002/09/08 22:13:50 fabio Exp $" [static]

CFile***********************************************************************

FileName [absCmd.c]

PackageName [abs]

Synopsis [Encapsulation for the incremental_ctl_verification command.]

Author [Abelardo Pardo <abel@vlsi.colorado.edu>]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 19 of file absCmd.c.