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.

Sign up for GitHub

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

Jump to bottom

Places with missing Location. #136

Closed
89 tasks
vecchiot-aws opened this issue May 21, 2021 · 0 comments · Fixed by #3253
Closed
89 tasks

Places with missing Location. #136

vecchiot-aws opened this issue May 21, 2021 · 0 comments · Fixed by #3253
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.

Comments

@vecchiot-aws
Copy link
Contributor

vecchiot-aws commented May 21, 2021 •
edited
Loading

These come from making certain constructors require Location to be passed in, and where the caller has no clear Location to use (currently using Location::none()).

  • Expr::ret
    • compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
      • GotocCtx::bound_ty_above_and_below
      • GotocCtx::bound_true_false
      • GotocCtx::codegen_assumption_ref_ptr_slice
      • GotocCtx::codegen_assumption_ref_ptr_slice
      • GotocCtx::codegen_assumption_ref_ptr_thin
      • GotocCtx::codegen_assumption_struct
      • GotocCtx::codegen_assumption_enum_single_variant
      • GotocCtx::codegen_assumption_enum_niche
      • GotocCtx::codegen_assumption_enum_direct
      • GotocCtx::codegen_assumption_array
      • GotocCtx::codegen_assumption_array
      • GotocCtx::codegen_assumption_tuple
    • compiler/rustc_codegen_llvm/src/gotoc/operand.rs
      • GotocCtx::codegen_direct_literal
      • GotocCtx::codegen_niche_literal
    • compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
      • GotocCtx::codegen_rvalue_repeat
  • Expr::assign
    • compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
      • GotocHook(Nondet)::handle
      • GotocHook(MemReplace)::handle
      • GotocHook(MemReplace)::handle
      • GotocHook(MemSwap)::handle
      • GotocHook(MemSwap)::handle
      • GotocHook(PtrRead)::handle
      • GotocHook(PtrWrite)::handle
      • GotocHook(SliceFromRawPart)::handle
    • compiler/rustc_codegen_llvm/src/gotoc/operand.rs
      • GotocCtx::codegen_direct_literal
      • GotocCtx::codegen_alloc_in_memory
      • GotocCtx::codegen_niche_literal
    • compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
      • GotocCtx::codegen_rvalue_repeat
      • GotocCtx::codegen_vtable
    • compiler/rustc_codegen_llvm/src/gotoc/statement.rs
      • GotocCtx::codegen_expr_to_place
      • GotocCtx::codegen_statement
      • GotocCtx::codegen_statement
      • GotocCtx::codegen_statement
      • GotocCtx::codegen_statement
      • GotocCtx::codegen_statement
  • Expr::as_stmt
    • compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
      • GotocCtx::codegen_assumption_ref_ptr_slice
      • GotocCtx::codegen_assumption_array
    • compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
      • GotocHook(MemSwap)::handle
    • compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
      • GotocCtx::codegen_rvalue_repeat
    • compiler/rustc_codegen_llvm/src/gotoc/statement.rs
      • GotocCtx::codegen_drop
      • GotocCtx::codegen_drop
      • GotocCtx::codegen_expr_to_place
      • GotocCtx::codegen_statement
      • GotocCtx::codegen_statement
  • Stmt::block
    • compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs
      • GotocCtx::codegen_assumption_ref_ptr_slice
      • GotocCtx::codegen_assumption_array
      • GotocCtx::codegen_assumption_genfunc
    • compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs
      • ToIrep(ExprValue)::to_irep
    • compiler/rustc_codegen_llvm/src/gotoc/hooks.rs
      • GotocHook(Nondet)::handle
      • GotocHook(Intrinsic)::handle
      • GotocHook(MemReplace)::handle
      • GotocHook(MemReplace)::handle
      • GotocHook(MemSwap)::handle
      • GotocHook(MemSwap)::handle
      • GotocHook(PtrRead)::handle
      • GotocHook(PtrWrite)::handle
      • GotocHook(RustAlloc)::handle
      • GotocHook(SliceFromRawPart)::handle
    • compiler/rustc_codegen_llvm/src/gotoc/metadata.rs
      • GotocCtx::register_initializer
    • compiler/rustc_codegen_llvm/src/gotoc/operand.rs
      • GotocCtx::codegen_direct_literal
      • GotocCtx::codegen_alloc_in_memory
      • GotocCtx::codegen_niche_literal
    • compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs
      • GotocCtx::codegen_rvalue_repeat
      • GotocCtx::codegen_rvalue_repeat
    • compiler/rustc_codegen_llvm/src/gotoc/statement.rs
      • GotocCtx::codegen_drop
      • GotocCtx::codegen_switch_int
    • compiler/rustc_codegen_llvm/src/gotoc/stubs/rust_stubber.rs
      • RustStubber::translate_function
@vecchiot-aws vecchiot-aws mentioned this issue May 21, 2021
Merged
4 tasks
@danielsn danielsn mentioned this issue Jun 8, 2021
Closed
celinval pushed a commit to celinval/kani-dev that referenced this issue Nov 16, 2021
@calebzulawski
Add from_bitmask (model-checking#136)
15b4e28 
* Add from_bitmask
* Add mips workaround
@tedinski tedinski added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. labels Nov 14, 2022
tautschnig added a commit to tautschnig/kani that referenced this issue Jun 11, 2024
@tautschnig
Remove further uses of Location::none
fb35ce0 
We now only have 11 uses of `Location::none` left, all of which have no
reasonable location to use.

Resolves: model-checking#136
@tautschnig tautschnig mentioned this issue Jun 11, 2024
Merged
tautschnig added a commit that referenced this issue Jun 12, 2024
@tautschnig
Remove further uses of Location::none (#3253)
7dad847 
We now only have 12 uses of `Location::none` left, all of which have no
reasonable location to use.

Resolves: #136
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Remove further uses of Location::none tautschnig/kani
2 participants
@tedinski @vecchiot-aws