Code

Smowton/merge/master 20170614#1012

Code

Merged

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

smowton:smowton/merge/master_20170614smowton/cbmc:smowton/merge/master_20170614Copy head branch name to clipboard

Jun 14, 2017

Commits

Commits on Apr 18, 2017

• Java object factory: allocate fixed length arrays

  Show description for 102885f
  smowton

  committed
  102885f

  Copy full SHA for 102885f

• Add assert to local_bitvector_analysis.cpp

  reuk

  committed
  2895408

  Copy full SHA for 2895408

Commits on May 10, 2017

• Fix SHARING behaviour

  reuk

  committed
  952680e

  Copy full SHA for 952680e

Commits on May 16, 2017

• Convert endl to newline in analyses

  reuk

  committed
  ba06a83

  Copy full SHA for ba06a83

• Convert endl to newline in ansi-c

  reuk

  committed
  1730b43

  Copy full SHA for 1730b43

• Convert endl to newline in cbmc

  reuk

  committed
  2e84835

  Copy full SHA for 2e84835

• Convert endl to newline in clobber

  reuk

  committed
  d5d53d9

  Copy full SHA for d5d53d9

• Convert endl to newline in cpp

  reuk

  committed
  fbef879

  Copy full SHA for fbef879

• Convert endl to newline in goto-analyzer

  reuk

  committed
  857f376

  Copy full SHA for 857f376

• Convert endl to newline in goto-cc

  reuk

  committed
  c7576bc

  Copy full SHA for c7576bc

• Convert endl to newline in goto-diff

  reuk

  committed
  9eb1af6

  Copy full SHA for 9eb1af6

• Convert endl to newline in goto-instrument

  reuk

  committed
  5b01890

  Copy full SHA for 5b01890

• Convert endl to newline in goto-programs

  reuk

  committed
  045ba9a

  Copy full SHA for 045ba9a

• Convert endl to newline in goto-symex

  reuk

  committed
  74f4a15

  Copy full SHA for 74f4a15

• Convert endl to newline in langapi

  reuk

  committed
  dba84f9

  Copy full SHA for dba84f9

• Convert endl to newline in memory-models

  reuk

  committed
  2d189a4

  Copy full SHA for 2d189a4

• Convert endl to newline in musketeer

  reuk

  committed
  a75b3a7

  Copy full SHA for a75b3a7

• Convert endl to newline in path-symex

  reuk

  committed
  fa18b08

  Copy full SHA for fa18b08

• Convert endl to newline in pointer-analysis

  reuk

  committed
  27ca1ad

  Copy full SHA for 27ca1ad

• Convert endl to newline in solvers

  reuk

  committed
  5758a9d

  Copy full SHA for 5758a9d

• Convert endl to newline in symex

  reuk

  committed
  4d4261b

  Copy full SHA for 4d4261b

• Convert endl to newline in util

  reuk

  committed
  e612c09

  Copy full SHA for e612c09

• Update linter to find std::endl

  reuk

  committed
  a0ef01a

  Copy full SHA for a0ef01a

Commits on May 20, 2017

• Merge pull request #908 from reuk/enable-sharing

  Show description for 1af075c
  

  Daniel Kroening

  authored
  1af075c

  Copy full SHA for 1af075c

• Merge pull request #838 from reuk/bitvector-analysis-assert

  Show description for 588ed05
  

  Daniel Kroening

  authored
  588ed05

  Copy full SHA for 588ed05

• Merge pull request #891 from reuk/endl

  Show description for 3a3e5a3
  

  Daniel Kroening

  authored
  3a3e5a3

  Copy full SHA for 3a3e5a3

• Merge pull request #839 from smowton/smowton/feature/fixed_length_nondet_arrays

  Show description for a486804
  

  Daniel Kroening

  authored
  a486804

  Copy full SHA for a486804

Commits on May 21, 2017

