In #263 we had to disable default checks in some tests to keep them working the same way. The affected tests are: - [ ] `src/test/cbmc/CodegenConstValue/main.rs` - [x] `src/test/cbmc/DynTrait/boxed_closure.rs` - [x] `src/test/cbmc/DynTrait/dyn_fn_param.rs` - [ ] `src/test/cbmc/FunctionCall_Ret-Param/main.rs` - [x] `src/test/cbmc/PointerOffset/Stable/main.rs` - [x] `src/test/cbmc/PointerOffset/Unstable/main.rs` - [ ] `src/test/cbmc/Pointers_OtherTypes/main.rs` - [x] `src/test/cbmc/Strings/main.rs` - [x] `src/test/cbmc/SwitchInt/main.rs` - [x] `src/test/cbmc/Whitespace/main.rs` - [x] `src/test/firecracker/virtio-block-parse/main.rs`
In #263 we had to disable default checks in some tests to keep them working the same way. The affected tests are:
src/test/cbmc/CodegenConstValue/main.rssrc/test/cbmc/DynTrait/boxed_closure.rssrc/test/cbmc/DynTrait/dyn_fn_param.rssrc/test/cbmc/FunctionCall_Ret-Param/main.rssrc/test/cbmc/PointerOffset/Stable/main.rssrc/test/cbmc/PointerOffset/Unstable/main.rssrc/test/cbmc/Pointers_OtherTypes/main.rssrc/test/cbmc/Strings/main.rssrc/test/cbmc/SwitchInt/main.rssrc/test/cbmc/Whitespace/main.rssrc/test/firecracker/virtio-block-parse/main.rs