Re-enable RMC to allow users to verify non-public main. #656
Conversation
Users don't usually set their main function to be public and we should enable them to verify their main function. For now, users will have to manually set the create type when running RMC directly. For cargo rmc, this should be automatically set up by cargo.
adpaco-aws
left a comment
adpaco-aws
left a comment
There was a problem hiding this comment.
Does not look ready to me, see comments below. Also, how it comes we are able to codegen binary crates now? The changes in RMC scripts remove all lib-related flags, I do not see any major change anywhere in this PR.
| // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
| pub fn main() { | ||
| fn main() { |
There was a problem hiding this comment.
Isn't this change needed for each test as in #523?
There was a problem hiding this comment.
No. It's not needed as in #523. With this change RMC will accept both public and non public main.
There was a problem hiding this comment.
Yes, I understand it is not strictly need but nice to have. Anyway, let me take care of that in #659
| .args(&self.props.cbmc_flags); | ||
| self.add_rmc_dir_to_path(&mut rmc); | ||
| let proc_res = self.compose_and_run_compiler(rmc, None); | ||
| let proc_res = self.run_rmc(); |
There was a problem hiding this comment.
Thanks for refactoring this!
Previous fixes is what enabled us to be able to codegen binary crates. This PR is just to remove the hack that we were enforcing the crate type to be a lib. |
Co-authored-by: Adrian Palacios <[email protected]>
| .args(&self.props.cbmc_flags); | ||
| self.add_rmc_dir_to_path(&mut rmc); | ||
| let proc_res = self.compose_and_run_compiler(rmc, None); | ||
| let proc_res = self.run_rmc(); |
…ng#656) * Re-enable RMC to allow users to verify non-public main. Users don't usually set their main function to be public and we should enable them to verify their main function. For now, users will have to manually set the create type when running RMC directly. For cargo rmc, this should be automatically set up by cargo. * Update src/tools/dashboard/src/books.rs Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>
* Re-enable RMC to allow users to verify non-public main. Users don't usually set their main function to be public and we should enable them to verify their main function. For now, users will have to manually set the create type when running RMC directly. For cargo rmc, this should be automatically set up by cargo. * Update src/tools/dashboard/src/books.rs Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>
4 participants
Users don't usually set their main function to be public and we should enable them to verify their main function. For now, users will have to manually set the create type when running RMC directly. For cargo rmc, this should be automatically set up by cargo.
Resolved issues:
Resolves #655
Call-outs:
We should figure out what is the default behavior of RMC and we might want to add a mechanism to figure out which one to use based on the user configuration. For example, maybe we can check what is the target function for the verification.
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.