• Adding preprocessing for functions of the Java Character library

  Show description for 57a262c
  romainbrenguier

  committed
  57a262c

  Copy full SHA for 57a262c

• Call to character preprocessing from java_bytecode

  romainbrenguier

  committed
  924e01b

  Copy full SHA for 924e01b

• Merge pull request #640 from romainbrenguier/java-character-library-support

  Show description for 9ec55a3
  

  Daniel Kroening

  authored
  9ec55a3

  Copy full SHA for 9ec55a3

• Java is now a default

  

  Daniel Kroening

  committed
  a408f80

  Copy full SHA for a408f80

• advance the year

  

  Daniel Kroening

  committed
  d999e56

  Copy full SHA for d999e56

Commits on May 22, 2017

• Coverage report: include absolute lines covered and total per function

  Show description for 7b3c96f
  tautschnig

  committed
  7b3c96f

  Copy full SHA for 7b3c96f

• Fix coverage reporting of forward-goto statements (break, continue)

  Show description for 31be993
  tautschnig

  committed
  31be993

  Copy full SHA for 31be993

• goto-instrument --remove-function-body

  Show description for accc412
  tautschnig

  committed
  accc412

  Copy full SHA for accc412

• W3C compliance fixes

  

  Daniel Kroening

  committed
  9f2df28

  Copy full SHA for 9f2df28

• Merge branch 'master' of github.com:diffblue/cbmc

  

  Daniel Kroening

  committed
  0bc21fa

  Copy full SHA for 0bc21fa

• GCC 6 is no longer required

  Show description for eb68db4
  tautschnig

  committed
  eb68db4

  Copy full SHA for eb68db4

• Added missing generated_files target to jsil

  Show description for 167ffb8
  tautschnig

  committed
  167ffb8

  Copy full SHA for 167ffb8

• Use ai function output in goto-instrument.

  

  danpoe

  authored and

  martin

  committed
  baa5741

  Copy full SHA for baa5741

Commits on May 23, 2017

• Add output_json to the dependence_graph abstract domain.

  

  martin

  committed
  026f2de

  Copy full SHA for 026f2de

• Improve annotation of dependence graph declarations.

  

  martin

  committed
  4b6e59e

  Copy full SHA for 4b6e59e

• Add utility function for remove_unreachable.

  

  martin

  committed
  ffd6e55

  Copy full SHA for ffd6e55

• Fix formatting of comments in interval domain.

  

  martin

  committed
  ff65162

  Copy full SHA for ff65162

• White space fix up in test case.

  

  martin

  committed
  3b0266d

  Copy full SHA for 3b0266d

• Tests have been fixed in some past commits

  tautschnig

  committed
  60bea64

  Copy full SHA for 60bea64

• Make c_types widely available and avoid locally building types

  Show description for 20de0d7
  tautschnig

  committed
  20de0d7

  Copy full SHA for 20de0d7

• The sub-size of void* is undefined; use char* as specified in the standard

  Show description for 7f6443b
  tautschnig

  committed
  7f6443b

  Copy full SHA for 7f6443b

• cout/cerr message handlers are stream_message_handlert

  tautschnig

  committed
  d209b90

  Copy full SHA for d209b90

• Message handlers maintain counters of messages per level

  Show description for e3e74b0
  tautschnig

  committed
  e3e74b0

  Copy full SHA for e3e74b0

• Support flush at eom to ensure complete output

  tautschnig

  committed
  aa8c5e9

  Copy full SHA for aa8c5e9

• Removed legacy_typecheckt interface, use new message counters

  tautschnig

  committed
  70755fc

  Copy full SHA for 70755fc

• Removed legacy messaget interface, removed message_clientt

  tautschnig

  committed
  3a55283

  Copy full SHA for 3a55283

• Make goto-cc fail when warnings are emitted and -Werror and -Wextra are set

  Show description for 9e25eb4
  tautschnig

  committed
  9e25eb4

  Copy full SHA for 9e25eb4

