Builder integration-explicitAnalysis Build #270

Results:

Warnings

SourceStamp:

BuildSlave:

Reason:

scheduler

Steps and Logfiles:

1. svn update ( 16 secs )
   1. stdio
2. Local mods Ran ( 0 secs )
   1. stdio
3. shell 'ant' ( 4 secs )
   1. stdio
4. shell_1 benchmark.py ( 22 mins, 13 secs )
   1. stdio
5. setproperty 5 properties set ( 0 secs )
   1. stdio
   2. property changes
6. shell_2 Cleanup results ( 0 secs )
   1. stdio
7. shell_3 regression.py ( 0 secs )
   1. stdio
8. shell_4 table_generator.py ( 0 secs )
   1. stdio
9. MasterShellCommand Ran ( 24 secs )
   1. stdio
10. shell_5 Prepare results 2 ( 0 secs )
    1. stdio
11. Transfer results uploading results ( 0 secs )
    1. - no logs -
12. Final result Final result ( 0 secs )
    1. - no logs -
    2. DIFF
    3. TABLE

Build Properties:

Blamelist:

1. pwendler

Timing:

Resubmit Build:

All Changes:

1. Change #359

   Changed by	pwendler
   Changed at	Mon 20 Feb 2012 14:11:31
   Repository	https://svn.sosy-lab.org/software/cpachecker/trunk
   Revision	5668

   Comments

   Change strategy of handling dead code.
   
   There are two sets of states for the CFA of a given function:
   - the set of states reachable from the entry node
   - the set of states created during creation of the CFA
   
   Previously, we wanted to defend against bugs in the cfa builder
   and thus tried to ensure that these two sets are always equals.
   This meant, during CFA creation we needed to detect all cases of dead
   code, because otherwise the first set of nodes would have been smaller.
   
   This strategy is quite difficult and has already caused some problems
   for users (whenever they encounter a new type of dead code we had not
   handled, there was an AssertionError).
   
   Now in bug #71 there is the following code (simplified):
   
   void foo() {
     return;
     while (1) {
       label: ;
     }
   }
   
   The whole loop is dead code, but only because the label is never
   mentioned in a goto clause. This case of dead code is very difficult to
   catch.
   
   Additionally, bug #70 shows that there is a performance problem with our
   detection of unreachable labels (the function mentioned in this bug
   report is used for this).
   
   Thus now I change the strategy and don't care anymore if the two sets
   above differ. Instead after creating a function CFA, I use the set of
   reachable states as the relevant set and delete all the other nodes.
   Thus we don't need to handle all cases of dead code explicitly.
   
   (fixes #71)
   (see #70)

   Changed files

   • src/org/sosy_lab/cpachecker/cfa/parser/eclipse/CFAFunctionBuilder.java