Code

Intervals with tests#5361

Code

Merged

thk123 merged 59 commits intodiffblue:developdiffblue/cbmc:developfrom

thk123:fix-vsd-intervalsthk123/cbmc:fix-vsd-intervalsCopy head branch name to clipboard

Jun 4, 2020

Commits

Commits on May 29, 2020

• (INT) Interval operations

  Show description for 9689a66
  

  Daniel Neville

  authored and

  Thomas Kiley

  committed
  9689a66

  Copy full SHA for 9689a66

• (INT) Fix broken interval unit tests

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  eefe162

  Copy full SHA for eefe162

• (INT) Rename interval is_constant to is_single_value_interval

  Show description for 4e2d044
  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  4e2d044

  Copy full SHA for 4e2d044

• (INT) Rename is_true and is_false in interval expressions

  Show description for 3473ad1
  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  3473ad1

  Copy full SHA for 3473ad1

• (INT) Make eval take an identifier instead of an exprt

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  ab44ab1

  Copy full SHA for ab44ab1

• (INT) Make constructors take constant references instead of values

  Show description for 1ba8004
  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  1ba8004

  Copy full SHA for 1ba8004

• (INT) Remove unnecessary constant specifier from value returning functions

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  007c84d

  Copy full SHA for 007c84d

• (INT) Use irep_idt in place of exprt when exprt isn't needed

  Show description for b9e0d5a
  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  b9e0d5a

  Copy full SHA for b9e0d5a

• (INT) Cleanup to_string and operator<< for intervals

  Show description for 8c48d15
  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  8c48d15

  Copy full SHA for 8c48d15

• (INT) Give handle constants a better name

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  bb0c583

  Copy full SHA for bb0c583

• (INT) Remove swap function in intervals

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  f7bb442

  Copy full SHA for f7bb442

• Refactor minus and correct a typo in the comments

  

  Thomas Kiley

  committed
  412bbad

  Copy full SHA for 412bbad

• (INT) Add additional unit tests for intervals

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  ad4dda3

  Copy full SHA for ad4dda3

• (INT) Various code style fixes in intervals code

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  d707ed0

  Copy full SHA for d707ed0

• (INT) Fix eval handling of ID_not case in intervals

  Show description for 069d113
  

  NlightNFotis

  authored and

  Thomas Kiley

  committed
  069d113

  Copy full SHA for 069d113

• (INT) Fix bitwise operators for intervals

  Show description for b07f98a
  

  NlightNFotis

  authored and

  Thomas Kiley

  committed
  b07f98a

  Copy full SHA for b07f98a

• (INT) Make eval in constant_interval_exprt const

  

  danpoe

  authored and

  Thomas Kiley

  committed
  f64591c

  Copy full SHA for f64591c

• (INT) Removed unimplemented function from util/interval.h

  

  danpoe

  authored and

  Thomas Kiley

  committed
  0258968

  Copy full SHA for 0258968

• (INT) accept false of ID_bool as valid zero value

  

  danpoe

  authored and

  Thomas Kiley

  committed
  0d37802

  Copy full SHA for 0d37802

• (INT) Add ID_bool type preconditions to logical interval operations

  

  danpoe

  authored and

  Thomas Kiley

  committed
  053c0c4

  Copy full SHA for 053c0c4

• (INT) use tvt_to_interval instead of tv_to_interval in constant_interval_exprt

  

  danpoe

  authored and

  Thomas Kiley

  committed
  ed2ae28

  Copy full SHA for ed2ae28

• (INT) Handle typecasts in constant_interval_exprt

  

  danpoe

  authored and

  Thomas Kiley

  committed
  8623c59

  Copy full SHA for 8623c59

• (INT) Typecast from ID_bool to integer types

  

  martin

  authored and

  Thomas Kiley

  committed
  f7b19a9

  Copy full SHA for f7b19a9

• (INT) Addressing review comments

  

  martin

  authored and

  Thomas Kiley

  committed
  140abbf

  Copy full SHA for 140abbf

• (INT) Add well-formedness checks for constant_interval_exprt

  

  danpoe

  authored and

  Thomas Kiley

  committed
  9caf96a

  Copy full SHA for 9caf96a

• (INT) Extend interval multiplication for extremes

  

  Petr Bauch

  authored and

  Thomas Kiley

  committed
  db7df69

  Copy full SHA for db7df69

• (INT) Add support for bit field and enums intervals.cpp

  

  martin

  authored and

  Thomas Kiley

  committed
  bbfb1bb

  Copy full SHA for bbfb1bb