• Pass message handler on to compilet

  Show description for c183996
  tautschnig

  committed
  c183996

  Copy full SHA for c183996

• Add make clean to clear the regression test results.

  

  martin

  committed
  784f2ed

  Copy full SHA for 784f2ed

• allow direct accesses into arrays despite signedness mismatch

  

  Daniel Kroening

  authored and

  tautschnig

  committed
  e1f4f07

  Copy full SHA for e1f4f07

• first stab at instrumenting memory-mapped I/O

  

  Daniel Kroening

  authored and

  tautschnig

  committed
  b890c54

  Copy full SHA for b890c54

• Copyright and include guard for internal library header

  tautschnig

  committed
  65b0455

  Copy full SHA for 65b0455

• __CPROVER_allocated_memory: Mark memory regions as valid

  Show description for b7a3466
  tautschnig

  committed
  b7a3466

  Copy full SHA for b7a3466

• Make the linter ignore generated builtin-header files

  tautschnig

  committed
  f0fe020

  Copy full SHA for f0fe020

• get-gcc-builtins: only dump declarations not found in existing files

  Show description for 01b8240
  tautschnig

  committed
  01b8240

  Copy full SHA for 01b8240

• Split generic GCC built-ins, extend using current GCC trunk

  tautschnig

  committed
  98e5c23

  Copy full SHA for 98e5c23

• get-gcc-builtins.sh: extract ia32 declarations automatically

  Show description for b4eaa3d
  tautschnig

  committed
  b4eaa3d

  Copy full SHA for b4eaa3d

• builtin-headers-ia32: remove space before '*'

  tautschnig

  committed
  bf3a45a

  Copy full SHA for bf3a45a

• Updates to ia32 headers by get-gcc-builtins.sh

  tautschnig

  committed
  0bdac88

  Copy full SHA for 0bdac88

• Added further ia32 GCC built-ins

  tautschnig

  committed
  3f23794

  Copy full SHA for 3f23794

• [goto-cc] Add support for ARM-enabling flags

  Show description for 21d0610
  karkhaz

  committed
  21d0610

  Copy full SHA for 21d0610

• Merge pull request #953 from martin-cs/goto-analyzer-5-part1

  Show description for fedc90b
  

  Daniel Kroening

  authored
  fedc90b

  Copy full SHA for fedc90b

• Merge pull request #957 from karkhaz/kk

  Show description for 5e6b593
  

  Daniel Kroening

  authored
  5e6b593

  Copy full SHA for 5e6b593

• Merge pull request #955 from tautschnig/void-cast

  Show description for e3ad659
  

  Daniel Kroening

  authored
  e3ad659

  Copy full SHA for e3ad659

• various HTML fixes for the manual

  

  Daniel Kroening

  committed
  fa47d99

  Copy full SHA for fa47d99

• Merge branch 'master' of github.com:diffblue/cbmc

  

  Daniel Kroening

  committed
  a9bc909

  Copy full SHA for a9bc909

• update CBMC applications URL

  

  Daniel Kroening

  committed
  a304db6

  Copy full SHA for a304db6

Commits on May 24, 2017

• Add a utility function to replace_symbol.

  

  martin

  committed
  8486086

  Copy full SHA for 8486086

• Add function header that was omitted in the previous merge.

  

  martin

  committed
  7468205

  Copy full SHA for 7468205

• Move the default implementations of output_json and output_xml into ai.cpp.

  Show description for ef406a0
  

  martin

  committed
  ef406a0

  Copy full SHA for ef406a0

• Make evaluation and/or simplification of conditions/expressions an ai domain operation.

  

  Martin Brain

  authored and

  martin

  committed
  050cc59

  Copy full SHA for 050cc59

• Merge pull request #946 from tautschnig/coverage-fixes

  Show description for 7f3a053
  

  Daniel Kroening

  authored
  7f3a053

  Copy full SHA for 7f3a053

