src/clause.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   6 ** This program is free software; you can redistribute it and/or modify it
   7 ** under the terms of the GNU General Public License as published by the
   8 ** Free Software Foundation; either version 2 of the License, or (at your
   9 ** option) any later version.
  10 **
  11 ** This program is distributed in the hope that it will be useful, but
  12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14 ** General Public License for more details.
  15 **
  16 ** The GNU General Public License is available from http://www.gnu.org/ or
  17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  18 ** MA 02111-1307, USA.
  19 **
  20 ** For information on splint: info@splint.org
  21 ** To report a bug: splint-bug@splint.org
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** clause.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 cstring
  32 clause_unparse (clause cl)
  33 {
  34   switch (cl)
  35     {
  36     case TRUECLAUSE:   return (cstring_makeLiteralTemp ("true"));
  37     case FALSECLAUSE:  return (cstring_makeLiteralTemp ("false"));
  38     case ANDCLAUSE:    return (cstring_makeLiteralTemp ("and"));
  39     case ORCLAUSE:     return (cstring_makeLiteralTemp ("or"));
  40     case DOWHILECLAUSE:  return (cstring_makeLiteralTemp ("do ... while"));
  41     case WHILECLAUSE:  return (cstring_makeLiteralTemp ("while"));
  42     case ITERCLAUSE:   return (cstring_makeLiteralTemp ("iter"));
  43     case FORCLAUSE:    return (cstring_makeLiteralTemp ("for"));
  44     case CASECLAUSE:   return (cstring_makeLiteralTemp ("case"));
  45     case NOCLAUSE:     return (cstring_makeLiteralTemp ("none"));
  46     case SWITCHCLAUSE: return (cstring_makeLiteralTemp ("switch"));
  47     case CONDCLAUSE:   return (cstring_makeLiteralTemp ("cond"));
  48     case TRUEEXITCLAUSE: return (cstring_makeLiteralTemp ("trueexit"));
  49     case FALSEEXITCLAUSE: return (cstring_makeLiteralTemp ("falseexit"));
  50     }
  51
  52   BADBRANCHRET (cstring_undefined);
  53 }
  54
  55 cstring
  56 clause_nameTaken (clause cl)
  57 {
  58   switch (cl)
  59     {
  60     case TRUECLAUSE:   return (cstring_makeLiteralTemp ("in true branch"));
  61     case FALSECLAUSE:  return (cstring_makeLiteralTemp ("in true branch"));
  62     case ANDCLAUSE:    return (cstring_makeLiteralTemp ("in first and clause"));
  63     case ORCLAUSE:     return (cstring_makeLiteralTemp ("in first or clause"));
  64     case DOWHILECLAUSE:  return (cstring_makeLiteralTemp ("in do ... while body"));
  65     case WHILECLAUSE:  return (cstring_makeLiteralTemp ("in while body"));
  66     case ITERCLAUSE:   return (cstring_makeLiteralTemp ("in iter body"));
  67     case FORCLAUSE:    return (cstring_makeLiteralTemp ("in for body"));
  68     case CASECLAUSE:   return (cstring_makeLiteralTemp ("in one case"));
  69     case NOCLAUSE:     return (cstring_makeLiteralTemp ("in some clause"));
  70     case SWITCHCLAUSE: return (cstring_makeLiteralTemp ("in one possible execution"));
  71     case CONDCLAUSE:   return (cstring_makeLiteralTemp ("in true condition"));
  72     case TRUEEXITCLAUSE: return (cstring_makeLiteralTemp ("in trueexit"));
  73     case FALSEEXITCLAUSE: return (cstring_makeLiteralTemp ("in falseexit"));
  74     }
  75
  76   BADBRANCHRET (cstring_undefined);
  77 }
  78
  79 cstring
  80 clause_nameAlternate (clause cl)
  81 {
  82   switch (cl)
  83     {
  84     case TRUECLAUSE:   return (cstring_makeLiteralTemp ("in continuation"));
  85     case FALSECLAUSE:  return (cstring_makeLiteralTemp ("in false branch"));
  86     case ANDCLAUSE:    return (cstring_makeLiteralTemp ("in second and clause"));
  87     case ORCLAUSE:     return (cstring_makeLiteralTemp ("in second or clause"));
  88     case DOWHILECLAUSE:  return (cstring_makeLiteralTemp ("if loop is not taken"));
  89     case WHILECLAUSE:  return (cstring_makeLiteralTemp ("if loop is not taken"));
  90     case ITERCLAUSE:   return (cstring_makeLiteralTemp ("if iter body does not execute"));
  91     case FORCLAUSE:    return (cstring_makeLiteralTemp ("if for loop body does not execute"));
  92     case CASECLAUSE:   return (cstring_makeLiteralTemp ("in other case"));
  93     case NOCLAUSE:
  94     case SWITCHCLAUSE: return (cstring_makeLiteralTemp ("in other possible execution"));
  95     case CONDCLAUSE:   return (cstring_makeLiteralTemp ("in false condition"));
  96     case TRUEEXITCLAUSE: return (cstring_makeLiteralTemp ("in trueexit"));
  97     case FALSEEXITCLAUSE: return (cstring_makeLiteralTemp ("in falseexit"));
  98     }
  99
 100   BADBRANCHRET (cstring_undefined);
 101 }
 102
 103 cstring clause_nameFlip (clause cl, bool flip)
 104 {
 105   if (flip)
 106     {
 107       return clause_nameAlternate (cl);
 108     }
 109   else
 110     {
 111       return clause_nameTaken (cl);
 112     }
 113 }
 114
 115 bool clause_isBreakable (clause cl)
 116 {
 117   return (cl == SWITCHCLAUSE
 118           || cl == WHILECLAUSE
 119           || cl == DOWHILECLAUSE
 120           || cl == FORCLAUSE
 121           || cl == ITERCLAUSE);
 122 }
 123
 124 bool clause_isLoop (clause cl)
 125 {
 126   return (cl == WHILECLAUSE
 127           || cl == FORCLAUSE
 128           || cl == ITERCLAUSE
 129           || cl == DOWHILECLAUSE);
 130 }
 131
 132 bool clause_isConditional (clause cl)
 133 {
 134   return (   cl == TRUECLAUSE
 135           || cl == FALSECLAUSE
 136           || cl == WHILECLAUSE
 137           || cl == FORCLAUSE
 138           || cl == SWITCHCLAUSE
 139           || cl == ITERCLAUSE);
 140 }
 141
 142 bool clause_isSwitch (clause cl)
 143 {
 144   return (cl == SWITCHCLAUSE);
 145 }
 146
 147 bool clause_isCase (clause cl)
 148 {
 149   return (cl == CASECLAUSE);
 150 }
 151
 152 bool clause_isNone (clause cl)
 153 {
 154   return (cl == NOCLAUSE);
 155 }