kani icon indicating copy to clipboard operation
kani copied to clipboard

Tracking issue: Tests with default checks disabled

Open adpaco-aws opened this issue 4 years ago • 3 comments

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

adpaco-aws avatar Jul 07 '21 17:07 adpaco-aws

#335 removed the --no-memory-safety-checks flag in DynTrait/boxed_closure.rs

adpaco-aws avatar Jul 30 '21 10:07 adpaco-aws

https://github.com/model-checking/rmc/pull/373 resolves DynTrait/dyn_fn_param.rs

avanhatt avatar Aug 04 '21 21:08 avanhatt

#647 fixed the following tests:

  • src/test/firecracker/virtio-block-parse/main.rs
  • src/test/rmc/PointerOffset/Stable/main.rs
  • src/test/rmc/PointerOffset/Unstable/main.rs
  • src/test/rmc/Strings/main.rs
  • src/test/rmc/SwitchInt/main.rs
  • src/test/rmc/Whitespace/main.rs

celinval avatar Nov 23 '21 22:11 celinval