Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upgrade Rust toolchain to nightly-2024-03-29 #3116

Merged
Merged
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
c89426c
Upgrade Rust toolchain to nightly-2024-03-29
feliperodri Mar 29, 2024
6e33108
Correctly use NullOp::UbChecks
feliperodri Mar 29, 2024
7d69cab
Update calls to ty::RawPtr
feliperodri Mar 29, 2024
0e52fed
Remove use of pretty_ty
feliperodri Mar 29, 2024
fdf28f6
Add #[allow(dead_code)] to avoid spurious warnings
feliperodri Mar 29, 2024
cd134a8
Remove dead code
feliperodri Mar 29, 2024
851362e
Update kani-compiler/src/kani_middle/transform/body.rs
tautschnig Apr 4, 2024
f93193c
fixup! Update kani-compiler/src/kani_middle/transform/body.rs
tautschnig Apr 4, 2024
31c549d
Implement typed_swap intrinsic
tautschnig Apr 4, 2024
20e1e17
Merge remote-tracking branch 'origin/main' into toolchain-upgrade-202…
tautschnig Apr 4, 2024
c270426
fixup! Remove use of pretty_ty
tautschnig Apr 4, 2024
1b4a535
Add #[allow(dead_code)] to keep clippy happy
tautschnig Apr 4, 2024
3077014
fixup! fixup! Update kani-compiler/src/kani_middle/transform/body.rs
tautschnig Apr 4, 2024
85f0818
Merge branch 'main' into toolchain-upgrade-2024-03-29
tautschnig Apr 4, 2024
d4abc03
Add test for typed_swap
tautschnig Apr 5, 2024
fc083d6
Add typed_swap to documentation
tautschnig Apr 5, 2024
7344be8
fixup! Add test for typed_swap
tautschnig Apr 5, 2024
518fd07
typed_swap: use x, y
tautschnig Apr 5, 2024
4dc6be4
Check types
tautschnig Apr 5, 2024
50d34e6
Restore start/end column fields
tautschnig Apr 5, 2024
1573607
Merge remote-tracking branch 'origin/main' into toolchain-upgrade-202…
tautschnig Apr 5, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update calls to ty::RawPtr
Signed-off-by: Felipe R. Monteiro <[email protected]>
  • Loading branch information
feliperodri committed Mar 29, 2024
commit 7d69cab86ea726acb676688c23e37cc8d3ef8385
11 changes: 4 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -570,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
// Note: This is not valid C but CBMC seems to be ok with it.
ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
ty::Str => Type::unsigned_int(8).flexible_array_of(),
ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
ty::FnDef(def_id, args) => {
let instance =
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
Expand Down Expand Up @@ -993,7 +993,7 @@ impl<'tcx> GotocCtx<'tcx> {
| ty::Foreign(_)
| ty::Coroutine(..)
| ty::Int(_)
| ty::RawPtr(_)
| ty::RawPtr(_, _)
| ty::Ref(..)
| ty::Tuple(_)
| ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
Expand Down Expand Up @@ -1352,10 +1352,7 @@ impl<'tcx> GotocCtx<'tcx> {
// `F16` and `F128` are not yet handled.
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
Primitive::F16 | Primitive::F128 => unimplemented!(),
Primitive::Pointer(_) => Ty::new_ptr(
self.tcx,
ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },
),
Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
}
}

Expand Down Expand Up @@ -1659,7 +1656,7 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec<DatatypeComponent> {
pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
match mir_type.kind() {
ty::Ref(_, pointee_type, _) => Some(*pointee_type),
ty::RawPtr(ty::TypeAndMut { ty: pointee_type, .. }) => Some(*pointee_type),
ty::RawPtr(pointee_type, _) => Some(*pointee_type),
_ => None,
}
}
Expand Down