Code

Merge master 20170705#1094

Code

Merged

smowton merged 91 commits intodiffblue:test-gen-supportdiffblue/cbmc:test-gen-supportfrom

smowton:merge_master_20170705smowton/cbmc:merge_master_20170705Copy head branch name to clipboard

Jul 7, 2017

Commits

Commits on May 24, 2017

• Adapt existing regression tests

  

  Matthias Güdemann

  committed
  c93cb8c

  Copy full SHA for c93cb8c

• Add regression tests for `iload`, `dup`, `dup_x1`, `dup_x2`

  

  Matthias Güdemann

  committed
  4c17377

  Copy full SHA for 4c17377

• Add regression tests for `dup2`, `dup2_x1` and `dup2_x2`

  

  Matthias Güdemann

  committed
  21cd8a5

  Copy full SHA for 21cd8a5

• Add regression test for `getfield`, `getstatic`

  

  Matthias Güdemann

  committed
  953fb43

  Copy full SHA for 953fb43

• Add regression test for ?store

  

  Matthias Güdemann

  committed
  0b81ed6

  Copy full SHA for 0b81ed6

• Add regression test for ?astore

  

  Matthias Güdemann

  committed
  9368613

  Copy full SHA for 9368613

• Add README to tests pointing to jasmin bytecode assembler

  

  Matthias Güdemann

  committed
  b5cbb7f

  Copy full SHA for b5cbb7f

Commits on May 25, 2017

• Add temporary variables for values on stack for write operations

  Show description for 0ce085f
  

  Matthias Güdemann

  committed
  0ce085f

  Copy full SHA for 0ce085f

Commits on May 30, 2017

• Assign function in instructions introduced by MM I/O instrumentation

  Show description for 2f29c99
  peterschrammel

  committed
  2f29c99

  Copy full SHA for 2f29c99

Commits on Jun 7, 2017

• MinGW GCC defines __int64 for Visual-Studio compatibility

  tautschnig

  committed
  afff4a7

  Copy full SHA for afff4a7

• A first cut at the additions we need to the math library.

  

  martin

  authored and

  tautschnig

  committed
  9f23c25

  Copy full SHA for 9f23c25

• An alternative implementation to avoid the difference between RNE and RNA.

  

  martin

  authored and

  tautschnig

  committed
  0777675

  Copy full SHA for 0777675

• Fix special cases for the remainder functions, now down to 4 failures!

  

  martin

  authored and

  tautschnig

  committed
  e821efe

  Copy full SHA for e821efe

• Support "polymorphic" floating-point functions, fix typos

  Show description for 45d7f08
  tautschnig

  committed
  45d7f08

  Copy full SHA for 45d7f08

Commits on Jun 8, 2017

• Add --print-internal-representation to goto-instrument

  Show description for 6822afa
  karkhaz

  committed
  6822afa

  Copy full SHA for 6822afa

Commits on Jun 12, 2017

• Stop attempting to convert previously-converted headers

  reuk

  committed
  a6c32b0

  Copy full SHA for a6c32b0

Commits on Jun 13, 2017

• Remove duplication from conversion script

  reuk

  committed
  bec818e

  Copy full SHA for bec818e

• Added test for array containing a zero struct

  Show description for e8202d9
  

  thk123

  committed
  e8202d9

  Copy full SHA for e8202d9

• Improved the interface of remove_const_functions

  Show description for ab23684
  

  thk123

  committed
  ab23684

  Copy full SHA for ab23684

• Making the approx and precise FP removal tests more precise

  Show description for e2049b0
  

  thk123

  committed
  e2049b0

  Copy full SHA for e2049b0

• Fixed null pointer related bug

  Show description for d7e4a35
  

  thk123

  committed
  d7e4a35

  Copy full SHA for d7e4a35

• Replace assert with appropriate invariant

  

  thk123

  committed
  8ec1890

  Copy full SHA for 8ec1890

Commits on Jun 15, 2017

