Code

Merge develop 20170914#1388

Code

Merged

smowton merged 101 commits intodiffblue:security-scanner-supportdiffblue/cbmc:security-scanner-supportfrom

smowton:merge-develop-20170914smowton/cbmc:merge-develop-20170914Copy head branch name to clipboard

Sep 14, 2017

Commits

Commits on Sep 4, 2017

• Add nonstd/optional.hpp library

  

  Lukasz A.J. Wrona

  committed
  8584bb0

  Copy full SHA for 8584bb0

• Add unit tests for nonstd::optional

  

  Lukasz A.J. Wrona

  committed
  43d0602

  Copy full SHA for 43d0602

• Manually fix optional

  

  Lukasz A.J. Wrona

  committed
  4dbf939

  Copy full SHA for 4dbf939

• Move optional unit tests into util directory

  

  Lukasz A.J. Wrona

  committed
  ae584df

  Copy full SHA for ae584df

Commits on Sep 6, 2017

• Make goto_modelt.output const

  

  janmroczkowski

  committed
  ebbbf5f

  Copy full SHA for ebbbf5f

• Make basic_blockst.output const

  

  janmroczkowski

  committed
  567eaa7

  Copy full SHA for 567eaa7

• Make automatont.output const

  

  janmroczkowski

  committed
  9be84ea

  Copy full SHA for 9be84ea

• Make path_nodet.output const

  

  janmroczkowski

  committed
  211fcc2

  Copy full SHA for 211fcc2

• Make uncaught_exceptions_analysis.output const

  

  janmroczkowski

  committed
  388a25e

  Copy full SHA for 388a25e

Commits on Sep 7, 2017

• Merge pull request #1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const

  Show description for 254f133
  

  Daniel Kroening

  authored
  254f133

  Copy full SHA for 254f133

• Remove long-deprecated c_sizeof in favour of size_of_expr et al.

  tautschnig

  committed
  d79067e

  Copy full SHA for d79067e

• sizeof(*(void*)) is sizeof(char)

  tautschnig

  committed
  1fa569f

  Copy full SHA for 1fa569f

• Fix type casts from initializer lists to arrays of unspecified size

  tautschnig

  committed
  3273bf5

  Copy full SHA for 3273bf5

• When possible, update array types before typechecking initializer

  Show description for 3613ebc
  tautschnig

  committed
  3613ebc

  Copy full SHA for 3613ebc

• clean out an unused method

  

  Daniel Kroening

  committed
  f6d94cf

  Copy full SHA for f6d94cf

• Add dry-run mode to test.pl

  Show description for 296349c
  smowton

  committed
  296349c

  Copy full SHA for 296349c

• Modified verbosity for loaded message

  Show description for 359a3e3
  

  thk123

  committed
  359a3e3

  Copy full SHA for 359a3e3

• Merge pull request #1358 from thk123/feature/decrease-message-spam

  Show description for 56b5e25
  

  Daniel Kroening

  authored
  56b5e25

  Copy full SHA for 56b5e25

• Merge pull request #1356 from smowton/smowton/feature/test_pl_add_dry_run

  Show description for 1c8d81a
  smowton

  authored
  1c8d81a

  Copy full SHA for 1c8d81a

• Remove unused files

  reuk

  committed
  2217501

  Copy full SHA for 2217501

Commits on Sep 8, 2017

• Merge pull request #1333 from tautschnig/remove-c_sizeof

  Show description for 5863a75
  tautschnig

  authored
  5863a75

  Copy full SHA for 5863a75

• Diagnostic output if run/execve fails

  tautschnig

  committed
  4928f69

  Copy full SHA for 4928f69

• Make the child process that failed to execvp exit

  Show description for 08a4077
  tautschnig

  committed
  08a4077

  Copy full SHA for 08a4077

• Merge pull request #1321 from reuk/reuk/remove-unused-files

  Show description for 435c0bf
  tautschnig

  authored
  435c0bf

  Copy full SHA for 435c0bf

• Merge pull request #1245 from tautschnig/run-diagnostic

  Show description for c125146
  

  Daniel Kroening

  authored
  c125146

  Copy full SHA for c125146

• simplify API of goto_convert

  

  Daniel Kroening

  committed
  40fe0f8

  Copy full SHA for 40fe0f8

• use initialize_goto_model in CBMC/goto-analyse/etc

  

  Daniel Kroening

  committed
  9469552

  Copy full SHA for 9469552

• use goto_modelt

  

  Daniel Kroening

  committed
  fc4d44a

  Copy full SHA for fc4d44a

• brief list of symbols, from language_uit

  

  Daniel Kroening

  committed
  e4498ca

  Copy full SHA for e4498ca

• remove spurious references to langapi/language_ui.h

  

  Daniel Kroening

  committed
  8c4ff7b

  Copy full SHA for 8c4ff7b

• missing copyright header

  

  Daniel Kroening

  committed
  7d30cde

  Copy full SHA for 7d30cde

Commits on Sep 10, 2017

