[C-safe-secure-studygroup] On MISRA C:2012 Rule 14.1

Clive Pygott clivepygott at gmail.com
Wed Apr 18 08:38:51 BST 2018


My thought on this is that the example Martin suggests shouldn't be
implemented as a for loop. I'd expect it to be implemented as a while loop

             void converge_on (double  requiredPrecision)
                    { double error =  requiredPrecision +1.0;  // anything
>  requiredPrecision
                      while (error > requiredPrecision)
                                error = iterate();;
                    }

    Clive

On Wed, Apr 18, 2018 at 6:31 AM, Roberto Bagnara <bagnara at cs.unipr.it>
wrote:

> On 18/04/2018 04:15, Martin Sebor wrote:
> > On 04/17/2018 05:54 AM, Roberto Bagnara wrote:
> >> MISRA C:2012 Rule 14.1:
> >> A loop counter shall not have essentially floating type
> >>
> >> This is a required rule.  The aim is to avoid that the complication and
> non-determinism of floating-point computations is reflected into the number
> of times loops are executed.
> >>
> >> By "complication" I mean that the limitations of floating-point types
> are not well understood by many programmers;  for instance many do not know
> that 0.1 is not exactly representable as a binary floating-point number and
> many of those who do know would not be able to say how it will be rounded
> and upon what conditions.
> >>
> >> By "non-determinism" I mean that, even if the C implementation at hand
> is based on, say, IEEE~754, obtaining deterministic behavior (that is,
> behavior that is reproducible on different systems, even using the very
> same compiler) is a challenging task.
> >>
> >> Being able to reliably predict the number of iterations of a
> numerically-controlled loop is important both for safety and security: for
> such loops, integer numbers should be used.
> >
> > Not to dispute the validity of the rule in the (I suspect rare)
> > instances when a floating type is misused for the counter but
> > what about the cases where the number of iterations isn't known
> > ahead of time and the loop terminates only when the computation
> > converges on some predetermined floating result?  How does one
> > write a loop like that so it doesn't violate the rule?
> >
> > For instance:
> >
> >   void converge_on (double z)
> >   {
> >     for (double x = 0; x < z; )
> >       x = foo (x);
> >   }
> >
> > Based on the definitions in 8.14 Control statement expressions,
> > it seems impossible to write a loop like that.  The concern that
> > the loop may not terminate is no different than with a scalar
> > counter:
> >
> >   void converge_on (int z)
> >   {
> >     for (int x = 0; x < z; )
> >       x = foo (x);
> >   }
> >
> > I wonder if it might be worthwhile to distill the underlying
> > problem that rule 14.1 is trying to prevent and formulate
> > a rule aimed at avoiding it instead.
>
> Sorry, I should have clarified that "loop counter" is a technical
> term in MISRA C: it is defined in Section 8.14.  The overall idea
> is to be able to express determinate iteration in MISRA C, that is,
> iteration whereby the maximum number of iterations can be known
> before the first iteration begins.  In Pascal, the FOR construct
> plays this role;  in MISRA C we have well-formed for loops.
> For indeterminate iteration you can use while or do-while loops,
> or you can deviate the relevant 14.* rules if you want to use
> for loops for that purpose as well.
>
> If you prefer semantic restrictions, you may consider
> Rule 3 of NASA JPL Institutional Coding Standard
> for the C Programming Language:
>
> Rule 3 (loop bounds)
> All loops shall have a statically determinable upper-bound on the
> maximum number of loop iterations. It shall be possible for a static
> compliance checking tool to affirm the existence of the bound. An
> exception is allowed for the use of a single non-terminating loop per task
> or thread where requests are received and processed. Such a server loop
> shall be annotated with the C comment: /* @non-terminating@ */.
> [Power of Ten Rule 2]
>
>
> --
>      Prof. Roberto Bagnara
>
> Applied Formal Methods Laboratory - University of Parma, Italy
> mailto:bagnara at cs.unipr.it
>                               BUGSENG srl - http://bugseng.com
>                               mailto:roberto.bagnara at bugseng.com
>
>
> _______________________________________________
> C-safe-secure-studygroup mailing list
> C-safe-secure-studygroup at lists.trustable.io
> https://lists.trustable.io/cgi-bin/mailman/listinfo/c-
> safe-secure-studygroup
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20180418/97ae0d2e/attachment-0001.html>


More information about the C-safe-secure-studygroup mailing list