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

Target directories should be cleaned before codegen #1821

Closed
adpaco-aws opened this issue Oct 31, 2022 · 0 comments · Fixed by #1847
Closed

Target directories should be cleaned before codegen #1821

adpaco-aws opened this issue Oct 31, 2022 · 0 comments · Fixed by #1847
Assignees
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@adpaco-aws
Copy link
Contributor

I've run into trouble a couple of times:

  • When working on Upgrade to CBMC 5.69.1 (with fixes) #1811 , cargo-kani regressions failed because conflicts were found in the GotoC programs I had generated. I think this is due to cargo-kani using the --target-dir option; not cleaning the directory first makes us reuse some code generated earlier.
  • When running the "unsupported features" experiment, it reported failures on half the crates because of some conflict. For this experiment, I need to run --legacy-linker (otherwise nothing is shown), and cleaning the experiments folder helped. I don't have a log file, but this one can be reproduced running the experiment first as is, and then with --legacy-linker.

But in general, whenever we are going to generate and link code, we should be cleaning the whole folder first. I believe some commands even use wildcards so it's no surprise this happens.

@adpaco-aws adpaco-aws added [C] Bug This is a bug. Something isn't working. Area: compilation labels Oct 31, 2022
@celinval celinval moved this to In Progress in Kani 0.15 Nov 3, 2022
Repository owner moved this from In Progress to Done in Kani 0.15 Nov 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
No open projects
Status: Done
Development

Successfully merging a pull request may close this issue.

2 participants