]> andersk Git - splint.git/blobdiff - src/exprChecks.c
EXtensive code clean up. Almost passes LCLint.
[splint.git] / src / exprChecks.c
index cbeeef85c81a31abbcf347642164a04553d928f3..72be47c0fa520eebd45d6d003ffe6fdf9cb0315d 100644 (file)
@@ -65,7 +65,7 @@ exprNode_checkStatement (exprNode e)
        { 
          if (ctype_isKnown (e->typ))
            {
-             if (ctype_isBool (ctype_realishType (e->typ)))
+             if (ctype_isManifestBool (ctype_realishType (e->typ)))
                {
                  hasError = optgenerror 
                    (FLG_RETVALBOOL,
@@ -648,20 +648,40 @@ void exprNode_checkMacroBody (/*@only@*/ exprNode e)
 
          uentry_setDefined (hdr, e->loc);
          
-         if (!(exprNode_matchType (ctype_realType (t), e)))
+         if (!(exprNode_matchType (t, e)))
            {
-             if (optgenerror 
-                 (FLG_INCONDEFS,
-                  message
-                  ("Constant %q specified as %s, but defined as %s: %s",
-                   uentry_getName (hdr),
-                   ctype_unparse (t),
-                   ctype_unparse (e->typ),
-                   exprNode_unparse (e)),
-                  e->loc))
+             cstring uname = uentry_getName (hdr);
+
+             if (cstring_equal (uname, context_getTrueName ())
+                 || cstring_equal (uname, context_getFalseName ()))
                {
-                 uentry_showWhereSpecified (hdr);
+                 /* 
+                 ** We need to do something special to allow FALSE and TRUE
+                 ** to be defined without reporting errors.  This is a tad
+                 ** bogus, but otherwise lots of things would break.
+                 */
+
+
+                 llassert (ctype_isManifestBool (t));
+                 /* Should also check type of e is a reasonable (?) bool type. */
                }
+             else 
+               {
+                 if (optgenerror 
+                     (FLG_INCONDEFS,
+                      message
+                      ("Constant %q specified as %s, but defined as %s: %s",
+                       uentry_getName (hdr),
+                       ctype_unparse (t),
+                       ctype_unparse (e->typ),
+                       exprNode_unparse (e)),
+                      e->loc))
+                   {
+                     uentry_showWhereSpecified (hdr);
+                   }
+               }
+
+             cstring_free (uname);
            }
          else
            {
@@ -863,6 +883,9 @@ void exprNode_checkFunctionBody (exprNode body)
                }
            }
        }
+
+      /* drl added call*/
+      exprNode_checkFunction (context_getHeader (), body);
       
       if (!checkret)
        {
@@ -870,11 +893,85 @@ void exprNode_checkFunctionBody (exprNode body)
        }
     }
 }
-      
+/*drl modified */
+
+extern constraintList implicitFcnConstraints;
+
 void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
 {
-  exprNode_free (body);
-  }
+  constraintList c, t;
+ constraintList c2, fix;
+
+ //  return;
+
+ //  context_setFlag(FLG_ORCONSTRAINT, TRUE);
+  exprNode_generateConstraints (body);
+  
+  c =   uentry_getFcnPreconditions (ue);
+  DPRINTF(("function constraints\n"));
+  DPRINTF (("\n\n\n\n\n\n\n"));
+
+  context_enterInnerContext ();
+  
+   if (c)
+     {
+
+       DPRINTF ( (message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
+       
+       t = reflectChanges (body->requiresConstraints, constraintList_copy (c) );
+       body->requiresConstraints = constraintList_copy (t);
+
+       c2  =  constraintList_copy (c);
+       fix =  constraintList_makeFixedArrayConstraints (body->uses);
+       c2  =  reflectChanges (c2, constraintList_copy(fix) );
+       if ( context_getFlag (FLG_ORCONSTRAINT) )
+        {
+          t = reflectChangesOr (body->requiresConstraints, constraintList_copy (c2) );
+        }
+       else
+        {
+          t = reflectChanges (body->requiresConstraints, constraintList_copy (c2) );
+        }
+       body->requiresConstraints = constraintList_copy (t);
+       
+       DPRINTF ( (message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
+       t = constraintList_mergeEnsures (c, body->ensuresConstraints);
+
+   body->ensuresConstraints = constraintList_copy (t);
+   
+   DPRINTF ( (message ("The body has the ensures constraints: %s", constraintList_printDetailed (t) ) ) );
+     }
+
+   if (c)
+     {
+       DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
+     }
+   else
+     {
+       DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
+     }
+
+   if ( implicitFcnConstraints)
+     {
+          if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+             {
+               body->requiresConstraints = reflectChanges (body->requiresConstraints, constraintList_copy (implicitFcnConstraints) );
+             }
+     }
+   
+   constraintList_printError(body->requiresConstraints, g_currentloc);
+   constraintList_printError(body->ensuresConstraints, g_currentloc);
+   
+   //   ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc);
+
+   //   ConPrint (message ("LCLint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
+  
+     //  printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
+     //   printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
+   
+   context_exitInnerPlain();
+   /* exprNode_free (body); */
+}
 
 void exprChecks_checkEmptyMacroBody (void)
 {
This page took 0.039114 seconds and 4 git commands to generate.