• Merge pull request #949 from tautschnig/generated-files

  Show description for 0713f0e
  

  Daniel Kroening

  authored
  0713f0e

  Copy full SHA for 0713f0e

• Implement ai_simplify for intervals.

  

  martin

  committed
  409d6ef

  Copy full SHA for 409d6ef

• Implement ai_simplify for the constant domain.

  

  Martin Brain

  authored and

  martin

  committed
  c64448b

  Copy full SHA for c64448b

• Merge pull request #961 from martin-cs/goto-analyzer-5-part2

  Show description for fe7b88a
  

  Daniel Kroening

  authored
  fe7b88a

  Copy full SHA for fe7b88a

• Merge pull request #956 from tautschnig/fixed-tests

  Show description for a4b9411
  

  Daniel Kroening

  authored
  a4b9411

  Copy full SHA for a4b9411

Commits on May 25, 2017

• get_modules no longer has a dependency on bmct

  

  Daniel Kroening

  committed
  cf4c0e5

  Copy full SHA for cf4c0e5

• Do not configure bmct/prop_convt before reading goto programs

  Show description for dd2a55f
  tautschnig

  committed
  dd2a55f

  Copy full SHA for dd2a55f

• remove unused instances of include util/config.h

  

  Daniel Kroening

  committed
  9233c08

  Copy full SHA for 9233c08

• Added -O2 to non-Windows compile flags unless -O... is already set

  Show description for b612180
  tautschnig

  committed
  b612180

  Copy full SHA for b612180

• Merge pull request #969 from tautschnig/fix-O2

  Show description for faaf25f
  

  Daniel Kroening

  authored
  faaf25f

  Copy full SHA for faaf25f

• Merge pull request #730 from tautschnig/inspect-functions

  Show description for be0ded1
  

  Daniel Kroening

  authored
  be0ded1

  Copy full SHA for be0ded1

• Merge pull request #954 from tautschnig/mmio

  Show description for c09e3dd
  

  Daniel Kroening

  authored
  c09e3dd

  Copy full SHA for c09e3dd

• Merge pull request #967 from tautschnig/bmc-config-fix

  Show description for b6057fb
  

  Daniel Kroening

  authored
  b6057fb

  Copy full SHA for b6057fb

• introduced to_reference_type

  

  Daniel Kroening

  committed
  0b1c268

  Copy full SHA for 0b1c268

• added reference_type, for the benefit of C++ and Java

  

  Daniel Kroening

  committed
  dd25814

  Copy full SHA for dd25814

• introduced java_lang_object_type; java_array_type is now a reference

  

  Daniel Kroening

  committed
  511c96f

  Copy full SHA for 511c96f

• use null_pointer_exprt

  

  Daniel Kroening

  committed
  33a2e5c

  Copy full SHA for 33a2e5c

• Merge branch 'master' of github.com:diffblue/cbmc

  

  Daniel Kroening

  committed
  d27ffe5

  Copy full SHA for d27ffe5

• Fix order of operands in extractbits_exprt

  Show description for c33266a
  tautschnig

  committed
  c33266a

  Copy full SHA for c33266a

• Describe the internal endianness and bit organisation of internal bit vectors

  Show description for 8033bee
  tautschnig

  committed
  8033bee

  Copy full SHA for 8033bee

• Additional very basic regression tests for byte_update

  Show description for 808139b
  tautschnig

  committed
  808139b

  Copy full SHA for 808139b

• Avoid byte_extract on pointers reaching solvers/flattening

  Show description for 2fd63f7
  tautschnig

  committed
  2fd63f7

  Copy full SHA for 2fd63f7

• Added destination/source overlap checks to C string library

  tautschnig

  committed
  305e148

  Copy full SHA for 305e148

• Defer type resolution in array_{copy,set} until after dereferencing

  tautschnig

  committed
  8deb3d9

  Copy full SHA for 8deb3d9

