[PATCH] Division by zero

[Anders Rönnholm]

Thanks for your comments. Here's a new patch.

//Anders

________________________________________
Från: Jordan Rose [jordan_rose at apple.com]
Skickat: den 19 juni 2014 18:17
Till: Anders Rönnholm
Cc: cfe-commits at cs.uiuc.edu; Daniel Marjamäki
Ämne: Re: [PATCH] Division by zero

On Jun 18, 2014, at 7:30 , Anders Rönnholm <Anders.Ronnholm at evidente.se> wrote:

> Changes according to comments.
>
> I'm pretty sure PVS-Studio does not have this checker, this bug has been seen in production code.


Oops, noticing more things:

+  const ExplodedNode *N = C.getPredecessor();
+  while (N) {
+    ProgramStateRef State = N->getState();
+
+    // Find the most recent expression bound to the symbol in the current
+    // context.
+    if (const MemRegion *MR = C.getLocationRegionIfPostStore(N)) {
+      SVal Val = State->getSVal(MR);
+      if (Val == S) {
+        Optional<DefinedSVal> DSV = Val.getAs<DefinedSVal>();
+        if (!C.getConstraintManager().assume(State, *DSV, false))
+          return true;
+      }
+    }
+    N = N->pred_empty() ? nullptr : *(N->pred_begin());
+  }

Why are you looking for the last time a value was stored rather than just asking for the value in the current state?

if (Optional<Loc> L = S.getAs<Loc>()) {
  SVal V = State->getSVal(L) // or getRawSVal if you don't want a symbol constrained to 0 to be simplified to 0.
  // ...


+    if (Optional<KnownSVal> V = Val.getAs<KnownSVal>()) {

Because you needed a symbol already to get this far, you can skip this step. Or assert it.


+void TestAfterDivZeroChecker::checkPreStmt(const BinaryOperator *B,
+                                   CheckerContext &C) const {

Strange alignment here. If the second line doesn't fit, just indent it twice from the start of the function...don't try to right-align it.


+    if (!B->getRHS()->getType()->isScalarType())
+      return;

Dividing by a floating-point 0 is well-defined, so this should be a more specific check.

Jordan
-------------- next part --------------
A non-text attachment was scrubbed...
Name: divzero2.diff
Type: text/x-patch
Size: 18445 bytes
Desc: divzero2.diff
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140624/1757babe/attachment.bin>