locked
Finding Dead Code Branches with Static Contracts Checker ? RRS feed

  • Question

  • Hi,
    Wouldn't it be possible to use the static Checker to find Codebranches (If branches, or other) witch will never be executed ?
    I mean, isn't that smilar to check the constrains/asserts ?
    Friday, February 6, 2009 7:17 PM

Answers

  • Hi Alexander,
      Debug.Assert should do the work too.

    Ciao,
    f
    Wednesday, March 11, 2009 10:37 PM
    Moderator

All replies

  • Hi Alexander,
      in some cases, the static checker can prove that a given assertion is not reachable by any execution (i.e. it is dead code).
    So for instance for the code snippet
    1 public Class1(int initial){  
    2 Contract.Requires(initial >= 0);  
    3 if (initial < -3)  
    4 {  
    5  Contract.Assert(false);  
    6 }  
    7 this.balance = initial;  
    8 }  
    9  


    the static checker will report that the assertion at line 5 is unreached (as initial cannot be >= 0 and < -3 at the same time).

    However, we do not have, at the moment, any automatic way of inserting those assertions, so to check reachability of each branch.

    Hope it helps,
    Francesco.

    Tuesday, February 10, 2009 1:43 AM
    Moderator
  • Hi Francesco,
    does the static checker only check, if you use Contract.Requires and Contract.Assert, or dos it alos check if you set the prereqires with 'if xxx throw yyy' and Debug.Assert(false) ?
    Wednesday, February 11, 2009 9:39 AM
  • Hi Alexander,
      the "if (...) throw ..." + Contract.Assert construct should do the job too.
    In fact, the static checker when trying to prove assertions, first checks if it is reachable by any execution.

    f
    Tuesday, February 17, 2009 10:37 AM
    Moderator
  • Hi Francesco,
    What I wanted to know, is, do you need Contract.Assert or does Debug.Assert work too ?
    Tuesday, February 17, 2009 1:14 PM
  • Hi Alexander,
      Debug.Assert should do the work too.

    Ciao,
    f
    Wednesday, March 11, 2009 10:37 PM
    Moderator