Skip to content

Update build workflow with cargo build#878

Merged
adpaco-aws merged 3 commits intomodel-checking:mainfrom
adpaco-aws:fix-bookrunner
Mar 1, 2022
Merged

Update build workflow with cargo build#878
adpaco-aws merged 3 commits intomodel-checking:mainfrom
adpaco-aws:fix-bookrunner

Conversation

@adpaco-aws
Copy link
Copy Markdown
Contributor

Description of changes:

Updates the build workflow to build cargo-kani and kani-link-restrictions. Changes the expected number of failures to 94.

Resolved issues:

Resolves #876

Call-outs:

Building kani-link-restrictions appears to be necessary, otherwise I get this error:

Error: Unable to find kani-link-restrictions. Looked for /home/ubuntu/kani/target/debug/kani-link-restrictions

Stack backtrace:
   0: anyhow::error::<impl anyhow::Error>::msg
             at /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/anyhow-1.0.52/src/error.rs:79:36
   1: cargo_kani::session::InstallType::kani_link_restrictions
             at ./src/cargo-kani/src/session.rs:215:21
   2: cargo_kani::session::KaniSession::new
             at ./src/cargo-kani/src/session.rs:49:37
   3: cargo_kani::standalone_main
             at ./src/cargo-kani/src/main.rs:70:15
   4: cargo_kani::main
             at ./src/cargo-kani/src/main.rs:27:39
   5: core::ops::function::FnOnce::call_once
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/core/src/ops/function.rs:227:5
   6: std::sys_common::backtrace::__rust_begin_short_backtrace
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/sys_common/backtrace.rs:122:18
   7: std::rt::lang_start::{{closure}}
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/rt.rs:145:18
   8: core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &F>::call_once
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/core/src/ops/function.rs:259:13
   9: std::panicking::try::do_call
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/panicking.rs:492:40
  10: std::panicking::try
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/panicking.rs:456:19
  11: std::panic::catch_unwind
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/panic.rs:137:14
  12: std::rt::lang_start_internal::{{closure}}
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/rt.rs:128:48
  13: std::panicking::try::do_call
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/panicking.rs:492:40
  14: std::panicking::try
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/panicking.rs:456:19
  15: std::panic::catch_unwind
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/panic.rs:137:14
  16: std::rt::lang_start_internal
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/rt.rs:128:20
  17: std::rt::lang_start
             at /rustc/03a8cc7df1d65554a4d40825b0490c93ac0f0236/library/std/src/rt.rs:144:17
  18: main
  19: __libc_start_main
  20: _start

Do we need an issue for this?

Testing:

  • How is this change tested? CI.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@adpaco-aws adpaco-aws requested a review from a team as a code owner March 1, 2022 22:46
Copy link
Copy Markdown
Contributor

@tedinski tedinski left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

link restrictions should be built, right up until we remove it as a binary separate from cargo-kani which will be coming before too long.

Comment on lines +37 to +39
cargo build -p kani-compiler
cargo build -p cargo-kani
cargo build -p kani-link-restrictions
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should we not just cargo build?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I thought we wanted to avoid building everything here for some reason, but that doesn't seem to be the case.

@adpaco-aws adpaco-aws changed the title Update build workflow with cargo-kani Update build workflow with cargo build Mar 1, 2022
@adpaco-aws adpaco-aws merged commit 3a6ed1c into model-checking:main Mar 1, 2022
@adpaco-aws adpaco-aws deleted the fix-bookrunner branch March 1, 2022 23:23
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Build `cargo-kani` and `kani-link-restrictions` in build action

* Update number of expected failures

* Build all the things
tedinski pushed a commit that referenced this pull request Apr 27, 2022
* Build `cargo-kani` and `kani-link-restrictions` in build action

* Update number of expected failures

* Build all the things
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

All bookrunner examples show verification failures

3 participants