Code

gcc style error messages for goto-cc#463

Code

Closed

kroening wants to merge 169 commits intomasterdiffblue/cbmc:masterfrom

gcc-errorsdiffblue/cbmc:gcc-errorsCopy head branch name to clipboard

Commits

Commits on Jan 22, 2017

• gcc style error messages for goto-cc

  

  Daniel Kroening

  committed
  c0fda23

  Copy full SHA for c0fda23

• merge

  

  Daniel Kroening

  committed
  bfca2d5

  Copy full SHA for bfca2d5

• fix for multi-ary fixed-bv multiplication

  

  Daniel Kroening

  committed
  9a61c2c

  Copy full SHA for 9a61c2c

Commits on Feb 8, 2017

• fix for multi-ary fixed-bv multiplication

  

  Daniel Kroening

  committed
  f1df0be

  Copy full SHA for f1df0be

• Added CEGIS control benchmark 4

  Show description for 7f33f04
  

  pkesseli

  authored and

  Daniel Kroening

  committed
  7f33f04

  Copy full SHA for 7f33f04

• Generalise dominators template (#422)

  Show description for 940eb34
  

  smowton

  authored and

  Daniel Kroening

  committed
  940eb34

  Copy full SHA for 940eb34

• Implement local variable live range merging

  Show description for 649d928
  

  smowton

  authored and

  Daniel Kroening

  committed
  649d928

  Copy full SHA for 649d928

• Replace old variable table implementation

  Show description for ac93ee3
  

  smowton

  authored and

  Daniel Kroening

  committed
  ac93ee3

  Copy full SHA for ac93ee3

• Factor the jbcm type and LVT functions into individual files

  

  smowton

  authored and

  Daniel Kroening

  committed
  23f7d81

  Copy full SHA for 23f7d81

• Use a total order when top-sorting variables

  

  smowton

  authored and

  Daniel Kroening

  committed
  0610bae

  Copy full SHA for 0610bae

• Local variable table: tolerate impossible flows

  Show description for 5f740c6
  

  smowton

  authored and

  Daniel Kroening

  committed
  5f740c6

  Copy full SHA for 5f740c6

• Fix hole-in-variable-live-range test

  

  smowton

  authored and

  Daniel Kroening

  committed
  923b7ab

  Copy full SHA for 923b7ab

• Style fixes

  

  smowton

  authored and

  Daniel Kroening

  committed
  41d2b27

  Copy full SHA for 41d2b27

• Add documentation

  

  smowton

  authored and

  Daniel Kroening

  committed
  b309f06

  Copy full SHA for b309f06

• Add tests for local variable live ranges with holes

  Show description for 7372e8f
  

  smowton

  authored and

  Daniel Kroening

  committed
  7372e8f

  Copy full SHA for 7372e8f

• Cleanup of operands() accesses

  Show description for e12cf9b
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  e12cf9b

  Copy full SHA for e12cf9b

• Consistently resize instead of just reserving in codet classes

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  85118e1

  Copy full SHA for 85118e1

• Fix package_friendly1 test

  Show description for bce928f
  

  smowton

  authored and

  Daniel Kroening

  committed
  bce928f

  Copy full SHA for bce928f

• Enable Java regression tests

  Show description for e647aaf
  

  smowton

  authored and

  Daniel Kroening

  committed
  e647aaf

  Copy full SHA for e647aaf

• Fixed CEGIS control vector solution nondet

  Show description for 7c2e95a
  

  pkesseli

  authored and

  Daniel Kroening

  committed
  7c2e95a

  Copy full SHA for 7c2e95a

• Fixed nondet returns in benchmark

  Show description for 1a9c2b3
  

  pkesseli

  authored and

  Daniel Kroening

  committed
  1a9c2b3

  Copy full SHA for 1a9c2b3

• Fixing simple linting errors in CVC

  Show description for 76cf8be
  

  thk123

  authored and

  Daniel Kroening

  committed
  76cf8be

  Copy full SHA for 76cf8be

• Split convert_expr into a collection of smaller functions

  Show description for 0196734
  

  thk123

  authored and

  Daniel Kroening

  committed
  0196734

  Copy full SHA for 0196734

• Replaced loop with simpler expression

  Show description for 43b95ca
  

  thk123

  authored and

  Daniel Kroening

  committed
  43b95ca

  Copy full SHA for 43b95ca

• Replaced a for loop with a ranged based for loop

  

  thk123

  authored and

  Daniel Kroening

  committed
  704ed4f

  Copy full SHA for 704ed4f

• Parse the exception table

  

  smowton

  authored and

  Daniel Kroening

  committed
  0f80ad4

  Copy full SHA for 0f80ad4

• Make the method object, and thus the exception table, available to dominator analysis

  

  smowton

  authored and

  Daniel Kroening

  committed
  bf0332d

  Copy full SHA for bf0332d

• Add exception edges to the CFG for dominator computation

  

  smowton

  authored and

  Daniel Kroening

  committed
  974ee14

  Copy full SHA for 974ee14

• Style fixes for local variable table

  

  smowton

  authored and

  Daniel Kroening

  committed
  bcbb13a

  Copy full SHA for bcbb13a

• Make JAR/zip support optional in regression tests

  Show description for 031001b
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  031001b

  Copy full SHA for 031001b

• fixup! Consistently resize instead of just reserving in codet classes

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  017d854

  Copy full SHA for 017d854

• Don't reference CPROVER_memory from Java code. Fixes #197.

  Show description for 60a1fb2
  

  smowton

  authored and

  Daniel Kroening

  committed
  60a1fb2

  Copy full SHA for 60a1fb2

• Make symex language mode symbol clearer

  Show description for aff699d
  

  smowton

  authored and

  Daniel Kroening

  committed
  aff699d

  Copy full SHA for aff699d

• Add comment that goto_program_dereference doesn't specify language mode

  Show description for 0293309
  

  smowton

  authored and

  Daniel Kroening

  committed
  0293309

  Copy full SHA for 0293309

• Don't use potentially-invalid downcasts to read an object's clsid if possible

  Show description for 0c8aedc
  

  smowton

  authored and

  Daniel Kroening

  committed
  0c8aedc

  Copy full SHA for 0c8aedc

• Include child types when creating a virtual function dispatch tree

  Show description for 96b386f
  

  smowton

  authored and

  Daniel Kroening

  committed
  96b386f

  Copy full SHA for 96b386f

• Call least-derived virtual function for unknown clsid

  Show description for 1062f5c
  

  smowton

  authored and

  Daniel Kroening

  committed
  1062f5c

  Copy full SHA for 1062f5c

• Add test for virtual dispatch against child type

  

  smowton

  authored and

  Daniel Kroening

  committed
  e73226c

  Copy full SHA for e73226c

• Style and documentation fixes

  

  smowton

  authored and

  Daniel Kroening

  committed
  5e774da

  Copy full SHA for 5e774da

• fixup! wmm/musketeer: Use wmm_grapht::node_indext instead of unsigned

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  6fb9cf2

  Copy full SHA for 6fb9cf2

• cegis uses labels for marking instructions

  Show description for d15e106
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  d15e106

  Copy full SHA for d15e106

• std::string::c_str() is non-const on Mac OS

  Show description for 5b4f2ac
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  5b4f2ac

  Copy full SHA for 5b4f2ac

• cegis: remove unused variables and namespace-local functions

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  a2d8585

  Copy full SHA for a2d8585

• Make unused return value explicit in source

  Show description for 18e1579
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  18e1579

  Copy full SHA for 18e1579

• cegis: uniform copyright headers, added missing ones

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  1c74b6b

  Copy full SHA for 1c74b6b

• cegis: fix include guards to match coding conventions

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  5863454

  Copy full SHA for 5863454

• clobber: update to current APIs

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  fabac07

  Copy full SHA for fabac07

• memory-models: Use ID_c_enum as ID_enum no longer exists

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  40413ed

  Copy full SHA for 40413ed

• Merge improvements from aa-symex

  Show description for ac36bea
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  ac36bea

  Copy full SHA for ac36bea

• aa-symex: share files with symex, path-symex

  Show description for 72c9b77
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  72c9b77

  Copy full SHA for 72c9b77

• Support building aa-symex, clobber, memory-model

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  f3969d0

  Copy full SHA for f3969d0

• Revert "also don't build memory-models.dir and clobber.dir"

  Show description for 3f244b3
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  3f244b3

  Copy full SHA for 3f244b3

• Revert "do not build aa-symex.dir"

  Show description for 2e98e10
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  2e98e10

  Copy full SHA for 2e98e10

• Fix address space limit test. Fixes #243

  

  smowton

  authored and

  Daniel Kroening

  committed
  dcc4260

  Copy full SHA for dcc4260

• Add address space size limit regression test

  

  smowton

  authored and

  Daniel Kroening

  committed
  071a0b1

  Copy full SHA for 071a0b1

• restructure expr2java

  Show description for de84fe1
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  de84fe1

  Copy full SHA for de84fe1

• pre-load java.lang.Object / String in class queue

  Show description for 7aef6ae
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  7aef6ae

  Copy full SHA for 7aef6ae

• correct array type for Java

  Show description for aa45937
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  aa45937

  Copy full SHA for aa45937

• nondeterministic initialization

  Show description for 8620cee
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  8620cee

  Copy full SHA for 8620cee

• exception table parser

  Show description for 8431204
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  8431204

  Copy full SHA for 8431204

• handle java.lang.String literals

  Show description for c3fdd43
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  c3fdd43

  Copy full SHA for c3fdd43

• handle array length and runtime checks for Java

  Show description for 385521a
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  385521a

  Copy full SHA for 385521a

• Java assertion handling

  Show description for 11be193
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  11be193

  Copy full SHA for 11be193

• class conversion runtime checks / array handling

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  09c6304

  Copy full SHA for 09c6304

• java bytecode index in source location

  Show description for 8877d75
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  8877d75

  Copy full SHA for 8877d75

• Correct parsing / generation of source filename

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  f8f8889

  Copy full SHA for f8f8889

• Clean up Java pointer cast handling

  

  Matthias Güdemann

  authored and

  Daniel Kroening

  committed
  a981430

  Copy full SHA for a981430

• extract java bytecode convert method class

  Show description for ba45b55
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  ba45b55

  Copy full SHA for ba45b55

• Java entry point / main function

  Show description for 6f6d613
  

  Matthias Güdemann

  authored and

  Daniel Kroening

  committed
  6f6d613

  Copy full SHA for 6f6d613

• Correct java type width handling

  Show description for 50089af
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  50089af

  Copy full SHA for 50089af

• pacify cpplint

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  51999dc

  Copy full SHA for 51999dc

• take comments into account

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  b8cc294

  Copy full SHA for b8cc294

• fix linter warnings after rebase

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  6ea64f1

  Copy full SHA for 6ea64f1

• remove static method is_string_array

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  8d32fc7

  Copy full SHA for 8d32fc7

• take comments into account

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  f454ed8

  Copy full SHA for f454ed8

• remove cast_if_necessary

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  47bd670

  Copy full SHA for 47bd670

• is_constructor and is_virtual as class methods

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  2599f40

  Copy full SHA for 2599f40

• make param const reference in clean_deref

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  6c65dd7

  Copy full SHA for 6c65dd7

• irep ID_java_super_method_call

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  abccf9e

  Copy full SHA for abccf9e

• comments for java object factory

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  281905f

  Copy full SHA for 281905f

• documentation block gen_nondeet_array_init

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  d6f6b64

  Copy full SHA for d6f6b64

• remove default values from object factory

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  520cfcc

  Copy full SHA for 520cfcc

• export as_number to java_utils.cpp

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  64d2f1e

  Copy full SHA for 64d2f1e

• take tautschnig's comments into account

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  ecb6cca

  Copy full SHA for ecb6cca

• remove namespace from vtable

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  06942df

  Copy full SHA for 06942df

• remove const_cast

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  7d2a303

  Copy full SHA for 7d2a303

• add java_utils.cpp

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  f73048f

  Copy full SHA for f73048f

• Peter's comments

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  a0e5510

  Copy full SHA for a0e5510

• remove superfluous std::move from conversion

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  51751ce

  Copy full SHA for 51751ce

• adapt NullPointer[1-4] regression tests

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  85de00e

  Copy full SHA for 85de00e

• default ctor for java_convert_methodt::variablet

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  494436a

  Copy full SHA for 494436a

• take tautschnig's comments into account

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  c54f78a

  Copy full SHA for c54f78a

• assert known Java object size

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  1aa5bfd

  Copy full SHA for 1aa5bfd

• remove unused skip_initialize

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  7c89802

  Copy full SHA for 7c89802

• remove TODOs from expr2java

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  950a202

  Copy full SHA for 950a202

• beautification

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  e3cf2ce

  Copy full SHA for e3cf2ce

• change "* "->" *", too

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  48b00d6

  Copy full SHA for 48b00d6

• adapt NullPointer2 regression test

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  8786af7

  Copy full SHA for 8786af7

• adapt interface in CEGIS with default values

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  4669ef3

  Copy full SHA for 4669ef3

• whitespace in front of {

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  0230b0d

  Copy full SHA for 0230b0d

• get_language options to language API (#480)

  Show description for fcbd267
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  fcbd267

  Copy full SHA for fcbd267

• Added check for div by zero in CEGIS control rational back end.

  Show description for a2010c8
  

  pkesseli

  authored and

  Daniel Kroening

  committed
  a2010c8

  Copy full SHA for a2010c8

• missing header for S_IRUSR

  

  Daniel Kroening

  committed
  70acc40

  Copy full SHA for 70acc40

• Factor class identifier extraction out of remove virtuals

  Show description for 718f10f
  

  smowton

  authored and

  Daniel Kroening

  committed
  718f10f

  Copy full SHA for 718f10f

• Remove virtuals style improvements

  Show description for c85f573
  

  smowton

  authored and

  Daniel Kroening

  committed
  c85f573

  Copy full SHA for c85f573

• Discover lexical scopes for anonymous variables

  Show description for c83c5cc
  

  smowton

  authored and

  Daniel Kroening

  committed
  c83c5cc

  Copy full SHA for c83c5cc

• Add test for anonymous local scoping

  Show description for 04f6998
  

  smowton

  authored and

  Daniel Kroening

  committed
  04f6998

  Copy full SHA for 04f6998

• Replace gen_zero/gen_one by from_integer where possible

  Show description for 175bc4e
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  175bc4e

  Copy full SHA for 175bc4e

• Use null_pointer_exprt instead of gen_zero

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  230dc50

  Copy full SHA for 230dc50

• zero_initializer without message_handlert

  Show description for c37c089
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  c37c089

  Copy full SHA for c37c089

• Use zero_initializer instead of gen_zero

  Show description for e304bad
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  e304bad

  Copy full SHA for e304bad

• Added file copyright header as noted by linter

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  33b45d3

  Copy full SHA for 33b45d3

• cbmc-java: Print details of errors in regression tests

  Show description for a9752cc
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  a9752cc

  Copy full SHA for a9752cc

• Make from_integer fail an assertion for unsupported types

  Show description for b083cf5
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  b083cf5

  Copy full SHA for b083cf5

• Makefile tweaks to enable re-use of Makefiles in vpath builds

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  d36aa5a

  Copy full SHA for d36aa5a

• Script to prepare out-of-tree (aka vpath) builds

  Show description for 6a7a64c
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  6a7a64c

  Copy full SHA for 6a7a64c

• Use vpath builds for coverage measurement

  Show description for 99d53d9
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  99d53d9

  Copy full SHA for 99d53d9

• ignore recursion set if class is subtype

  

  mgudemann

  authored and

  Daniel Kroening

  committed
  a7a4ebb

  Copy full SHA for a7a4ebb

• loop unwinding in static init of Java enum

  Show description for 9f37ed4
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  9f37ed4

  Copy full SHA for 9f37ed4

• Keep SSA L1 IDs as an attribute

  Show description for 0bbb638
  

  smowton

  authored and

  Daniel Kroening

  committed
  0bbb638

  Copy full SHA for 0bbb638

• Replaced all instances of show-goto-functions a define

  Show description for ebe9f2e
  

  thk123

  authored and

  Daniel Kroening

  committed
  ebe9f2e

  Copy full SHA for ebe9f2e

• Renamed the GOTO_CHECK defintions according to the new naming convention

  

  thk123

  authored and

  Daniel Kroening

  committed
  ddc75af

  Copy full SHA for ddc75af

• Do not add named vars to used_local_names

  Show description for 712fed1
  

  smowton

  authored and

  Daniel Kroening

  committed
  712fed1

  Copy full SHA for 712fed1

• CPPlint on travis change: it will run, but not produce errors. (#473)

  

  forejtv

  authored and

  Daniel Kroening

  committed
  edf0edd

  Copy full SHA for edf0edd

• Mark internal functions static

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  b6a5436

  Copy full SHA for b6a5436

• remove_complex: modify expressions only when necessary

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  4adb505

  Copy full SHA for 4adb505

• remove_vector: modify expressions only when necessary

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  a7c6880

  Copy full SHA for a7c6880

• Apply adjust_float_expressions, rewrite_union just once per expression

  Show description for d38ccff
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  d38ccff

  Copy full SHA for d38ccff

• rewrite_union, adjust_float_expressions: modify expressions only when necessary

  

  tautschnig

  authored and

  Daniel Kroening

  committed
  db2f6a4

  Copy full SHA for db2f6a4

• Add remove_instanceof pass

  Show description for 36c87d9
  

  smowton

  authored and

  Daniel Kroening

  committed
  36c87d9

  Copy full SHA for 36c87d9

• Use container-based Travis builds (#488)

  Show description for 2e56672
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  2e56672

  Copy full SHA for 2e56672

• Make the pre-commit hook report non-temporary path names (#477)

  Show description for cef4870
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  cef4870

  Copy full SHA for cef4870

• Keep track of types for structs and unions

  Show description for ae3bb31
  

  thk123

  authored and

  Daniel Kroening

  committed
  ae3bb31

  Copy full SHA for ae3bb31

• Correcting test and adding to the suite

  Show description for ecf73db
  

  thk123

  authored and

  Daniel Kroening

  committed
  ecf73db

  Copy full SHA for ecf73db

• Added tests for different cases

  Show description for af84034
  

  thk123

  authored and

  Daniel Kroening

  committed
  af84034

  Copy full SHA for af84034

• Removed zip package

  Show description for 332af10
  

  pkesseli

  authored and

  Daniel Kroening

  committed
  332af10

  Copy full SHA for 332af10

• specify initial values for Boolean in struct optiont

  Show description for 7e8a2b3
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  7e8a2b3

  Copy full SHA for 7e8a2b3

• Additions to the gitignore

  Show description for 294c7db
  

  thk123

  authored and

  Daniel Kroening

  committed
  294c7db

  Copy full SHA for 294c7db

• initialize Boolean values in c_typecheck_baset

  Show description for 59996f7
  

  Matthias Güdemann

  authored and

  Daniel Kroening

  committed
  59996f7

  Copy full SHA for 59996f7

• add explicit undef value to format string enums

  Show description for e24d992
  

  mgudemann

  authored and

  Daniel Kroening

  committed
  e24d992

  Copy full SHA for e24d992

• Use remove_instanceof in driver programs

  Show description for bf09a0b
  

  smowton

  authored and

  Daniel Kroening

  committed
  bf09a0b

  Copy full SHA for bf09a0b

• Add instanceof test cases

  Show description for f25980c
  

  smowton

  authored and

  Daniel Kroening

  committed
  f25980c

  Copy full SHA for f25980c

• goto-instrument: remove virt calls and RTTI

  Show description for bf187ef
  

  smowton

  authored and

  Daniel Kroening

  committed
  bf187ef

  Copy full SHA for bf187ef

• read ACC_ABSTRACT attribute in Java class files

  Show description for e9712bb
  

  Matthias Güdemann

  authored and

  Daniel Kroening

  committed
  e9712bb

  Copy full SHA for e9712bb

• Check static array bounds of dynamic objects

  Show description for 8e54769
  

  smowton

  authored and

  Daniel Kroening

  committed
  8e54769

  Copy full SHA for 8e54769

• mode!=ID_java is trivially true in this branch

  Show description for d8ba38f
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  d8ba38f

  Copy full SHA for d8ba38f

• Limit dereferencing checks to actual access size

  Show description for 735900a
  

  tautschnig

  authored and

  Daniel Kroening

  committed
  735900a

  Copy full SHA for 735900a

• Making check methods of refinement virtual

  Show description for af19303
  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  af19303

  Copy full SHA for af19303

• Adding identifiers for string expressions and functions

  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  3d1fa7a

  Copy full SHA for 3d1fa7a

• Added a to_unsigned_integer function to arith_tools

  Show description for 2da0f17
  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  2da0f17

  Copy full SHA for 2da0f17

• Class for string types used in the string solver

  Show description for edf57da
  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  edf57da

  Copy full SHA for edf57da

• Class for string expressions to be used by the string solver

  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  651e53d

  Copy full SHA for 651e53d

• Class for string constraints.

  Show description for f4fd79c
  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  f4fd79c

  Copy full SHA for f4fd79c

• Class for generating string constraints from string functions

  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  df336c3

  Copy full SHA for df336c3

• String refinement class

  Show description for f7645ab
  

  romainbrenguier

  authored and

  Daniel Kroening

  committed
  f7645ab

  Copy full SHA for f7645ab

• Remove virtual functions: shorten dispatch table

  Show description for 0b2a5c1
  

  smowton

  authored and

  Daniel Kroening

  committed
  0b2a5c1

  Copy full SHA for 0b2a5c1

• If the only dispatch option is abstract, erase the call

  Show description for 3f0a880
  

  smowton

  authored and

  Daniel Kroening

  committed
  3f0a880

  Copy full SHA for 3f0a880

• Make test more tolerant of formatting differences

  Show description for e720837
  

  smowton

  authored and

  Daniel Kroening

  committed
  e720837

  Copy full SHA for e720837

• Add test for vtable abbreviation

  Show description for 48ffff3
  

  smowton

  authored and

  Daniel Kroening

  committed
  48ffff3

  Copy full SHA for 48ffff3

• Add source locations to virt calls

  Show description for 49d1ae7
  

  smowton

  authored and

  Daniel Kroening

  committed
  49d1ae7

  Copy full SHA for 49d1ae7

• Make string literal tables global

  Show description for f84460d
  

  smowton

  authored and

  Daniel Kroening

  committed
  f84460d

  Copy full SHA for f84460d

• Correct return value test of to_integer (#508)

  Show description for b6b0063
  

  allredj

  authored and

  Daniel Kroening

  committed
  b6b0063

  Copy full SHA for b6b0063

• Fixed use of inline

  

  NathanJPhillips

  authored and

  Daniel Kroening

  committed
  2ee34f3

  Copy full SHA for 2ee34f3

• Added regression tests for full-slice option

  Show description for 932ba57
  

  lucasccordeiro

  authored and

  Daniel Kroening

  committed
  932ba57

  Copy full SHA for 932ba57

• moved full-slice test cases from cbmc to goto-instrument

  Show description for bbe8fcc
  

  lucasccordeiro

  authored and

  Daniel Kroening

  committed
  bbe8fcc

  Copy full SHA for bbe8fcc

• Fix adjustment of goto targets in the loop unwinder

  

  danpoe

  authored and

  Daniel Kroening

  committed
  db88e7a

  Copy full SHA for db88e7a

• gcc style error messages for goto-cc

  

  Daniel Kroening

  committed
  adcd342

  Copy full SHA for adcd342

• merge

  

  Daniel Kroening

  committed
  09f2d80

  Copy full SHA for 09f2d80

• Merge branch 'master' into gcc-errors

  

  Daniel Kroening

  committed
  09e7615

  Copy full SHA for 09e7615