Skip to content

need to check lower bound on index in rw_range_sett::get_objects_byte_extract #2822

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 1 commit into from
Feb 26, 2022

Conversation

kroening
Copy link
Member

This addresses part of issue #2653

@peterschrammel
Copy link
Member

This seems related to #2524.

@kroening
Copy link
Member Author

Ok, let's see whether that can do a KNOWNBUG -> CORE.

@NlightNFotis
Copy link
Contributor

Hi @kroening, is it possible that you address the issues that Michael raised?

If not, shall we have this closed please?

A negative offset may result in a read/write access to a parent object.

Fixes: #2524

Co-authored-by: Michael Tautschnig <[email protected]>
@tautschnig tautschnig force-pushed the rw_range_lower_bound_fix branch from 8bc1b47 to afac4a0 Compare February 15, 2022 21:21
@codecov
Copy link

codecov bot commented Feb 15, 2022

Codecov Report

Merging #2822 (afac4a0) into develop (b26ad8b) will increase coverage by 0.06%.
The diff coverage is 99.76%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #2822      +/-   ##
===========================================
+ Coverage    76.76%   76.82%   +0.06%     
===========================================
  Files         1582     1582              
  Lines       182360   182769     +409     
===========================================
+ Hits        139992   140416     +424     
+ Misses       42368    42353      -15     
Impacted Files Coverage Δ
src/analyses/goto_rw.cpp 55.90% <75.00%> (+3.60%) ⬆️
...solvers/smt2_incremental/smt_bit_vector_theory.cpp 100.00% <100.00%> (ø)
...solvers/smt2_incremental/smt_bit_vector_theory.cpp 100.00% <100.00%> (ø)
src/cbmc/cbmc_parse_options.cpp 77.77% <0.00%> (+0.21%) ⬆️

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 a3e1411...afac4a0. Read the comment docs.

@tautschnig tautschnig merged commit 1e5b7aa into develop Feb 26, 2022
@tautschnig tautschnig deleted the rw_range_lower_bound_fix branch February 26, 2022 17:11
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