• Added __CPROVER_array_replace to complement __CPROVER_array_set

  tautschnig

  committed
  ad56a18

  Copy full SHA for ad56a18

• Use array_{copy,replace,set} in C library to avoid loops

  tautschnig

  committed
  8c7d1e3

  Copy full SHA for 8c7d1e3

• added memcpy_chk implementation

  tautschnig

  committed
  af73aec

  Copy full SHA for af73aec

• Do not inline functions using arrays of symbolic size

  Show description for 91aef54
  tautschnig

  committed
  91aef54

  Copy full SHA for 91aef54

• Fix and extend byte extract flattening

  Show description for 237d8be
  tautschnig

  committed
  237d8be

  Copy full SHA for 237d8be

• The offset of void* is the same as char*

  tautschnig

  committed
  a6daa8a

  Copy full SHA for a6daa8a

• Do not use ID_pointer_offset directly, use pointer_offset() from pointer_predicates

  Show description for 353d5a9
  tautschnig

  committed
  353d5a9

  Copy full SHA for 353d5a9

• Dereferencing to void induces 0 read bytes

  tautschnig

  committed
  a71a093

  Copy full SHA for a71a093

• member_offset is strictly positive, use size_type instead of signed_size_type

  Show description for ed0c88f
  tautschnig

  committed
  ed0c88f

  Copy full SHA for ed0c88f

• restore do_bmc interface, for the benefit of cegis and hw-cbmc; partially reverts dd2a55f43a761441d4d718721c30e47f62493b3c

  

  Daniel Kroening

  committed
  3dbda92

  Copy full SHA for 3dbda92

• the c_types now have stronger C++ types

  

  Daniel Kroening

  committed
  2e11fef

  Copy full SHA for 2e11fef

Commits on May 26, 2017

• Merge pull request #971 from diffblue/c-types-typing

  Show description for 7f8efa0
  tautschnig

  authored
  7f8efa0

  Copy full SHA for 7f8efa0

Commits on May 29, 2017

• Merge pull request #166 from tautschnig/messaget

  Show description for 0b62971
  

  Daniel Kroening

  authored
  0b62971

  Copy full SHA for 0b62971

• Merge pull request #876 from tautschnig/gcc-builtins

  Show description for 928c28f
  

  Daniel Kroening

  authored
  928c28f

  Copy full SHA for 928c28f

• Merge pull request #795 from tautschnig/array-replace

  Show description for d23aa7e
  

  Daniel Kroening

  authored
  d23aa7e

  Copy full SHA for d23aa7e

• Inside newlib, __assert_func takes a non-const argument

  tautschnig

  committed
  9d4acea

  Copy full SHA for 9d4acea

• Ensure type consistency in scanf("%s", ...)

  tautschnig

  committed
  eddd157

  Copy full SHA for eddd157

• asm blocks have an asm+void combined type, just use "void"

  tautschnig

  committed
  04ac8d8

  Copy full SHA for 04ac8d8

• Fix merging of attributes

  tautschnig

  committed
  3f29f62

  Copy full SHA for 3f29f62

• Only merge foo() and foo(int) declarations when the former has no body

  tautschnig

  committed
  5c836a4

  Copy full SHA for 5c836a4

• C/C++ front end fixes

  tautschnig

  committed
  3d9c87b

  Copy full SHA for 3d9c87b

• Demote goto/destructor interaction to debug message level

  Show description for b7c7e8f
  tautschnig

  committed
  b7c7e8f

  Copy full SHA for b7c7e8f

• Update initializer and expression types after linking

  Show description for bcdd322
  tautschnig

  committed
  bcdd322

  Copy full SHA for bcdd322

• GCC supports -> in offsetof when forming a member designator

  Show description for 5936a3d
  tautschnig

  committed
  5936a3d

  Copy full SHA for 5936a3d

Commits on May 30, 2017

