Skip to content

Add and use symbolt constructors #6591

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

Merged
merged 10 commits into from
Dec 1, 2022

Conversation

tautschnig
Copy link
Collaborator

To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Jan 18, 2022

Codecov Report

Base: 78.38% // Head: 78.32% // Decreases project coverage by -0.05% ⚠️

Coverage data is based on head (60eaaad) compared to base (9100d23).
Patch coverage: 91.53% of modified lines in pull request are covered.

❗ Current head 60eaaad differs from pull request most recent head 6ac16bf. Consider uploading reports for the commit 6ac16bf to get more accurate results

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #6591      +/-   ##
===========================================
- Coverage    78.38%   78.32%   -0.06%     
===========================================
  Files         1647     1645       -2     
  Lines       190362   189922     -440     
===========================================
- Hits        149213   148760     -453     
- Misses       41149    41162      +13     
Impacted Files Coverage Δ
src/ansi-c/ansi_c_declaration.h 95.23% <ø> (ø)
src/goto-instrument/accelerate/accelerate.cpp 32.50% <0.00%> (+0.22%) ⬆️
src/goto-instrument/dump_c.cpp 79.97% <0.00%> (ø)
src/goto-instrument/function.cpp 0.00% <ø> (ø)
src/goto-instrument/race_check.cpp 0.00% <0.00%> (ø)
src/goto-programs/builtin_functions.cpp 59.10% <0.00%> (-0.92%) ⬇️
src/goto-symex/auto_objects.cpp 25.00% <0.00%> (+1.19%) ⬆️
src/jsil/jsil_convert.cpp 0.00% <0.00%> (ø)
src/jsil/jsil_entry_point.cpp 0.00% <0.00%> (ø)
src/jsil/jsil_internal_additions.cpp 0.00% <0.00%> (ø)
... and 156 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

@tautschnig
Copy link
Collaborator Author

To reviewers (multiple required): please review commit-by-commit, possibly choosing only those parts of the code that you actually care about (the parts can be inferred from the commit messages).

Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

Whilst I'm not usually a massive fan of wide changes for the sake of them, I'm very happy to see this change - especially the dropping of lots of ...is_type=false :-)

Might be worth a quick sanity check with @martin-cs that this doesn't clash with anything urgent he may be working on - especially around gnat2goto and related projects.

@@ -446,14 +446,10 @@ void java_bytecode_convert_classt::convert(
}(id2string(c.name));

// produce class symbol
symbolt new_symbol;
class_type.set_name(qualified_classname);
type_symbolt new_symbol{qualified_classname, class_type, ID_java};
Copy link
Contributor

Choose a reason for hiding this comment

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

👍

Copy link
Collaborator

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

Approving changes to code contracts. LGTM.

@tautschnig tautschnig force-pushed the cleanup/symbolt branch 3 times, most recently from 9a33916 to 24e97f1 Compare February 3, 2022 16:27
@tautschnig tautschnig force-pushed the cleanup/symbolt branch 2 times, most recently from 2c89546 to 508335e Compare February 26, 2022 21:47
@SaswatPadhi SaswatPadhi removed their request for review September 17, 2022 23:58
@tautschnig
Copy link
Collaborator Author

tautschnig commented Sep 28, 2022

Requires #7160 for CI to pass. (merged, rebased)

@tautschnig tautschnig force-pushed the cleanup/symbolt branch 2 times, most recently from ddbc0fb to dc3abbe Compare October 7, 2022 14:01
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set. Constructors are now consistent in what they do,
and do not set the base_name in addition to the name.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.
@tautschnig tautschnig assigned tautschnig and unassigned kroening Dec 1, 2022
@tautschnig tautschnig merged commit 7b5945b into diffblue:develop Dec 1, 2022
@tautschnig tautschnig deleted the cleanup/symbolt branch December 1, 2022 22:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants