File tree 1 file changed +2
-14
lines changed
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.
144
144
145
145
### Standard library functions
146
146
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.
161
149
162
150
### Advanced features
163
151
You can’t perform that action at this time.
0 commit comments