Skip to content

Expression initialiser: do not generate nil for empty union #5667

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

Closed

Conversation

tautschnig
Copy link
Collaborator

Empty unions do not have a meaningful union_exprt as an initialiser, and
thus the expression initialiser should make use of returning an
optionalt{} instead.

This test was generated using C-Reduce based on an example initially
generated by CSmith.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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 Dec 15, 2020

Codecov Report

Merging #5667 (8cf524f) into develop (c29b69a) will decrease coverage by 0.02%.
The diff coverage is 82.75%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5667      +/-   ##
===========================================
- Coverage    74.44%   74.41%   -0.03%     
===========================================
  Files         1446     1447       +1     
  Lines       157778   157786       +8     
===========================================
- Hits        117456   117420      -36     
- Misses       40322    40366      +44     
Impacted Files Coverage Δ
jbmc/src/janalyzer/janalyzer_main.cpp 100.00% <ø> (ø)
jbmc/src/java_bytecode/assignments_from_json.cpp 97.26% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods.cpp 99.47% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods.h 100.00% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp 98.24% <ø> (ø)
jbmc/src/java_bytecode/ci_lazy_methods_needed.h 100.00% <ø> (ø)
jbmc/src/java_bytecode/convert_java_nondet.cpp 81.15% <ø> (ø)
...java_bytecode/create_array_with_type_intrinsic.cpp 97.67% <ø> (ø)
jbmc/src/java_bytecode/expr2java.cpp 86.61% <ø> (ø)
jbmc/src/java_bytecode/expr2java.h 100.00% <ø> (ø)
... and 705 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1ab5de1...8cf524f. Read the comment docs.

@tautschnig tautschnig marked this pull request as draft December 15, 2020 14:37
@tautschnig tautschnig self-assigned this Dec 15, 2020
@tautschnig tautschnig force-pushed the empty-union-initialiser2 branch from 8c1903e to f893582 Compare December 16, 2020 00:34
@tautschnig tautschnig marked this pull request as ready for review December 16, 2020 00:35
@tautschnig tautschnig removed their assignment Dec 16, 2020
@tautschnig tautschnig force-pushed the empty-union-initialiser2 branch 2 times, most recently from 280d647 to 4e8f9ca Compare December 16, 2020 00:55
@tautschnig tautschnig force-pushed the empty-union-initialiser2 branch from 4e8f9ca to 600250e Compare March 3, 2021 07:54
Empty unions do not have a meaningful union_exprt as an initialiser, and
thus the expression initialiser should make use of returning an
optionalt{} instead.

This test was generated using C-Reduce based on an example initially
generated by CSmith.
@tautschnig tautschnig force-pushed the empty-union-initialiser2 branch from 600250e to 8cf524f Compare May 7, 2021 06:27
@tautschnig tautschnig self-assigned this May 7, 2021
@tautschnig
Copy link
Collaborator Author

Closing as #6408 addresses the issue more properly, and all tests from this PR pass as well with those changes made.

@tautschnig tautschnig closed this Oct 25, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant