Code

String solver max-length option#652

Code

Closed

romainbrenguier wants to merge 40 commits intodiffblue:masterdiffblue/cbmc:masterfrom

allredj:string-solver-dev-2-new-optionsallredj/cbmc:string-solver-dev-2-new-optionsCopy head branch name to clipboard

Commits

Commits on Mar 17, 2017

• Preprocessing of goto programs for string refinement

  romainbrenguier

  committed
  d43529e

  Copy full SHA for d43529e

• Moving is_java_string_type functions to string_preprocess

  Show description for 4fd8694
  romainbrenguier

  committed
  4fd8694

  Copy full SHA for 4fd8694

• Moving refined_string_type to util

  Show description for f28ffe2
  romainbrenguier

  committed
  f28ffe2

  Copy full SHA for f28ffe2

• Removed distinction between c string type and refined string type

  romainbrenguier

  committed
  fff364c

  Copy full SHA for fff364c

• Removed mention of c string type

  Show description for c64c512
  romainbrenguier

  committed
  c64c512

  Copy full SHA for c64c512

• Linting corrections on /util/

  

  Joel Allred

  authored and

  romainbrenguier

  committed
  2f69606

  Copy full SHA for 2f69606

• Using unordered_map and merging private sections

  romainbrenguier

  committed
  41f1f40

  Copy full SHA for 41f1f40

• Using std::size_t and Better line breaking

  romainbrenguier

  committed
  e800b58

  Copy full SHA for e800b58

• Breaking long line

  romainbrenguier

  committed
  ea3872c

  Copy full SHA for ea3872c

• Making sure `copy` has an argument, checking if assignments list empty

  romainbrenguier

  committed
  53b398d

  Copy full SHA for 53b398d

• Remove useless assertion

  romainbrenguier

  committed
  7a91dac

  Copy full SHA for 7a91dac

• Const reference in ranged for

  romainbrenguier

  committed
  b4bd1d6

  Copy full SHA for b4bd1d6

• Replaced by

  romainbrenguier

  committed
  976b920

  Copy full SHA for 976b920

• Adding function and location to inserted assignments

  romainbrenguier

  committed
  1604f5f

  Copy full SHA for 1604f5f

• Using unordered maps instead of maps

  romainbrenguier

  committed
  c745df5

  Copy full SHA for c745df5

• Assertion on non nil object size

  romainbrenguier

  committed
  a382498

  Copy full SHA for a382498

• Make a copy of the function call with side effect

  romainbrenguier

  committed
  58e3ada

  Copy full SHA for 58e3ada

• New copies of location and function for inserting assignments

  romainbrenguier

  committed
  038c574

  Copy full SHA for 038c574

• Splitting long lines

  romainbrenguier

  committed
  719ca84

  Copy full SHA for 719ca84

• In ranged for, use auto& to modify elements

  romainbrenguier

  committed
  53b6a54

  Copy full SHA for 53b6a54

• Making add_string_type more generic

  Show description for 6a0bcfd
  romainbrenguier

  committed
  6a0bcfd

  Copy full SHA for 6a0bcfd

• new identifier for converting char pointer to array

  romainbrenguier

  committed
  a6f9cb6

  Copy full SHA for a6f9cb6

• Many correction in preprocessing of strings

  Show description for 00e99e1
  romainbrenguier

  committed
  00e99e1

  Copy full SHA for 00e99e1

• Many corrections in string refinement

  Show description for 4044236
  romainbrenguier

  committed
  4044236

  Copy full SHA for 4044236

• Adding refined_string_type to util Makefile

  romainbrenguier

  committed
  61340a7

  Copy full SHA for 61340a7

• Adding string preprocessing of goto-programs to Makefile

  romainbrenguier

  committed
  0eeec2e

  Copy full SHA for 0eeec2e

• Adding string solver cpp files to Makefile

  romainbrenguier

  committed
  ee27f27

  Copy full SHA for ee27f27

• Adding the string refinement option to the CBMC solvers

  Show description for 8100175
  romainbrenguier

  committed
  8100175

  Copy full SHA for 8100175

• Update on string regression tests

  Show description for 195bef2
  

  Joel Allred

  authored and

  romainbrenguier

  committed
  195bef2

  Copy full SHA for 195bef2

• Correction in the hacks to use refined strings in C programs

  romainbrenguier

  committed
  b8d036b

  Copy full SHA for b8d036b

• Add smoke tests for java string support

  Show description for 17c3f1f
  

  Joel Allred

  authored and

  romainbrenguier

  committed
  17c3f1f

  Copy full SHA for 17c3f1f

• Update smoke tests

  Show description for 0633454
  

  Joel Allred

  authored and

  romainbrenguier

  committed
  0633454

  Copy full SHA for 0633454

• Move java_easychair to performance tests

  

  Joel Allred

  authored and

  romainbrenguier

  committed
  f1debba

  Copy full SHA for f1debba

• Add performance tests with negated asserts

  Show description for 7f2aec3
  

  Joel Allred

  authored and

  romainbrenguier

  committed
  7f2aec3

  Copy full SHA for 7f2aec3

• Update java_char_array_init/test_init.class

  

  Joel Allred

  authored and

  romainbrenguier

  committed
  2d18c02

  Copy full SHA for 2d18c02

• Add first fixed_bugs test

  Show description for c24978f
  

  Joel Allred

  authored and

  romainbrenguier

  committed
  c24978f

  Copy full SHA for c24978f

• [string-refine] Case of array-of in substitute array access

  romainbrenguier

  committed
  c14eec7

  Copy full SHA for c14eec7

• [string-refine] Setting ui for temporary solver

  romainbrenguier

  committed
  fd2276a

  Copy full SHA for fd2276a

• [string-refine] Added option to the string solver for string length and

  Show description for b43057c
  romainbrenguier

  committed
  b43057c

  Copy full SHA for b43057c

• [cbmc] Adding options to cbmc for parameters of the string solver

  Show description for 2a866f6
  romainbrenguier

  committed
  2a866f6

  Copy full SHA for 2a866f6