Skip to content

Changes to intervals needed to merge VSD #5203

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

Closed
wants to merge 35 commits into from
Closed

Changes to intervals needed to merge VSD #5203

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
b70513a
(INT) Interval operations
Jun 16, 2017
a003056
(INT) Fix broken interval unit tests
hannes-steffenhagen-diffblue May 9, 2018
5942219
(INT) Remove unnecessary construction of dstring
hannes-steffenhagen-diffblue May 16, 2018
b7a7123
(INT) Rename interval is_constant to is_single_value_interval
hannes-steffenhagen-diffblue May 16, 2018
848b976
(INT) Rename is_true and is_false in interval expressions
hannes-steffenhagen-diffblue May 16, 2018
ff3dd1f
(INT) Make eval take an identifier instead of an exprt
hannes-steffenhagen-diffblue May 16, 2018
fe65713
(INT) Make constructors take constant references instead of values
hannes-steffenhagen-diffblue May 16, 2018
bff9516
(INT) Apply clang-format
hannes-steffenhagen-diffblue May 16, 2018
0ed412f
(INT) Remove unnecessary constant specifier from value returning func…
hannes-steffenhagen-diffblue May 16, 2018
6abdda2
(INT) Use irep_idt in place of exprt when exprt isn't needed
hannes-steffenhagen-diffblue May 16, 2018
38193e1
(INT) Cleanup to_string and operator<< for intervals
hannes-steffenhagen-diffblue May 16, 2018
8f31842
(INT) Give handle constants a better name
hannes-steffenhagen-diffblue May 16, 2018
9e2e1a9
(INT) Remove swap function in intervals
hannes-steffenhagen-diffblue May 16, 2018
fa720e9
(INT) Add additional unit tests for intervals
hannes-steffenhagen-diffblue May 21, 2018
dfbe6c8
(INT) Various code style fixes in intervals code
hannes-steffenhagen-diffblue May 21, 2018
c46f13c
(INT) Fix eval handling of ID_not case in intervals
NlightNFotis May 23, 2018
1458656
(INT) Fix bitwise operators for intervals
NlightNFotis May 23, 2018
6940fe2
(INT) Make eval in constant_interval_exprt const
danpoe May 29, 2018
9972d79
(INT) Removed unimplemented function from util/interval.h
danpoe May 29, 2018
7235a30
(INT) accept false of ID_bool as valid zero value
danpoe May 29, 2018
6497477
(INT) Add ID_bool type preconditions to logical interval operations
danpoe May 29, 2018
d8c1e02
(INT) use tvt_to_interval instead of tv_to_interval in constant_inter…
danpoe May 29, 2018
19dbd4c
(INT) Handle typecasts in constant_interval_exprt
danpoe May 29, 2018
3ac8c90
(INT) Typecast from ID_bool to integer types
Dec 8, 2019
90ffba1
(INT) Addressing review comments
Dec 8, 2019
47424c0
(INT) Add well-formedness checks for constant_interval_exprt
danpoe May 30, 2018
bdc2b08
(INT) Extend interval multiplication for extremes
Sep 13, 2018
c42cac7
(INT) Add support for bit field and enums intervals.cpp
Dec 8, 2019
6cd795f
(INT) Fix broken interval unit tests
hannes-steffenhagen-diffblue Jul 18, 2018
efe4328
(INT) Fix bug with interval typecasts
hannes-steffenhagen-diffblue Jul 23, 2018
8d8ed40
(INT) Assume relation between two int vars (issue #179)
Sep 10, 2018
1867091
(INT) Fixup for nil_typet being removed
chrisr-diffblue Oct 11, 2019
4f76dbf
(INT) Fixups post-rebase
Dec 8, 2019
d62ce16
clang-format changes to the interval code and unit tests
Dec 9, 2019
d92a7db
Fixes for the linter.
Dec 9, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/analyses/interval_domain.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -329,10 +329,10 @@ void interval_domaint::assume_rec(
{
integer_intervalt &lhs_i=int_map[lhs_identifier];
integer_intervalt &rhs_i=int_map[rhs_identifier];
lhs_i.meet(rhs_i);
rhs_i=lhs_i;
if(rhs_i.is_bottom())
make_bottom();
if(id == ID_lt && !lhs_i.is_less_than(rhs_i))
Copy link
Contributor

Choose a reason for hiding this comment

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

❓ I'd expect to see an equivalent for ID_gt and ID_ge?

lhs_i.make_less_than(rhs_i);
if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i))
lhs_i.make_less_than_eq(rhs_i);
}
else if(is_float(lhs.type()) && is_float(rhs.type()))
{
Expand Down
1 change: 1 addition & 0 deletions src/util/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ SRC = allocate_objects.cpp \
version.cpp \
xml.cpp \
xml_irep.cpp \
interval.cpp \
# Empty last line

INCLUDES= -I ..
Expand Down
Loading