• pthread_create arguments null/nonnull fix

  

  Daniel Kroening

  committed
  fe60e60

  Copy full SHA for fe60e60

Commits on Sep 11, 2017

• Disable Alpine in Travis

  reuk

  committed
  95c5e63

  Copy full SHA for 95c5e63

• clean-out ill-modeled optimization in string comparisons

  

  Daniel Kroening

  committed
  3ddd377

  Copy full SHA for 3ddd377

• Merge pull request #1291 from LAJW/optional

  Show description for b846858
  

  Daniel Kroening

  authored
  b846858

  Copy full SHA for b846858

• Map wrappers: forward more of the std::map interface

  Show description for 6facf74
  smowton

  committed
  6facf74

  Copy full SHA for 6facf74

• Add CMakeLists

  reuk

  committed
  22c2ab9

  Copy full SHA for 22c2ab9

• Add CMake howto to COMPILING file

  reuk

  committed
  e609bbb

  Copy full SHA for e609bbb

• Enable running tests from CMake

  reuk

  committed
  f6e4968

  Copy full SHA for f6e4968

• Enable CMake in Travis

  reuk

  committed
  3c36aa5

  Copy full SHA for 3c36aa5

• Fix and refactor library_check target

  reuk

  committed
  6251055

  Copy full SHA for 6251055

• Enable caching for CMake builds (hopefully)

  reuk

  committed
  d953327

  Copy full SHA for d953327

• Disable 32-bit builds in Travis

  reuk

  committed
  9afbced

  Copy full SHA for 9afbced

• Quote paths in flex/bison commands

  reuk

  committed
  5afa929

  Copy full SHA for 5afa929

• Set up glucose externalproject

  reuk

  committed
  ad486f8

  Copy full SHA for ad486f8

• Control SAT library from makefiles

  reuk

  committed
  5ee349f

  Copy full SHA for 5ee349f

• Make CMake release flags similar to Makefile build

  reuk

  committed
  7d4e9b5

  Copy full SHA for 7d4e9b5

• Clean up CMake files after #1321

  reuk

  committed
  91684da

  Copy full SHA for 91684da

• Disable glucose in Travis

  reuk

  committed
  4dde3c5

  Copy full SHA for 4dde3c5

• Merge pull request #1365 from smowton/smowton/feature/more_map_forwarding

  Show description for 8782103
  smowton

  authored
  8782103

  Copy full SHA for 8782103

• Remove PRE_COMMAND scaffolding

  reuk

  committed
  0cfd7b0

  Copy full SHA for 0cfd7b0

• Merge pull request #1364 from diffblue/phread-create-fix

  Show description for 4febd10
  

  Daniel Kroening

  authored
  4febd10

  Copy full SHA for 4febd10

• Merge pull request #1339 from diffblue/initialize_goto_model

  Show description for 73b4357
  

  Daniel Kroening

  authored
  73b4357

  Copy full SHA for 73b4357

• Merge pull request #1367 from reuk/reuk/disable-alpine-in-travis

  Show description for 728ac5b
  

  Daniel Kroening

  authored
  728ac5b

  Copy full SHA for 728ac5b

Commits on Sep 12, 2017

• use __CPROVER_assert

  

  Daniel Kroening

  committed
  8fc714d

  Copy full SHA for 8fc714d

• output statements

  

  Daniel Kroening

  committed
  3896110

  Copy full SHA for 3896110

• comments on test

  

  Daniel Kroening

  committed
  211355d

  Copy full SHA for 211355d

• remove_returns missing in symex

  

  Daniel Kroening

  committed
  746bff5

  Copy full SHA for 746bff5

• option is now --trace

  

  Daniel Kroening

  committed
  430218f

  Copy full SHA for 430218f

• avoid confusion between SSA lhs and full lhs during assignment

  

  Daniel Kroening

  committed
  5195d24

  Copy full SHA for 5195d24

• enable symex regression testing

  

  Daniel Kroening

  committed
  5d2d07b

  Copy full SHA for 5d2d07b

• Merge pull request #1373 from diffblue/symex-trace-fix

  Show description for 8cd4490
  

  Daniel Kroening

  authored
  8cd4490

  Copy full SHA for 8cd4490

• added symex to Appveyor build

  

  Daniel Kroening

  committed
  6a2fd50

  Copy full SHA for 6a2fd50

Commits on Sep 13, 2017

• revert symex regression until Appvoyer works

  

  Daniel Kroening

  committed
  2816b80

  Copy full SHA for 2816b80

• Account for replaced functions in exceptions_map

  Show description for 0496142
  pkesseli

  committed
  0496142

  Copy full SHA for 0496142

• Attempt to fix the symex appveyor build

  Show description for e73a884
  

  thk123

  committed
  e73a884

  Copy full SHA for e73a884

• Reverting manually commited fixes

  

  thk123

  committed
  af8d46f

  Copy full SHA for af8d46f

• remove musketeer

  

  Daniel Kroening

  committed
  a31f1d9

  Copy full SHA for a31f1d9

