Skip to content

Conversation

@tautschnig
Copy link
Collaborator

Introduce a new expression to handle GCC's __builtin_X_overflow in the
middle-end (during goto conversion) instead of directly encoding the
semantics during type checking.

This commit is a refactoring only, it does not yet fix the bugs that #5544 intends to fix. #5544 will now be rebased on top of this commit.

  • 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 Mar 9, 2021

Codecov Report

Merging #5900 (1db0ad4) into develop (95e1161) will decrease coverage by 0.00%.
The diff coverage is 75.27%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5900      +/-   ##
===========================================
- Coverage    75.02%   75.02%   -0.01%     
===========================================
  Files         1431     1433       +2     
  Lines       155595   155752     +157     
===========================================
+ Hits        116734   116850     +116     
- Misses       38861    38902      +41     
Impacted Files Coverage Δ
src/ansi-c/c_typecheck_base.h 100.00% <ø> (ø)
src/goto-programs/goto_convert_class.h 87.30% <ø> (ø)
...rc/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp 76.58% <45.07%> (-4.36%) ⬇️
src/ansi-c/c_typecheck_expr.cpp 75.04% <81.81%> (-0.24%) ⬇️
src/ansi-c/c_expr.cpp 96.55% <96.55%> (ø)
src/goto-programs/goto_convert_side_effect.cpp 93.52% <96.66%> (+0.29%) ⬆️
src/ansi-c/c_expr.h 100.00% <100.00%> (ø)
...olvers/strings/string_constraint_instantiation.cpp 94.69% <0.00%> (+3.53%) ⬆️

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 ab538eb...1db0ad4. Read the comment docs.

@tautschnig tautschnig force-pushed the side-effect-overflow-expression branch from a5a38d3 to 6f99658 Compare March 9, 2021 10:29
@kroening
Copy link
Collaborator

Same here now -- consider ansi-c/c_expr.h

@tautschnig tautschnig force-pushed the side-effect-overflow-expression branch from 6f99658 to d905f8a Compare March 24, 2021 22:11
@tautschnig tautschnig force-pushed the side-effect-overflow-expression branch from d905f8a to adffad2 Compare March 25, 2021 21:16
@tautschnig tautschnig assigned tautschnig and unassigned kroening Mar 25, 2021
@tautschnig tautschnig force-pushed the side-effect-overflow-expression branch from adffad2 to 1739299 Compare March 25, 2021 22:40
Introduce a new expression to handle GCC's __builtin_X_overflow in the
middle-end (during goto conversion) instead of directly encoding the
semantics during type checking.
@tautschnig tautschnig force-pushed the side-effect-overflow-expression branch from 1739299 to 1db0ad4 Compare March 25, 2021 22:46
@tautschnig tautschnig merged commit 390f5c2 into diffblue:develop Mar 26, 2021
@tautschnig tautschnig deleted the side-effect-overflow-expression branch March 26, 2021 09:30
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.

3 participants