• Force simplification of cast-from-universal-integer

  Show description for 30866b5
  smowton

  committed
  30866b5

  Copy full SHA for 30866b5

• Add script to find linkerscript-defined info

  Show description for 6cd9693
  karkhaz

  committed
  6cd9693

  Copy full SHA for 6cd9693

Commits on Jun 16, 2017

• Added a 't' to the name of interval_template to be consistent with general naming style

  

  Daniel Neville

  committed
  7c849cd

  Copy full SHA for 7c849cd

Commits on Jun 18, 2017

• Merge pull request #1025 from DanielNeville/danielneville/fix/add_t_to_interval_template

  Show description for f21ff7f
  

  Daniel Kroening

  authored
  f21ff7f

  Copy full SHA for f21ff7f

• Merge pull request #1022 from karkhaz/ls-parse-script

  Show description for a2a143a
  

  Daniel Kroening

  authored
  a2a143a

  Copy full SHA for a2a143a

• Merge pull request #1005 from reuk/script-update

  Show description for 17e5963
  

  Daniel Kroening

  authored
  17e5963

  Copy full SHA for 17e5963

• Merge pull request #991 from karkhaz/pretty-print

  Show description for 1b58ff9
  

  Daniel Kroening

  authored
  1b58ff9

  Copy full SHA for 1b58ff9

• Merge pull request #951 from mgudemann/fix/bytecode_args_write_from_stack

  Show description for a71dfb5
  

  Daniel Kroening

  authored
  a71dfb5

  Copy full SHA for a71dfb5

Commits on Jun 19, 2017

• Use empty() instead of size()==0, size()<1

  Show description for 9d991b4
  tautschnig

  committed
  9d991b4

  Copy full SHA for 9d991b4

• Add test for Java integers with --no-simplify

  Show description for e2e2360
  smowton

  committed
  e2e2360

  Copy full SHA for e2e2360

• Fix sipush return type annotation

  Show description for 167636f
  smowton

  committed
  167636f

  Copy full SHA for 167636f

• Don't warn on array_of_expr with zero length

  Show description for 40fb6a0
  smowton

  committed
  40fb6a0

  Copy full SHA for 40fb6a0

• Add zero-length array test

  Show description for 677f39d
  smowton

  committed
  677f39d

  Copy full SHA for 677f39d

• Merge pull request #1032 from tautschnig/empty-cleanup

  Show description for e2204fc
  

  Daniel Kroening

  authored
  e2204fc

  Copy full SHA for e2204fc

• Merge pull request #733 from tautschnig/float-lib

  Show description for c897e06
  

  Daniel Kroening

  authored
  c897e06

  Copy full SHA for c897e06

• Add empty() to grapht as it implements size(), bug-fix

  Show description for 7039018
  tautschnig

  committed
  7039018

  Copy full SHA for 7039018

• Merge pull request #1034 from diffblue/smowton/fix/sipush_return_type

  Show description for dd8ed06
  

  Daniel Kroening

  authored
  dd8ed06

  Copy full SHA for dd8ed06

• Merge pull request #1040 from tautschnig/fix-1032

  Show description for 7dbb203
  

  Daniel Kroening

  authored
  7dbb203

  Copy full SHA for 7dbb203

• add empty() to container-like classes with size()

  

  Daniel Kroening

  committed
  2c84b3a

  Copy full SHA for 2c84b3a

• missing header

  

  Daniel Kroening

  committed
  7181e41

  Copy full SHA for 7181e41

• Merge pull request #1041 from diffblue/add_empty

  Show description for 0bc503a
  tautschnig

  authored
  0bc503a

  Copy full SHA for 0bc503a

• Fix typing in signed/unsigned comparison

  tautschnig

  committed
  8542736

  Copy full SHA for 8542736

Commits on Jun 21, 2017

• detect missing message handler, and set a missing one

  

  Daniel Kroening

  committed
  ed15077

  Copy full SHA for ed15077