• Merge pull request #1375 from pkesseli/bugfix/uncaught-exceptions-invariant

  Show description for 41bafc0
  peterschrammel

  authored
  41bafc0

  Copy full SHA for 41bafc0

• Manually disable some failing tests

  Show description for 91e733d
  

  thk123

  committed
  91e733d

  Copy full SHA for 91e733d

• Add initial value to languaget::generate_opaque_stubs

  Show description for 444f256
  pkesseli

  committed
  444f256

  Copy full SHA for 444f256

• Merge pull request #1378 from thk123/bugfix/fix-symex-appveyor

  Show description for d45325c
  peterschrammel

  authored
  d45325c

  Copy full SHA for d45325c

• Merge pull request #1382 from pkesseli/bugfix/language-opaque-stubs

  Show description for 69d05a9
  peterschrammel

  authored
  69d05a9

  Copy full SHA for 69d05a9

• Cause a regeneration of the entry method if a --function is provided

  Show description for f347a22
  

  thk123

  committed
  f347a22

  Copy full SHA for f347a22

• Adding explanatory comment

  

  thk123

  committed
  2a3d876

  Copy full SHA for 2a3d876

• Protect against invalid function label

  Show description for ee5fb93
  

  thk123

  committed
  ee5fb93

  Copy full SHA for ee5fb93

• Call generate_start_function only when regenerating the start function

  Show description for cd416bc
  

  thk123

  committed
  cd416bc

  Copy full SHA for cd416bc

• Implemented generate_start_function for Java

  Show description for 94b7185
  

  thk123

  committed
  94b7185

  Copy full SHA for 94b7185

• Added regression test for using --function on a GOTO program

  Show description for 71e6800
  

  thk123

  committed
  71e6800

  Copy full SHA for 71e6800

• Refactored the regenerate function into goto-programs

  Show description for f0d6d72
  

  thk123

  committed
  f0d6d72

  Copy full SHA for f0d6d72

• Made generate_start_function abstract

  Show description for 2aea88d
  

  thk123

  committed
  2aea88d

  Copy full SHA for 2aea88d

• Use ID_main as the default name for entry function

  Show description for 71dec3d
  

  thk123

  committed
  71dec3d

  Copy full SHA for 71dec3d

• Adding missing overrides

  Show description for 0732580
  

  thk123

  committed
  0732580

  Copy full SHA for 0732580

• Add support for using the --function flag to goto-analyze and symex

  Show description for 1ccd1a2
  

  thk123

  committed
  1ccd1a2

  Copy full SHA for 1ccd1a2

• Fixing the method to work with java_bytecode

  Show description for dee89b0
  

  thk123

  committed
  dee89b0

  Copy full SHA for dee89b0

• Weaked the tests for pointer-function-parameters

  Show description for 15b89fc
  

  thk123

  committed
  15b89fc

  Copy full SHA for 15b89fc

• Disable failing test in the symex directory

  

  thk123

  committed
  e37d3d5

  Copy full SHA for e37d3d5

• Ensure symex and goto-analyzer regenerate functions

  

  thk123

  committed
  c6f1430

  Copy full SHA for c6f1430

• Corrected doxygen errors

  

  thk123

  committed
  92a52a5

  Copy full SHA for 92a52a5

• Merge pull request #1293 from reuk/cmake-develop

  Show description for 3ede81b
  peterschrammel

  authored
  3ede81b

  Copy full SHA for 3ede81b

• Correcting windows build

  

  thk123

  committed
  22f06fd

  Copy full SHA for 22f06fd

• Merge pull request #1380 from diffblue/remove-musketeer

  Show description for f77822b
  peterschrammel

  authored
  f77822b

  Copy full SHA for f77822b

• Regenerate malformed binary blobs

  reuk

  committed
  a46ad62

  Copy full SHA for a46ad62

• Ensure pointer invariants are maintained

  reuk

  committed
  a9806c0

  Copy full SHA for a9806c0

• Use PRECONDITION in std_types.h

  reuk

  committed
  81f1300

  Copy full SHA for 81f1300

• Fix up CMake build (unrelated)

  reuk

  committed
  00e4555

  Copy full SHA for 00e4555

Commits on Sep 14, 2017

• Merge pull request #1374 from reuk/reuk/maintain-pointer-invariants

  Show description for 63c9a1e
  

  Joel Allred

  authored
  63c9a1e

  Copy full SHA for 63c9a1e

• Merge pull request #338 from thk123/bug/function-flag-on-goto-program

  Show description for e54c0e9
  

  Thomas Kiley

  authored
  e54c0e9

  Copy full SHA for e54c0e9

• Re-enable old function signatures for test-gen compat

  reuk

  committed
  1264b4d

  Copy full SHA for 1264b4d

• Merge pull request #1383 from reuk/reuk/sync-projects

  Show description for 4df244c
  

  Joel Allred

  authored
  4df244c

  Copy full SHA for 4df244c

• Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914

  smowton

  committed
  e3f3abd

  Copy full SHA for e3f3abd