Linux Driver Verification

Pavel Shved 2010-01-20 16:40:05 MSK

   struct l_struct_2E_mutex *blast_must_tmp__3;
   unsigned int blast_must_tmp__4;
   struct l_struct_2E_mutex *blast_must_tmp__5;

 ...

   blast_must_tmp__3 = *(&llvm_cbe_aaa);
   blast_must_tmp__4 = *((&blast_must_tmp__3->field0));
   blast_must_tmp__5 = *(&llvm_cbe_aaa);
   blast_must_tmp__6 = (&blast_must_tmp__5->field1);
   if ((blast_must_tmp__4 != 0u)) {
     goto llvm_cbe_bb;
   } else {
     goto llvm_cbe_bb1;
   }

 llvm_cbe_bb:
   *blast_must_tmp__6 = 10u;
   goto llvm_cbe_bb2;

 llvm_cbe_bb1:
   *blast_must_tmp__6 = 20u;
   goto llvm_cbe_bb2;

I identified the problem. The thing is that in current BLAST must-aliasing infrastructure expression "*blast_must_tmp__6" is a must-alias, because it is based on an identifier with special must-prefix. The thing is that in this case the "tag" expression is mere "blast_must_tmp__6", but in other cases it may be "*(mem_3->xxx)". The method to distinguish them is needed.