Skip to content

Conversation

@remi-delmas-3000
Copy link
Contributor

@remi-delmas-3000 remi-delmas-3000 commented Feb 20, 2023

Description of changes:

When --write-goto-binary is used, JSON symtab files are not produced, so we should not rely on them.
For --gen-c we now store the name to prettyName mapping in its own JSON ArtifactType::PrettyNameMap.
For --function, we modify CargoOutputs so that it tracks GOTO symtabs instead of JSON symtabs.

Testing:

  • How is this change tested?

CI regression run.

  • 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.

@remi-delmas-3000 remi-delmas-3000 added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Feb 20, 2023
@remi-delmas-3000 remi-delmas-3000 requested a review from a team as a code owner February 20, 2023 22:30
@remi-delmas-3000 remi-delmas-3000 self-assigned this Feb 20, 2023
@remi-delmas-3000 remi-delmas-3000 mentioned this pull request Feb 20, 2023
4 tasks
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Thanks! One minor comment. Otherwise looks good.

When `--write-goto-binary` is used, JSON symtab files are not produced, so we should not rely on them.
For `--gen-c` we now store the `name` to `prettyName` mapping in its own JSON `ArtifactType::PrettyNameMap`.
For `--function`, we modify `CargoOutputs` so that it tracks GOTO symtabs instead of JSON symtabs.
@zhassan-aws zhassan-aws merged commit 6c96d1e into model-checking:main Feb 21, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Projects

No open projects
Status: No status

Development

Successfully merging this pull request may close these issues.

3 participants