Commits on Jun 23, 2017

• Merge pull request #1016 from diffblue/smowton/fix/java_integers_without_simplify

  Show description for e0b4515
  

  Daniel Kroening

  authored
  e0b4515

  Copy full SHA for e0b4515

Commits on Jun 28, 2017

• Expansion of array_replace/array_copy must not drop offsets

  tautschnig

  committed
  03347eb

  Copy full SHA for 03347eb

• Fix removal of first component

  Show description for 78a23bb
  pkesseli

  committed
  78a23bb

  Copy full SHA for 78a23bb

• Taints cannot currently be tracked across undefined functions

  tautschnig

  committed
  76fa413

  Copy full SHA for 76fa413

• Add bytecode files for non-public classes

  Show description for 07841f7
  tautschnig

  committed
  07841f7

  Copy full SHA for 07841f7

• Source locations have function names

  tautschnig

  committed
  29dd3f1

  Copy full SHA for 29dd3f1

• Move taint tests to goto-analyzer folder to ensure they are used

  Show description for 34e6b04
  tautschnig

  committed
  34e6b04

  Copy full SHA for 34e6b04

• Make the custom bitvector analysis actually work

  Show description for 5d84b1f
  tautschnig

  committed
  5d84b1f

  Copy full SHA for 5d84b1f

• Propagate bitvector analysis state across function calls

  tautschnig

  committed
  10822d4

  Copy full SHA for 10822d4

• Split up gen_nondet_init function

  Show description for 5a88619
  

  thk123

  committed
  5a88619

  Copy full SHA for 5a88619

• Split up gen_nondet_init for structs

  Show description for f4e8a9a
  

  thk123

  committed
  f4e8a9a

  Copy full SHA for f4e8a9a

• Added missing comment to class_hieracrchyt

  

  thk123

  committed
  0547fae

  Copy full SHA for 0547fae

• Correcting assertions

  Show description for e873e00
  

  thk123

  committed
  e873e00

  Copy full SHA for e873e00

Commits on Jun 29, 2017

• Merge pull request #1068 from tautschnig/fix-array-replace

  Show description for 745a9b9
  

  Daniel Kroening

  authored
  745a9b9

  Copy full SHA for 745a9b9

Commits on Jun 30, 2017

• Merge pull request #1027 from thk123/refactor/gen-nondet-init-master

  Show description for 9d232d4
  

  Daniel Kroening

  authored
  9d232d4

  Copy full SHA for 9d232d4

• Updated doxyfile to a modern version

  Show description for b72cf31
  cesaro

  committed
  b72cf31

  Copy full SHA for b72cf31

Commits on Jul 3, 2017

• Merge pull request #1074 from cesaro/feature/update-doxyfile

  Show description for 7f4599f
  

  Daniel Kroening

  authored
  7f4599f

  Copy full SHA for 7f4599f

• Merge pull request #1039 from tautschnig/signed-unsigned

  Show description for e1c313d
  

  Daniel Kroening

  authored
  e1c313d

  Copy full SHA for e1c313d

• Merge pull request #1013 from smowton/smowton/fix/array_of_zero_length

  Show description for 1cb1fd9
  

  Daniel Kroening

  authored
  1cb1fd9

  Copy full SHA for 1cb1fd9

• dump-c: Try to guess further system headers

  tautschnig

  committed
  5938ecb

  Copy full SHA for 5938ecb

• Typedef names are symbols

  Show description for c54ddb8
  tautschnig

  committed
  c54ddb8

  Copy full SHA for c54ddb8

• Fix dump-c output involving typedef names

  Show description for dc5ae8c
  tautschnig

  committed
  dc5ae8c

  Copy full SHA for dc5ae8c

• No special handling of $link. This might appear due to unknown reasons.

  

  stahlbauer

  authored and

  tautschnig

  committed
  f56a398

  Copy full SHA for f56a398