• update highlight package

  

  Daniel Kroening

  committed
  320722f

  Copy full SHA for 320722f

Commits on May 31, 2017

• Revert "disable nonsense code"

  Show description for fbdd728
  tautschnig

  committed
  fbdd728

  Copy full SHA for fbdd728

• Support return statements in C(!) constructors/destructors

  Show description for f195d69
  tautschnig

  committed
  f195d69

  Copy full SHA for f195d69

• Rework and fix parsing of unicode strings

  Show description for 3c51152
  tautschnig

  committed
  3c51152

  Copy full SHA for 3c51152

Commits on Jun 1, 2017

• Avoid repeated computation of guardt::operator-=

  Show description for 56aaf0c
  tautschnig

  committed
  56aaf0c

  Copy full SHA for 56aaf0c

• Merge pull request #729 from tautschnig/c-linking

  Show description for cc22448
  

  Daniel Kroening

  authored
  cc22448

  Copy full SHA for cc22448

• Merge pull request #981 from tautschnig/guard-diff

  Show description for 7ee0510
  

  Daniel Kroening

  authored
  7ee0510

  Copy full SHA for 7ee0510

Commits on Jun 6, 2017

• Add conversion/checking scripts

  reuk

  committed
  25183ac

  Copy full SHA for 25183ac

• Fix whitespace in doxygen.cfg

  reuk

  committed
  9f25d7c

  Copy full SHA for 9f25d7c

• Set doxygen to extract all

  reuk

  committed
  e6c1f59

  Copy full SHA for e6c1f59

• Update source and exclude paths

  reuk

  committed
  4142b60

  Copy full SHA for 4142b60

• Rename doxygen.cfg to doxyfile

  reuk

  committed
  00e97f8

  Copy full SHA for 00e97f8

• Enable doxygen quiet mode

  reuk

  committed
  86776e8

  Copy full SHA for 86776e8

• Update script based on review feedback

  reuk

  committed
  4e6c56e

  Copy full SHA for 4e6c56e

• Add legalese handling to conversion script

  reuk

  committed
  7ec965e

  Copy full SHA for 7ec965e

• Move conversion scripts to scripts folder

  reuk

  committed
  fa1d8e2

  Copy full SHA for fa1d8e2

• Fix up linter script to accept new Copyright label

  reuk

  committed
  60c5091

  Copy full SHA for 60c5091

• Revert "Fix up linter script to accept new Copyright label"

  Show description for 3e623f6
  reuk

  committed
  3e623f6

  Copy full SHA for 3e623f6

• Allow python script to reformat in place

  reuk

  committed
  7ed20c1

  Copy full SHA for 7ed20c1

• Fix parameter list bug

  reuk

  committed
  e0f2b2b

  Copy full SHA for e0f2b2b

• Add doc conversion driver script

  reuk

  committed
  0f6df5c

  Copy full SHA for 0f6df5c

• Update gitignore

  reuk

  committed
  5a01942

  Copy full SHA for 5a01942

• Update postprocessor comparison script

  reuk

  committed
  69dacac

  Copy full SHA for 69dacac

• Modify reformatting script to retain existing headers

  reuk

  committed
  aed3c25

  Copy full SHA for aed3c25

• Reformat src

  reuk

  committed
  e9349f8

  Copy full SHA for e9349f8

• Merge pull request #869 from reuk/doxy-squashed

  Show description for e2afe93
  

  Daniel Kroening

  authored
  e2afe93

  Copy full SHA for e2afe93

Commits on Jun 8, 2017

• Clean-up irep-id emptyness checks in analyses

  peterschrammel

  committed
  06638de

  Copy full SHA for 06638de

• Clean-up irep-id emptyness checks in ansi-c

  peterschrammel

  committed
  2c7a355

  Copy full SHA for 2c7a355

• Clean-up irep-id emptyness checks in cpp

  peterschrammel

  committed
  6f61609

  Copy full SHA for 6f61609

