File tree Expand file tree Collapse file tree 1 file changed +2
-14
lines changed Expand file tree Collapse file tree 1 file changed +2
-14
lines changed Original file line number Diff line number Diff line change @@ -144,20 +144,8 @@ compiles as if it was sequential code.
144144
145145### Standard library functions  
146146
147- At present, Kani is able to link in functions from the standard library but the
148- generated code will not contain them unless they are generic, intrinsics,
149- inlined or macros. Missing functions are treated in a similar way to [ unsupported
150- features] ( #code-generation-for-unsupported-features ) .
151- This results in verification failures if a call to one of these missing functions
152- is reachable.
153- 
154- We've done some experiments to embed the standard library into the generated
155- code, but this causes verification times to increase significantly. As of now,
156- we've not been able to find a simple solution for [ this
157- issue] ( https://github.com/model-checking/kani/issues/581 ) , but we have some
158- ideas for future work in this direction. At present, Kani
159- [ overrides] ( ./overrides.md )  a few common functions (e.g., print macros) as
160- a workaround.
147+ Kani [ overrides] ( ./overrides.md )  a few common functions
148+ (e.g., print macros) to provide a more verification friendly implementation.
161149
162150### Advanced features  
163151
 
 
   
 
     
   
   
          
    
    
     
    
      
     
     
    You can’t perform that action at this time.
  
 
    
  
    
      
        
     
       
      
     
   
 
    
    
  
 
  
 
     
    
0 commit comments