• Do not dump certain types if they are defined in system headers

  

  stahlbauer

  authored and

  tautschnig

  committed
  2aa140c

  Copy full SHA for 2aa140c

• Do not dump anonymous types from system headers

  Show description for b0e0c0a
  

  stahlbauer

  authored and

  tautschnig

  committed
  b0e0c0a

  Copy full SHA for b0e0c0a

• Dump the global declarations after the included system headers

  

  stahlbauer

  authored and

  tautschnig

  committed
  ac270c5

  Copy full SHA for ac270c5

• Locate var args use even when va_arg_next is not used

  Show description for fe04e59
  tautschnig

  committed
  fe04e59

  Copy full SHA for fe04e59

• Output _Noreturn qualifier at appropriate place

  tautschnig

  committed
  0428f6a

  Copy full SHA for 0428f6a

• Do not dump internal $object declarations

  Show description for 3a57645
  tautschnig

  committed
  3a57645

  Copy full SHA for 3a57645

• Output float literals in a GCC-compatible fashion

  Show description for f6509c3
  tautschnig

  committed
  f6509c3

  Copy full SHA for f6509c3

• bswap is not a library function; use __builtin_bswap[bit-suffix] instead

  tautschnig

  committed
  ad55c4f

  Copy full SHA for ad55c4f

• Improve --use-system-headers output for GCC compatibility

  Show description for a9dca20
  tautschnig

  committed
  a9dca20

  Copy full SHA for a9dca20

• dump-c: respect local translation bounds in resolving switch/case

  tautschnig

  committed
  38b4c48

  Copy full SHA for 38b4c48

• Use invariant annotations instead of asserts

  tautschnig

  committed
  e2cfed3

  Copy full SHA for e2cfed3

• Merge pull request #885 from tautschnig/mingw-__int64

  Show description for 3433dc6
  

  Daniel Kroening

  authored
  3433dc6

  Copy full SHA for 3433dc6

• Merge pull request #977 from peterschrammel/bugfix/mm-io-instruction-function

  Show description for acc42c5
  

  Daniel Kroening

  authored
  acc42c5

  Copy full SHA for acc42c5

• Merge pull request #1038 from pkesseli/cpplint/header-guard-first-component

  Show description for 3c896fd
  

  Daniel Kroening

  authored
  3c896fd

  Copy full SHA for 3c896fd

• Merge pull request #1009 from thk123/bugfix/arrays-structs-null-pointers

  Show description for eac8e2c
  

  Daniel Kroening

  authored
  eac8e2c

  Copy full SHA for eac8e2c

• dump-c: Replace --use-system-headers by --no-system-headers

  Show description for 34a476f
  tautschnig

  committed
  34a476f

  Copy full SHA for 34a476f

• Reset unwinding counters when leaving a loop at the loop head

  Show description for a4945f3
  tautschnig

  committed
  a4945f3

  Copy full SHA for a4945f3

• Partly revert to try out more beautiful approach

  tautschnig

  committed
  5fc1ca6

  Copy full SHA for 5fc1ca6

• Merge pull request #999 from tautschnig/fix-taint

  Show description for 7ef0091
  

  Daniel Kroening

  authored
  7ef0091

  Copy full SHA for 7ef0091

• Merge pull request #858 from tautschnig/dump-c-typedef

  Show description for c7ce527
  

  Daniel Kroening

  authored
  c7ce527

  Copy full SHA for c7ce527

• Initialise loop counters at loop entry

  Show description for 21afd2f
  tautschnig

  committed
  21afd2f

  Copy full SHA for 21afd2f

Commits on Jul 4, 2017

• Merge pull request #988 from tautschnig/fix-unwind-count

  Show description for 32b68ce
  

  Daniel Kroening

  authored
  32b68ce

  Copy full SHA for 32b68ce

Commits on Jul 7, 2017

• Merge remote-tracking branch 'upstream/master' into merge_master_20170705

  smowton

  committed
  0e1b95c

  Copy full SHA for 0e1b95c