• (INT) Fix broken interval unit tests

  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  fba3a55

  Copy full SHA for fba3a55

• (INT) Fix bug with interval typecasts

  Show description for f19ad6a
  

  hannes-steffenhagen-diffblue

  authored and

  Thomas Kiley

  committed
  f19ad6a

  Copy full SHA for f19ad6a

• (INT) Fixup for nil_typet being removed

  

  chrisr-diffblue

  authored and

  Thomas Kiley

  committed
  8558abd

  Copy full SHA for 8558abd

• (INT) Fixups post-rebase

  

  martin

  authored and

  Thomas Kiley

  committed
  0eb8cef

  Copy full SHA for 0eb8cef

• Fixes for the linter.

  

  martin

  authored and

  Thomas Kiley

  committed
  3477c38

  Copy full SHA for 3477c38

• Sort makefile includes

  

  Thomas Kiley

  committed
  368fc66

  Copy full SHA for 368fc66

• Add missing unit test to the Makefile

  

  Thomas Kiley

  committed
  ea981ce

  Copy full SHA for ea981ce

• Adapt unit tests for consistent interface

  Show description for 0e5f919
  

  Thomas Kiley

  committed
  0e5f919

  Copy full SHA for 0e5f919

• Add tests for divide

  

  Thomas Kiley

  committed
  1cd26b4

  Copy full SHA for 1cd26b4

• Add missing test coverage for unary operations

  

  Thomas Kiley

  committed
  50fae45

  Copy full SHA for 50fae45

• Add missing coverage for multiply

  

  Thomas Kiley

  committed
  b9d3dcf

  Copy full SHA for b9d3dcf

• Fix equality

  Show description for bd34f7d
  

  Thomas Kiley

  committed
  bd34f7d

  Copy full SHA for bd34f7d

• Fix printing code

  Show description for 813c5b5
  

  Thomas Kiley

  committed
  813c5b5

  Copy full SHA for 813c5b5

• Fix typo in unary plus tests for min and max

  

  Thomas Kiley

  committed
  2c43d53

  Copy full SHA for 2c43d53

• Disable unary minus tests on ranges

  Show description for b62d567
  

  Thomas Kiley

  committed
  b62d567

  Copy full SHA for b62d567

• Adapt test for bitwise not on a range

  Show description for 481f181
  

  Thomas Kiley

  committed
  481f181

  Copy full SHA for 481f181

• Tidy up shift test

  

  Thomas Kiley

  committed
  c1f60ad

  Copy full SHA for c1f60ad

• Add remaining shift tests

  Show description for 763b906
  

  Thomas Kiley

  committed
  763b906

  Copy full SHA for 763b906

• Add missing tests for increment

  

  Thomas Kiley

  committed
  a0cff82

  Copy full SHA for a0cff82

• Add missing bitwise tests for actual intervals

  

  Thomas Kiley

  committed
  3722357

  Copy full SHA for 3722357

• Add missing comparator tests

  

  Thomas Kiley

  committed
  cc83805

  Copy full SHA for cc83805

• Add tests for definitely_true/false for numeric intervals

  

  Thomas Kiley

  committed
  d838704

  Copy full SHA for d838704

• Add missing tests for modulo

  

  Thomas Kiley

  committed
  1faf516

  Copy full SHA for 1faf516

• Add tests for equality and inequality

  

  Thomas Kiley

  committed
  7c16a14

  Copy full SHA for 7c16a14

• Fix error in binary eval for subtraction

  Show description for 2d067f2
  

  Thomas Kiley

  committed
  2d067f2

  Copy full SHA for 2d067f2

• Add test case for eval on binary operations

  

  Thomas Kiley

  committed
  39edeea

  Copy full SHA for 39edeea

• Add tests for the to_string operation

  

  Thomas Kiley

  committed
  a84494c

  Copy full SHA for a84494c

• fixup binary eval unit test commit

  

  Thomas Kiley

  committed
  7f61939

  Copy full SHA for 7f61939

• Tidy the test for unary minus

  

  Thomas Kiley

  committed
  42e2d5a

  Copy full SHA for 42e2d5a

• Make the equality comparison test easier to follow

  

  Thomas Kiley

  committed
  536fc46

  Copy full SHA for 536fc46

• Add a comment explaining that modulo is imprecise

  

  Thomas Kiley

  committed
  296fe68

  Copy full SHA for 296fe68

• Do a full check on the multiply test

  

  Thomas Kiley

  committed
  1d92ca0

  Copy full SHA for 1d92ca0