[C-safe-secure-studygroup] MISRA rule 13.2 questions

[Fulvio Baccaglini]

I believe that with respect to other standards MISRA C is trying harder
to have rules based on structural analysis (decidable) rather than
dataflow analysis (undecidable), but that is not always possible or
convenient.

Rule 13.2 is actually categorised as undecidable, suggesting that
dataflow analysis has a role, but I believe that there could be a case
to restrict the rule further and make it decidable.

Here is an example that is more borderline:

~~~~>

int v = 5;

int f1 (void) { return 3; }

int f2 (void) { v = 2; return v; }

int f (int x)

{

typedef int (* F) (void);

F f3 = (x > 0 ? f1 : f2);

return v + f3 (); // is Rule 13.2 violated?

}

int main (void)

{

return f (5);

}

<~~~~

Based on dataflow analysis the rule would not be violated,  but based on
structural analysis it would have to be.

Fulvio

On 04/05/18 14:15, Robert Seacord wrote:
> I guess that makes sense.  MISRA rules are all about structural
> analysis and don't consider data flow at all, right?
>
> rCs
>
> On Fri, May 4, 2018 at 8:40 AM, Fulvio Baccaglini
> <fulvio_baccaglini at prqa.com <mailto:fulvio_baccaglini at prqa.com>> wrote:
>
>     Hi,
>
>     The official answer has now been posted:
>
>     https://www.misra.org.uk/forum/viewtopic.php?t=1720
>     <https://www.misra.org.uk/forum/viewtopic.php?t=1720>
>
>     Fulvio
>
>
>     On 23/03/18 12:53, Clive Pygott wrote:
>>     Hi
>>
>>     I've been speaking with a couple of member of the MISRA C
>>     committee, including the person that looks after the bulletin
>>     board, and whilst Robert's question will get answered officially
>>     eventually (after its been discussed at a MISRA meeting,
>>     hopefully in April) - it will take some time, and may just say
>>     'Yes, your example does violate this rule'.  So here is my
>>     UNOFFICIAL understanding of the answers to our implied questions:
>>
>>     1)  We are right to assume that an amplification takes precedence
>>     over the headline rule
>>
>>     2)  The reason why the amplification includes 'full expressions'
>>     and not just between sequence points can be illustrated by:
>>
>>                 y  =  x++  +  foo();
>>
>>     where foo includes an assignment to x.  
>>
>>     There is a sequence point at the start of the execution of foo()  
>>     -  see C11  6.5.2.2 #10.  
>>
>>     As I interpret it, the compiler can choose to evaluate  x++  and 
>>     foo()  in either order. If initially  x  has the value  x0, and 
>>     foo()  will assign it  fx(x)  and foo() returns  fr(x), then:
>>
>>       * if  x++  is evaluated first, the assignment of  x0+1 back to
>>         x  has to be performed before the execution of foo starts, 
>>         so  x finishes up as fx(x0+1) and y  ==  x0 +  fr(x0+1)
>>       * if foo() is evaluated first, x will be assigned fx(x0) before
>>         the increment is performed,   so  x finishes up as  fx(x0)+1 
>>         and  y ==  fx(x0) +  fr(x0)
>>
>>     For our purposes, I think we can permit the sorts of expressions
>>     that Martin was arguing for by making an exception that 
>>     'sub-expressions separated by  &&  ||  the comma operator ....
>>     may be treated as separate "full expressions" for the purposes of
>>     this rule'
>>
>>     3) I asked the question 'does this apply to changes in
>>     rounding in floating point calculations due to the order that
>>     sub-expressions are evaluated?'  They're still thinking about
>>     that - and also what happens to an integer expression that may
>>     overflow or not depending upon the order of evaluation
>>
>>     Hope this clarifies things
>>
>>     Thanks to Liz Whiting and Chris Tapp for their help
>>
>>         Clive
>>
>>
>>
>>
>>
>>     _______________________________________________
>>     C-safe-secure-studygroup mailing list
>>     C-safe-secure-studygroup at lists.trustable.io
>>     <mailto:C-safe-secure-studygroup at lists.trustable.io>
>>     https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup
>>     <https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup>
>
>
>
>     ------------------------------------------------------------------------
>     This email has been scanned for email related threats and
>     delivered safely by Mimecast.
>     For more information please visit http://www.mimecast.com
>     ------------------------------------------------------------------------
>
>     _______________________________________________
>     C-safe-secure-studygroup mailing list
>     C-safe-secure-studygroup at lists.trustable.io
>     <mailto:C-safe-secure-studygroup at lists.trustable.io>
>     https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup
>     <https://lists.trustable.io/cgi-bin/mailman/listinfo/c-safe-secure-studygroup>
>
>
>
>
> _______________________________________________
> 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
---------------------------------------------------------------------------------------
 This email has been scanned for email related threats and delivered safely by Mimecast.
 For more information please visit http://www.mimecast.com
---------------------------------------------------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.trustable.io/pipermail/c-safe-secure-studygroup/attachments/20180504/f1a8d0d8/attachment.html>