File tree Expand file tree Collapse file tree 1 file changed +5
-0
lines changed Expand file tree Collapse file tree 1 file changed +5
-0
lines changed Original file line number Diff line number Diff line change @@ -21,10 +21,15 @@ struct
2121
2222  (*  HELPER FUNCTIONS *) 
2323
24+   let  warn_for_multi_threaded  ctx  behavior  cwe_number  = 
25+     if  not  (ctx.ask (Queries. MustBeSingleThreaded )) then 
26+       M. warn ~category: (Behavior  behavior) ~tags: [CWE  cwe_number] " Program isn't running in single-threaded mode. Use-After-Free might occur due to multi-threading" 
27+ 
2428  let  rec  warn_lval_might_contain_freed  ?(is_double_free  = false )  (transfer_fn_name :string ) ctx  (lval :lval ) = 
2529    let  state =  ctx.local in 
2630    let  undefined_behavior =  if  is_double_free then  Undefined  DoubleFree  else  Undefined  UseAfterFree  in 
2731    let  cwe_number =  if  is_double_free then  415  else  416  in 
32+     warn_for_multi_threaded ctx undefined_behavior cwe_number; (*  Simple solution to warn when multi-threaded *) 
2833    let  rec  offset_might_contain_freed  offset  = 
2934      match  offset with 
3035      |  NoOffset  -> () 
 
 
   
 
     
   
   
          
    
    
     
    
      
     
     
    You can’t perform that action at this time.
  
 
    
  
    
      
        
     
       
      
     
   
 
    
    
  
 
  
 
     
    
0 commit comments