• Clean-up irep-id emptyness checks in goto-programs

  peterschrammel

  committed
  6ceb610

  Copy full SHA for 6ceb610

• Clean-up irep-id emptyness checks in goto-symex

  peterschrammel

  committed
  df528eb

  Copy full SHA for df528eb

• Clean-up irep-id emptyness checks in java-bytecode

  peterschrammel

  committed
  826a79b

  Copy full SHA for 826a79b

• Clean-up irep-id emptyness checks in path-symex

  peterschrammel

  committed
  e105fb1

  Copy full SHA for e105fb1

• Clean-up irep-id emptyness checks in pointer-analysis

  peterschrammel

  committed
  7ce9549

  Copy full SHA for 7ce9549

• Clean-up irep-id emptyness checks in util

  peterschrammel

  committed
  248eed6

  Copy full SHA for 248eed6

Commits on Jun 9, 2017

• Full slice property regression test

  peterschrammel

  committed
  c392312

  Copy full SHA for c392312

• Test to detect incorrect relabelling of properties after slicing

  peterschrammel

  committed
  7f8d909

  Copy full SHA for 7f8d909

• Label properties before using property slicer

  Show description for a9b4514
  peterschrammel

  committed
  a9b4514

  Copy full SHA for a9b4514

• Make property identifiers in output of --show-properties consistent

  Show description for 40983dd
  peterschrammel

  committed
  40983dd

  Copy full SHA for 40983dd

• Merge pull request #998 from peterschrammel/label-properties-before-full-slice

  Show description for 74e21ce
  

  Daniel Kroening

  authored
  74e21ce

  Copy full SHA for 74e21ce

Commits on Jun 11, 2017

• Merge pull request #997 from peterschrammel/clean-up-irep-id-empty

  Show description for 9d8d81a
  

  Daniel Kroening

  authored
  9d8d81a

  Copy full SHA for 9d8d81a

Commits on Jun 13, 2017

• A new macro based replacement for assert().

  

  martin

  committed
  b290a9e

  Copy full SHA for b290a9e

• Abnormal termination is no longer an automatic test failure.

  Show description for 668dbfa
  

  martin

  committed
  668dbfa

  Copy full SHA for 668dbfa

• Add an (undocumented) option to test out what happens if an invariant fails.

  

  martin

  committed
  720e0f8

  Copy full SHA for 720e0f8

• Get the linter to check for assertions and give a deprecated warning.

  

  martin

  committed
  975b5a3

  Copy full SHA for 975b5a3

• Remove clashing parts of my previous implementation.

  

  martin

  committed
  0a60788

  Copy full SHA for 0a60788

• Convert the assertions in std_expr.h to invariants as a demonstration.

  Show description for 0560b33
  

  martin

  committed
  0560b33

  Copy full SHA for 0560b33

• Add conversion functions for ID_bitnot.

  

  martin

  committed
  f77b843

  Copy full SHA for f77b843

• Replace assertions in some core libraries.

  Show description for cbe7de3
  

  martin

  committed
  cbe7de3

  Copy full SHA for cbe7de3

• Merge pull request #911 from martin-cs/feature/internal-invariant

  Show description for ae74767
  

  Daniel Kroening

  authored
  ae74767

  Copy full SHA for ae74767

Commits on Jun 14, 2017

• Merge commit 'aed3c25' into smowton/merge/master_20170614

  smowton

  committed
  a320377

  Copy full SHA for a320377

• Merge commit 'e9349f8' into smowton/merge/master_20170614

  smowton

  committed
  823b32d

  Copy full SHA for 823b32d

• Merge remote-tracking branch 'origin/master' into smowton/merge/master_20170614

  smowton

  committed
  eed0afb

  Copy full SHA for eed0afb

• Disable warnings that result from array-of with zero length

  smowton

  committed
  4324bbd

  Copy full SHA for 4324bbd