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

List Subcommand (Implementation) #3523

Merged
merged 40 commits into from
Oct 9, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
f54c0f3
standalone list command
carolynzech Sep 12, 2024
67ed073
more concise pretty output
carolynzech Sep 12, 2024
4ace776
json output
carolynzech Sep 12, 2024
b903473
use standalone project instead
carolynzech Sep 12, 2024
b412d06
clippy
carolynzech Sep 12, 2024
bc802a1
refactor
carolynzech Sep 12, 2024
bfd2684
cargo list
carolynzech Sep 12, 2024
8e4efc0
use CrateItems instead; refactor into kani-middle
carolynzech Sep 16, 2024
2e79fbc
add std flag
carolynzech Sep 16, 2024
b1c5a9e
output updates
carolynzech Sep 16, 2024
ced1dab
update RFC with implementation
carolynzech Sep 16, 2024
c98b0b0
nits
carolynzech Sep 17, 2024
b57e47d
add tests
carolynzech Sep 17, 2024
6a659d0
add modifies rationale to rfc
carolynzech Sep 17, 2024
d88a4aa
Merge branch 'main' into list-subcommand
carolynzech Sep 17, 2024
87328bc
copyrights
carolynzech Sep 17, 2024
0e14cd1
Merge branch 'list-subcommand' of github.com:carolynzech/kani into li…
carolynzech Sep 17, 2024
e41c2b6
kani-compiler is list-agnostic
carolynzech Sep 20, 2024
5d0edb8
check explicitly that fn resolves
carolynzech Sep 20, 2024
e5de12c
change tests to json; sort output
carolynzech Sep 26, 2024
7a52503
clippy
carolynzech Sep 26, 2024
552f339
Merge branch 'main' into list-subcommand
carolynzech Sep 27, 2024
7383445
clippy
carolynzech Sep 27, 2024
55c9937
revert unnecessary changes
carolynzech Sep 27, 2024
a85ec2c
update rfc
carolynzech Sep 27, 2024
76365a3
Merge branch 'main' into list-subcommand
carolynzech Sep 27, 2024
b5f48a1
update RFC status
carolynzech Oct 1, 2024
a2a5082
Merge branch 'main' into list-subcommand
carolynzech Oct 1, 2024
0854cb3
update Cargo.lock
carolynzech Oct 1, 2024
7faeb2a
remove cli-table dependency; print manually
carolynzech Oct 1, 2024
15dd78a
add Markdown explanation to RFc
carolynzech Oct 2, 2024
3f583d3
remove contracts count; reduce rfc detail
carolynzech Oct 2, 2024
9daa8ba
use StableDefId
carolynzech Oct 3, 2024
cfc1db3
Doc comments formatting
carolynzech Oct 4, 2024
3380cb8
PR feedback
carolynzech Oct 4, 2024
e3455c0
Apply RFC suggestions from code review
carolynzech Oct 7, 2024
2ad1360
Apply suggestions from code review
carolynzech Oct 7, 2024
1cc50a0
remove contracts count mention from RFC
carolynzech Oct 7, 2024
c2474e3
rfc nit
carolynzech Oct 7, 2024
5d536c1
Merge branch 'main' into list-subcommand
carolynzech Oct 9, 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
Merge branch 'main' into list-subcommand
  • Loading branch information
carolynzech authored Sep 27, 2024
commit 552f3390de1d06e5c94b429ff1f6671a6ec434b6
5 changes: 2 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,8 @@ use rustc_hir::def_id::DefId as InternalDefId;
use rustc_smir::rustc_internal;
use stable_mir::CrateDef;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::mir::Local;
use stable_mir::ty::{RigidTy, TyKind};
use stable_mir::CrateDef;
use stable_mir::mir::{Local, VarDebugInfoContents};
use stable_mir::ty::{FnDef, RigidTy, TyKind};

impl<'tcx> GotocCtx<'tcx> {
/// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/kani_middle/metadata.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ use stable_mir::mir::{Body, TerminatorKind};
use stable_mir::ty::{RigidTy, TyKind};
use stable_mir::{CrateDef, CrateItems};

/// Create the harness metadata for a proof harness for a given function.
pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
let def = instance.def;
let kani_attributes = KaniAttributes::for_instance(tcx, instance);
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/kani_middle/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ use rustc_target::abi::call::FnAbi;
use rustc_target::abi::{HasDataLayout, TargetDataLayout};
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::mir::{Body, VarDebugInfoContents};
use stable_mir::CrateDef;
use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
use stable_mir::visitor::{Visitable, Visitor as TyVisitor};
use std::ops::ControlFlow;
Expand Down
Loading
You are viewing a condensed version of this merge commit. You can view the full changes here.