File tree Expand file tree Collapse file tree 4 files changed +18
-1
lines changed 
regression/jbmc/nil-names Expand file tree Collapse file tree 4 files changed +18
-1
lines changed Original file line number Diff line number Diff line change 1+ public  class  nil  {
2+ 
3+   int  nil ;
4+ 
5+   public  int  getNil () {
6+     return  nil ;
7+   }
8+ 
9+ }
Original file line number Diff line number Diff line change 1+ CORE
2+ nil.class
3+ --function nil.getNil
4+ ^VERIFICATION SUCCESSFUL$
5+ ^EXIT=0$
6+ ^SIGNAL=0$
7+ --
8+ std::bad_cast
Original file line number Diff line number Diff line change @@ -352,7 +352,7 @@ class fieldref_exprt : public exprt
352352template  <>
353353inline  bool  can_cast_expr<fieldref_exprt>(const  exprt &base)
354354{
355-   return  base.get (ID_class) != ID_nil  && base.get (ID_component_name) != ID_nil ;
355+   return  ! base.get (ID_class). empty ()  && ! base.get (ID_component_name). empty () ;
356356}
357357
358358#endif //  CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
    
 
   
 
     
   
   
          
     
  
    
     
 
    
      
     
 
     
    You can’t perform that action at this time.
  
 
    
  
     
    
      
        
     
 
       
      
     
   
 
    
    
  
 
  
 
     
    
0 commit comments