Code

String solver back-end#374

Code

Merged

peterschrammel merged 8 commits intodiffblue:masterdiffblue/cbmc:masterfrom

romainbrenguier:string-refine-solverromainbrenguier/cbmc:string-refine-solverCopy head branch name to clipboard

Feb 5, 2017

Commits

Commits on Jan 31, 2017

• Making check methods of refinement virtual

  Show description for e8cd7be
  romainbrenguier

  committed
  e8cd7be

  Copy full SHA for e8cd7be

• Adding identifiers for string expressions and functions

  romainbrenguier

  committed
  5018806

  Copy full SHA for 5018806

Commits on Feb 2, 2017

• Added a to_unsigned_integer function to arith_tools

  Show description for 188d918
  romainbrenguier

  committed
  188d918

  Copy full SHA for 188d918

• Class for string types used in the string solver

  Show description for 756dea2
  romainbrenguier

  committed
  756dea2

  Copy full SHA for 756dea2

Commits on Feb 3, 2017

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

  romainbrenguier

  committed
  c45f8cb

  Copy full SHA for c45f8cb

• Class for string constraints.

  Show description for bb4fe7d
  romainbrenguier

  committed
  bb4fe7d

  Copy full SHA for bb4fe7d

• Class for generating string constraints from string functions

  romainbrenguier

  committed
  f5dc2e6

  Copy full SHA for f5dc2e6

• String refinement class

  Show description for 20f4970
  romainbrenguier

  committed
  20f4970

  Copy full SHA for 20f4970