Skip to content

VSD Intervals #5354

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.

Sign up for GitHub

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

Jump to bottom
Closed
thk123 wants to merge 37 commits into from
Closed

VSD Intervals #5354

thk123 wants to merge 37 commits into from

Conversation

@thk123
Copy link
Contributor

@thk123 thk123 commented May 21, 2020

Rebased version of #5203 to see codecov report

  • 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.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Daniel Neville and others added 30 commits May 21, 2020 17:43
(INT) Interval operations
18b9509 
(INT) Interval values
@hannes-steffenhagen-diffblue
(INT) Fix broken interval unit tests
fa59ec0
@hannes-steffenhagen-diffblue
(INT) Remove unnecessary construction of dstring
58c8a58 
Also fix wrong placing of parentheses in output
@hannes-steffenhagen-diffblue
(INT) Rename interval is_constant to is_single_value_interval
f1b673d 
As it stands in conflicted with the method from exprt
@hannes-steffenhagen-diffblue
(INT) Rename is_true and is_false in interval expressions
4adae76 
So they don't conflict with the exprt methods
@hannes-steffenhagen-diffblue
(INT) Make eval take an identifier instead of an exprt
66b6a40
@hannes-steffenhagen-diffblue
(INT) Make constructors take constant references instead of values
8797aee 
Also, mark them as explicit where appropriate and
add some documentation
@hannes-steffenhagen-diffblue
(INT) Apply clang-format
da5dd0f
@hannes-steffenhagen-diffblue
(INT) Remove unnecessary constant specifier from value returning func…
e8deecc 
…tions
@hannes-steffenhagen-diffblue
(INT) Use irep_idt in place of exprt when exprt isn't needed
f8091c9 
Also replace some asserts with INVARIANT, PRECONDITION or UNREACHABLE
@hannes-steffenhagen-diffblue
(INT) Cleanup to_string and operator<< for intervals
ffde1ee 
Also left some comments for things that need to be cleaned up
in the future
@hannes-steffenhagen-diffblue
(INT) Give handle constants a better name
4012743
@hannes-steffenhagen-diffblue
(INT) Remove swap function in intervals
25a34d9 
Also, refactor minus and correct a typo in the comments
@hannes-steffenhagen-diffblue
(INT) Add additional unit tests for intervals
b035c8b
@hannes-steffenhagen-diffblue
(INT) Various code style fixes in intervals code
d373df2
@NlightNFotis
(INT) Fix eval handling of ID_not case in intervals
6e36c8c 
And also add tests for it.
@NlightNFotis
(INT) Fix bitwise operators for intervals
e850530 
and add tests for them and eval.
@danpoe
(INT) Make eval in constant_interval_exprt const
e536404
@danpoe
(INT) Removed unimplemented function from util/interval.h
1321ed2
@danpoe
(INT) accept false of ID_bool as valid zero value
e3dbce7
@danpoe
(INT) Add ID_bool type preconditions to logical interval operations
eebfcbc
@danpoe
(INT) use tvt_to_interval instead of tv_to_interval in constant_inter…
6fb8567 
…val_exprt
@danpoe
(INT) Handle typecasts in constant_interval_exprt
f7152b5
(INT) Typecast from ID_bool to integer types
0077a18
(INT) Addressing review comments
8c5f9b6
@danpoe
(INT) Add well-formedness checks for constant_interval_exprt
f57a616
(INT) Extend interval multiplication for extremes
2bec215
(INT) Add support for bit field and enums intervals.cpp
7c050a2
@hannes-steffenhagen-diffblue
(INT) Fix broken interval unit tests
7a5c6d3
@hannes-steffenhagen-diffblue
(INT) Fix bug with interval typecasts
b685412 
Previously the typecast operator for interval_exprt simply set the type on the
bounds; This yielded incorrect results for widening or narrowing casts. This
delegates the typecast handling to simplify_expr instead.
@thk123
Copy link
Contributor Author

thk123 commented May 22, 2020

CI failing due to seemingly missing unit tests from the Makefile

@codecov
Copy link

codecov bot commented May 22, 2020 •
edited
Loading

Codecov Report

Merging #5354 into develop will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5354   +/-   ##
========================================
  Coverage    68.04%   68.04%           
========================================
  Files         1172     1172           
  Lines        97151    97151           
========================================
  Hits         66106    66106           
  Misses       31045    31045
Flag Coverage Δ
#cproversmt2 42.47% <0.00%> (ø)
#regression 65.35% <0.00%> (ø)
#unit 31.94% <0.00%> (ø)

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

@thk123
Copy link
Contributor Author

thk123 commented May 27, 2020

On this branch I've attempted to start tidying up the interface - but this work should wait until VSD is merged, to avoid having to dive into the VSD commits and fixing them inline

@thk123 thk123 closed this May 27, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs will be requested when the pull request is marked ready for review martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel will be requested when the pull request is marked ready for review peterschrammel is a code owner

@kroening kroening Awaiting requested review from kroening kroening will be requested when the pull request is marked ready for review kroening is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig will be requested when the pull request is marked ready for review tautschnig is a code owner

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@thk123 @hannes-steffenhagen-diffblue @NlightNFotis @danpoe @chrisr-diffblue