Code

String solver#341

Code

Closed

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

romainbrenguier:string-solver-experimentsromainbrenguier/cbmc:string-solver-experimentsCopy head branch name to clipboard

Commits

Commits on Apr 9, 2016

• started adding support for Strings (with the CVC4 backend)

  

  Alberto Griggio

  committed
  05b7300

  Copy full SHA for 05b7300

Commits on Apr 15, 2016

• merged with upstream

  

  Alberto Griggio

  committed
  361d98a

  Copy full SHA for 361d98a

• improved string support in smt2 backend

  Show description for 9633963
  

  Alberto Griggio

  committed
  9633963

  Copy full SHA for 9633963

• added first string test to the regression suite (still no .desc though)

  

  Alberto Griggio

  committed
  6d59022

  Copy full SHA for 6d59022

Commits on Apr 29, 2016

• merging with upstream

  

  Alberto Griggio

  committed
  5cd5643

  Copy full SHA for 5cd5643

• fixed bug in converting string length for the CVC4 backend

  

  Alberto Griggio

  committed
  61b64bb

  Copy full SHA for 61b64bb

• added more string tests

  

  Alberto Griggio

  committed
  08af98c

  Copy full SHA for 08af98c

• removed accidentally committed changes to config.inc

  

  Alberto Griggio

  committed
  89dbec2

  Copy full SHA for 89dbec2

Commits on May 6, 2016

• strings: added hand-written SMT2 versions of test3.c

  Show description for b820c1e
  

  Alberto Griggio

  committed
  b820c1e

  Copy full SHA for b820c1e

• strings test3: added version with assertions checked one by one

  Show description for 7cc6a6b
  

  Alberto Griggio

  committed
  7cc6a6b

  Copy full SHA for 7cc6a6b

Commits on May 13, 2016

• revised string encoding as quantified arrays

  

  Alberto Griggio

  committed
  ccba04e

  Copy full SHA for ccba04e

• added more string tests

  

  Alberto Griggio

  committed
  72ccef3

  Copy full SHA for 72ccef3

Commits on May 20, 2016

• use native support for int2bv in CVC4

  

  Alberto Griggio

  committed
  44f48e5

  Copy full SHA for 44f48e5

• try to add an explicit upper bound to string lengths

  

  Alberto Griggio

  committed
  1f4d2ab

  Copy full SHA for 1f4d2ab

Commits on May 27, 2016

• merged with diffblue/master

  

  Alberto Griggio

  committed
  1baf4db

  Copy full SHA for 1baf4db

Commits on Jun 3, 2016

• merged with diffblue master

  

  Alberto Griggio

  committed
  b560ec1

  Copy full SHA for b560ec1

Commits on Jun 10, 2016

• added further string length constraints to cope with possible overflows

  

  Alberto Griggio

  committed
  c3cc804

  Copy full SHA for c3cc804

• fixed encoding of string suffix

  

  Alberto Griggio

  committed
  916f7ce

  Copy full SHA for 916f7ce

Commits on Jun 17, 2016

• fixed double output in encoding string constraints (check in the cache before re-generating)

  

  Alberto Griggio

  committed
  9bb988d

  Copy full SHA for 9bb988d

Commits on Jul 1, 2016

• merged with master

  

  Alberto Griggio

  committed
  9cb8535

  Copy full SHA for 9cb8535

• added various string benchmarks taken from z3str2-bv

  

  Alberto Griggio

  committed
  4b84909

  Copy full SHA for 4b84909

Commits on Jul 8, 2016

• started working on string support in the SAT backend (via PASS-like axiom instantiation)

  Show description for 8be3253
  

  Alberto Griggio

  committed
  8be3253

  Copy full SHA for 8be3253

Commits on Jul 15, 2016

• sync with master

  

  Alberto Griggio

  committed
  e02fee2

  Copy full SHA for e02fee2

• continued working on string refinement

  

  Alberto Griggio

  committed
  599b343

  Copy full SHA for 599b343

• further work on string refinement

  Show description for d138195
  

  Alberto Griggio

  committed
  d138195

  Copy full SHA for d138195

Commits on Aug 1, 2016

• continued working on string refinement loop

  Show description for 4abb6d6
  

  Alberto Griggio

  committed
  4abb6d6

  Copy full SHA for 4abb6d6

Commits on Aug 2, 2016

• string refinement: fixed bug in i2bin

  

  Alberto Griggio

  committed
  06eccb4

  Copy full SHA for 06eccb4

• string refinement: fixed processing of command-line args

  

  Alberto Griggio

  committed
  7ce74e8

  Copy full SHA for 7ce74e8

• string refinement: added missing conversions, fixed bug in axiom instantiation

  

  Alberto Griggio

  committed
  64ae282

  Copy full SHA for 64ae282

• string refinement: further progress. Now something works, but checking for axiom violations is still broken (don't know why though)

  

  Alberto Griggio

  committed
  6afcf55

  Copy full SHA for 6afcf55

• Adding --pass option to cbmc to use the string refinement code of Alberto

  

  Romain Brenguier

  committed
  ad547d2

  Copy full SHA for ad547d2

Commits on Aug 3, 2016

• experimenting with another conversion to bit vectors to take the length into account

  

  Romain Brenguier

  committed
  c864f07

  Copy full SHA for c864f07

Commits on Aug 5, 2016

• Changed the encoding of strings to use a structured type

  

  Romain Brenguier

  committed
  557b119

  Copy full SHA for 557b119

• Post proccessing of the lemmas

  

  Romain Brenguier

  committed
  a1fce4f

  Copy full SHA for a1fce4f

Commits on Aug 9, 2016

• Converting all strings to bit vectors using a structure containing the length and content

  

  Romain Brenguier

  committed
  c4c0815

  Copy full SHA for c4c0815

• cleaned some code

  

  Romain Brenguier

  committed
  a3e39ea

  Copy full SHA for a3e39ea

• better structure for the code of string expressions

  

  Romain Brenguier

  committed
  4d0f0c3

  Copy full SHA for 4d0f0c3

Commits on Aug 10, 2016

• taking care of char expressions

  

  Romain Brenguier

  committed
  2675eaf

  Copy full SHA for 2675eaf

• uniformisation of lemmas and axioms by putting them in a same class (string_axiomt)

  

  Romain Brenguier

  committed
  453381d

  Copy full SHA for 453381d

• adapted the code for string_equal

  

  Romain Brenguier

  committed
  2baf3bd

  Copy full SHA for 2baf3bd

• adapted the code for string_equal

  

  Romain Brenguier

  committed
  e447fa7

  Copy full SHA for e447fa7

Commits on Aug 11, 2016

• making the PASS algorithm cleaner

  

  Romain Brenguier

  committed
  7999115

  Copy full SHA for 7999115

Commits on Aug 12, 2016

• corrected the problem with infinite loops and some missing conversion for functions that return Boolean values

  

  Romain Brenguier

  committed
  653ae6c

  Copy full SHA for 653ae6c

• removed some debugging information that should no longer be needed

  

  Romain Brenguier

  committed
  30c1b78

  Copy full SHA for 30c1b78

• removed some debugging information that should no longer be needed

  

  Romain Brenguier

  committed
  0a489c7

  Copy full SHA for 0a489c7

• corrected a sign problem in the computation of the substitution

  

  Romain Brenguier

  committed
  2888fc2

  Copy full SHA for 2888fc2

• avoid creating new string symbols when there is no need for it

  

  Romain Brenguier

  committed
  d03aac0

  Copy full SHA for d03aac0

Commits on Aug 15, 2016

• adding instantiations before solving

  

  Romain Brenguier

  committed
  45c9d04

  Copy full SHA for 45c9d04

• Adding new tests for strings

  

  Romain Brenguier

  committed
  7bf66a1

  Copy full SHA for 7bf66a1

• adding index to the index set when we have a char_at function

  

  Romain Brenguier

  committed
  a690724

  Copy full SHA for a690724

• Corrected the order in the arguments of issuffix

  

  Romain Brenguier

  committed
  888e374

  Copy full SHA for 888e374

• A couple of other examples for strings

  

  Romain Brenguier

  committed
  1c89da7

  Copy full SHA for 1c89da7

• Test descriptions for strings

  

  Romain Brenguier

  committed
  b90ec2c

  Copy full SHA for b90ec2c

• Better displaying of the lemmas and other expressions

  

  Romain Brenguier

  committed
  f1a4908

  Copy full SHA for f1a4908

• Cleaning a bit the code for string refinement

  

  Romain Brenguier

  committed
  759613c

  Copy full SHA for 759613c

Commits on Aug 16, 2016

• Tests coming from the PASS article

  

  Romain Brenguier

  committed
  3f21d28

  Copy full SHA for 3f21d28

Commits on Aug 17, 2016

• adding support for axioms with existential quantifier, and adding the function contains

  

  Romain Brenguier

  committed
  36015e3

  Copy full SHA for 36015e3

Commits on Aug 18, 2016

• changed the index type to be signed in order to accomodate some functions like index_of, a drawback is that we have to add lemmas saying that the length of each string is positive

  

  Romain Brenguier

  committed
  96d30c1

  Copy full SHA for 96d30c1

Commits on Aug 19, 2016

• more precise tests, with both assertions that should succeed and fail

  

  Romain Brenguier

  committed
  24bfd52

  Copy full SHA for 24bfd52

• repaired the order of instantiation when there are existential quantifiers

  

  Romain Brenguier

  committed
  ff4d91a

  Copy full SHA for ff4d91a

Commits on Aug 22, 2016

• giving up for now refinement approach for the index set, which was not working for the contains example

  

  Romain Brenguier

  committed
  cac8777

  Copy full SHA for cac8777

Commits on Aug 26, 2016

• changing the way string constraints are represented

  

  Romain Brenguier

  committed
  b81708e

  Copy full SHA for b81708e

• changing the way string constraints are represented

  

  Romain Brenguier

  committed
  1624e6e

  Copy full SHA for 1624e6e

• changed the way string constraints are represented

  

  Romain Brenguier

  committed
  3f1c02b

  Copy full SHA for 3f1c02b

Commits on Aug 29, 2016

• structured the code for string refinement in several files

  

  Romain Brenguier

  committed
  04ad43d

  Copy full SHA for 04ad43d

Commits on Aug 30, 2016

• Completed the algorithm for contains function

  

  Romain Brenguier

  committed
  95a4d9e

  Copy full SHA for 95a4d9e

• Test for the substring function

  

  Romain Brenguier

  committed
  1eea52d

  Copy full SHA for 1eea52d

• corrected the prefix_of function

  

  Romain Brenguier

  committed
  23426ce

  Copy full SHA for 23426ce

• some missing tests

  

  Romain Brenguier

  committed
  4dc1edd

  Copy full SHA for 4dc1edd

• removed the copy declarations which we don't really know how to do for now

  

  Romain Brenguier

  committed
  4f878c0

  Copy full SHA for 4f878c0

Commits on Sep 6, 2016

• Compatibility with java strings

  

  Romain Brenguier

  committed
  86abfae

  Copy full SHA for 86abfae

• Compatibility with java strings, and a couple of examples of java programs

  

  Romain Brenguier

  committed
  37a3b75

  Copy full SHA for 37a3b75

Commits on Sep 7, 2016

• Corrected type checkm for string equality in Java programs

  

  Romain Brenguier

  committed
  b254c25

  Copy full SHA for b254c25

• Corrected type checkm for string equality in Java programs

  

  Romain Brenguier

  committed
  ea93657

  Copy full SHA for ea93657

Commits on Sep 10, 2016

• Pass preprocessing of java string literals

  

  Romain Brenguier

  committed
  f04df39

  Copy full SHA for f04df39

• improved pass processing for string literals inside arguments of functions

  

  Romain Brenguier

  committed
  7526764

  Copy full SHA for 7526764

• pass processing of new String

  

  Romain Brenguier

  committed
  fab0bc6

  Copy full SHA for fab0bc6

Commits on Sep 11, 2016

• PASS preprocessing for indexOf and lastIndexOf

  

  Romain Brenguier

  committed
  7cf5e6d

  Copy full SHA for 7cf5e6d

• removed unecessary debugging information

  

  Romain Brenguier

  committed
  cddbb6c

  Copy full SHA for cddbb6c

Commits on Sep 12, 2016

• Substring method and more tests

  

  Romain Brenguier

  committed
  19f5172

  Copy full SHA for 19f5172

• corrected a confusion between c strings and java strings in the case of pointers

  

  Romain Brenguier

  committed
  9635737

  Copy full SHA for 9635737

• regression test for java endsWith method

  

  Romain Brenguier

  committed
  4061517

  Copy full SHA for 4061517

• added java contains string method

  

  Romain Brenguier

  committed
  32d997e

  Copy full SHA for 32d997e

Commits on Sep 13, 2016

• cleaning the code by removing some debugging information that were using std::cout

  

  Romain Brenguier

  committed
  d4cee59

  Copy full SHA for d4cee59

• basic support for StringBuilder

  

  Romain Brenguier

  committed
  f9c45b3

  Copy full SHA for f9c45b3

• support for StringBuilder init without argument

  

  Romain Brenguier

  committed
  f100d55

  Copy full SHA for f100d55

• test for StringBuilder

  

  Romain Brenguier

  committed
  33ded2d

  Copy full SHA for 33ded2d

• support for StringBuilder.length

  

  Romain Brenguier

  committed
  8e212b2

  Copy full SHA for 8e212b2

• init from String and void for String and StringBuilder

  

  Romain Brenguier

  committed
  9f53d15

  Copy full SHA for 9f53d15

• tests for StringBuilder.length

  

  Romain Brenguier

  committed
  27a4a7d

  Copy full SHA for 27a4a7d

• substring with only one argument (we should add tests for this also)

  

  Romain Brenguier

  committed
  6661386

  Copy full SHA for 6661386

Commits on Sep 14, 2016

• conversion from integers to strings

  

  Romain Brenguier

  committed
  3751029

  Copy full SHA for 3751029

• conversion from integers to strings in java

  

  Romain Brenguier

  committed
  2bc890d

  Copy full SHA for 2bc890d

• parsing of integer in strings

  

  Romain Brenguier

  committed
  0081e63

  Copy full SHA for 0081e63

• parsing of integer in strings

  

  Romain Brenguier

  committed
  45f4b77

  Copy full SHA for 45f4b77

• parsing of integer in strings for java

  

  Romain Brenguier

  committed
  24cf61b

  Copy full SHA for 24cf61b

• better handling of StringBuilder.append to allow chained append calls

  

  Romain Brenguier

  committed
  1e91533

  Copy full SHA for 1e91533

Commits on Sep 15, 2016

• of int for negative numbers

  

  Romain Brenguier

  committed
  2c4395e

  Copy full SHA for 2c4395e

• conversion between string and int for negative numbers

  

  Romain Brenguier

  committed
  a874b87

  Copy full SHA for a874b87

• corrected a mistake in the code for string refinement of if expressions

  

  Romain Brenguier

  committed
  b56fcdc

  Copy full SHA for b56fcdc

Commits on Sep 16, 2016

• easychair example from TACAS09 (Path feasability analysis for string-manipulating programs

  

  Romain Brenguier

  committed
  99add90

  Copy full SHA for 99add90

• Separating the classes for the refined string type and string expressions

  

  Romain Brenguier

  committed
  26be0a4

  Copy full SHA for 26be0a4

• Separating the classes for the refined string type and string expressions

  

  Romain Brenguier

  committed
  20cd623

  Copy full SHA for 20cd623

• clening the code of string refinement of useless functions

  

  Romain Brenguier

  committed
  39e4ccc

  Copy full SHA for 39e4ccc

• incremental string solver for better performances

  

  Romain Brenguier

  committed
  fef67d7

  Copy full SHA for fef67d7

• incremental string solver

  

  Romain Brenguier

  committed
  2236603

  Copy full SHA for 2236603

Commits on Sep 19, 2016

• a couple of additional string methods, not tested yet

  

  Romain Brenguier

  committed
  baebf8f

  Copy full SHA for baebf8f

Commits on Sep 20, 2016

• corrected string builders

  

  Romain Brenguier

  committed
  0ff5946

  Copy full SHA for 0ff5946

• corrected trim function and test

  

  Romain Brenguier

  committed
  1249657

  Copy full SHA for 1249657

• corrected case functions and test

  

  Romain Brenguier

  committed
  4066ea2

  Copy full SHA for 4066ea2

Commits on Sep 22, 2016

• corrected case functions and test

  

  Romain Brenguier

  committed
  7e49aa1

  Copy full SHA for 7e49aa1

Commits on Oct 3, 2016

• changed the name of the CPROVER strcat functions to avoid confusion between its different versions

  

  Romain Brenguier

  committed
  a7e6c4c

  Copy full SHA for a7e6c4c

• corrected append int and test for empty string

  

  Romain Brenguier

  committed
  9a0f4af

  Copy full SHA for 9a0f4af

• made the string of bool conversion precise

  

  Romain Brenguier

  committed
  dab12b2

  Copy full SHA for dab12b2

• added the set length method for string builders

  

  Romain Brenguier

  committed
  aff92df

  Copy full SHA for aff92df

Commits on Oct 4, 2016

• added delete and deleteCharAt. Also improved the index simplification by grouping constants together

  

  Romain Brenguier

  committed
  ff6b640

  Copy full SHA for ff6b640

• tests for delete and deleteCharAt

  

  Romain Brenguier

  committed
  74a7d6b

  Copy full SHA for 74a7d6b

• tests for delete and deleteCharAt

  

  Romain Brenguier

  committed
  94afd07

  Copy full SHA for 94afd07

• tests for delete and deleteCharAt

  

  Romain Brenguier

  committed
  3da7602

  Copy full SHA for 3da7602

Commits on Oct 5, 2016

• added startsWith(char,fromIndex)

  

  Romain Brenguier

  committed
  185eb92

  Copy full SHA for 185eb92

• added indexOf and lastIndexOf with fromIndex argument

  

  Romain Brenguier

  committed
  731623d

  Copy full SHA for 731623d

• tests for indexOf and lastIndexOf with fromIndex argument

  

  Romain Brenguier

  committed
  8177899

  Copy full SHA for 8177899

• adding startsWith with toffset argument

  

  Romain Brenguier

  committed
  2ac64a2

  Copy full SHA for 2ac64a2

• adding String.replace(CC)

  

  Romain Brenguier

  committed
  c1691c3

  Copy full SHA for c1691c3

• tests for setLength and toCharArray

  

  Romain Brenguier

  committed
  7d1d5f9

  Copy full SHA for 7d1d5f9

• adding String.valueOf for several classes

  

  Romain Brenguier

  committed
  ed20626

  Copy full SHA for ed20626

• adding String.valueOf char

  

  Romain Brenguier

  committed
  827bda9

  Copy full SHA for 827bda9

Commits on Oct 6, 2016

• adding String.setCharAt

  

  Romain Brenguier

  committed
  7755cde

  Copy full SHA for 7755cde

• adding String.subSequence

  

  Romain Brenguier

  committed
  592a8f2

  Copy full SHA for 592a8f2

• adding StringBuilder.insert and tests

  

  Romain Brenguier

  committed
  c6c0f69

  Copy full SHA for c6c0f69

Commits on Oct 7, 2016

• unicode string litterals and codePointAt

  

  Romain Brenguier

  committed
  4f7fc09

  Copy full SHA for 4f7fc09

• codePointBefore and Count

  

  Romain Brenguier

  committed
  acbc764

  Copy full SHA for acbc764

• adding appendCodePoint

  

  Romain Brenguier

  committed
  3731dd8

  Copy full SHA for 3731dd8

Commits on Oct 10, 2016

• adding String.compareTo

  

  Romain Brenguier

  committed
  57b3d8d

  Copy full SHA for 57b3d8d

• adding String.hashCode

  

  Romain Brenguier

  committed
  f6bc09c

  Copy full SHA for f6bc09c

• adding Integer.toHexString

  

  Romain Brenguier

  committed
  98d0687

  Copy full SHA for 98d0687

• adding Integer.toHexString

  

  Romain Brenguier

  committed
  d3a39a1

  Copy full SHA for d3a39a1

Commits on Oct 11, 2016

• corrected an implementation problem with the initialisation of the index set

  

  Romain Brenguier

  committed
  0fadc77

  Copy full SHA for 0fadc77

Commits on Oct 13, 2016

• partial specification for floats

  

  Romain Brenguier

  committed
  0fc6d29

  Copy full SHA for 0fc6d29

• overapproximation of indexOf for strings as arguments

  

  Romain Brenguier

  committed
  3c5b277

  Copy full SHA for 3c5b277

• overapproximation of lastIndexOf for strings as arguments

  

  Romain Brenguier

  committed
  9df15f3

  Copy full SHA for 9df15f3

• corrected tests for IndexOf

  

  Romain Brenguier

  committed
  ad4ec55

  Copy full SHA for ad4ec55

• simplification of the code for string functions identifiers

  

  Romain Brenguier

  committed
  c814f13

  Copy full SHA for c814f13

• simplification of the code for string functions identifiers

  

  Romain Brenguier

  committed
  547f384

  Copy full SHA for 547f384

Commits on Oct 14, 2016

• simplification of the code for string functions identifiers and corection of the c tests accordingly

  

  Romain Brenguier

  committed
  0202011

  Copy full SHA for 0202011

• merge main branch with string solver

  

  Romain Brenguier

  committed
  fa589ef

  Copy full SHA for fa589ef

Commits on Oct 15, 2016

• removing useless z3 string tests

  

  Romain Brenguier

  committed
  1bfc264

  Copy full SHA for 1bfc264

Commits on Oct 17, 2016

• removed changes from the string solver branch that where unecessary

  

  Romain Brenguier

  committed
  7ea360c

  Copy full SHA for 7ea360c

• removed changes from the string solver branch that where unecessary

  

  Romain Brenguier

  committed
  08d8b7a

  Copy full SHA for 08d8b7a

• returning an error when the same variable is counted several time in an expression that should be added to the index set

  

  Romain Brenguier

  committed
  f64c7ad

  Copy full SHA for f64c7ad

• skipping delete test, for which our solver runs into the problem of having a variable appear several time in the same expression

  

  Romain Brenguier

  committed
  f3e40fd

  Copy full SHA for f3e40fd

• skipping a couple of tests for which we have the problem of a variable appear several time in the same expression

  

  Romain Brenguier

  committed
  e474609

  Copy full SHA for e474609

• skipping a couple of tests for which we have the problem of a variable appear several time in the same expression

  

  Romain Brenguier

  committed
  e5e3dfb

  Copy full SHA for e5e3dfb

• skipping a couple of tests for which we have the problem of a variable appear several time in the same expression

  

  Romain Brenguier

  committed
  fd2898c

  Copy full SHA for fd2898c

Commits on Oct 18, 2016

• some experiment with the format function, not conclusive so far

  

  Romain Brenguier

  committed
  fc4fadb

  Copy full SHA for fc4fadb

• restructuration using a constraint generator

  

  Romain Brenguier

  committed
  404760d

  Copy full SHA for 404760d

• restructuration using a constraint generator

  

  Romain Brenguier

  committed
  36c3e60

  Copy full SHA for 36c3e60

• restructuration using a constraint generator class

  

  Romain Brenguier

  committed
  9c7ee9b

  Copy full SHA for 9c7ee9b

Commits on Oct 19, 2016

• restructuration using a constraint generator class

  

  Romain Brenguier

  committed
  fa6eece

  Copy full SHA for fa6eece

• corected problems after restructuration

  

  Romain Brenguier

  committed
  103628f

  Copy full SHA for 103628f

Commits on Oct 20, 2016

• repaired some type problems with methods of the code_point kind and compare

  

  Romain Brenguier

  committed
  b27b90d

  Copy full SHA for b27b90d

• repaired an index problem with trim (case where length gets close to the largest integer)

  

  Romain Brenguier

  committed
  58d62ec

  Copy full SHA for 58d62ec

• repaired some type problems with integers

  

  Romain Brenguier

  committed
  eeea178

  Copy full SHA for eeea178

• Merge branch 'string-solver-restructuration' into sat-strings

  

  Romain Brenguier

  committed
  d8b2bfe

  Copy full SHA for d8b2bfe

• starting to use map for pass preprocessing

  

  Romain Brenguier

  committed
  14e21c0

  Copy full SHA for 14e21c0

• starting to use map for pass preprocessing

  

  Romain Brenguier

  committed
  ab6ceee

  Copy full SHA for ab6ceee

• starting to use map for pass preprocessing

  

  Romain Brenguier

  committed
  219a603

  Copy full SHA for 219a603

• using maps for pass preprocessing

  

  Romain Brenguier

  committed
  659427d

  Copy full SHA for 659427d

• introducing a variable for temporary pointers

  

  Romain Brenguier

  committed
  97c2323

  Copy full SHA for 97c2323

Commits on Oct 23, 2016

• pass preprocessing for functions returning pointers

  

  Romain Brenguier

  committed
  5f2cc79

  Copy full SHA for 5f2cc79

Commits on Oct 24, 2016

• pass preprocessing for toCharArray function, not complete but a simple example with length is working

  

  Romain Brenguier

  committed
  51f7d84

  Copy full SHA for 51f7d84

Commits on Oct 25, 2016

• pass preprocessing for toCharArray function, corrected type problems for geting data into a char array

  

  Romain Brenguier

  committed
  777be9e

  Copy full SHA for 777be9e

• corrected a mistake in the pass preprocessing, which was puting arguments in the wrong places for some functions

  

  Romain Brenguier

  committed
  497e41d

  Copy full SHA for 497e41d

• corrected the type problems for data access in toCharArray

  

  Romain Brenguier

  committed
  b6d7750

  Copy full SHA for b6d7750

• regression test for toCharArray

  

  Romain Brenguier

  committed
  fd6ecb6

  Copy full SHA for fd6ecb6

• regression test for toCharArray

  

  Romain Brenguier

  committed
  dca43ef

  Copy full SHA for dca43ef

Commits on Oct 26, 2016

• corrected a problem with StringBuilder in goto programs

  

  Romain Brenguier

  committed
  e2904ba

  Copy full SHA for e2904ba

• trying to add ofCharArray function

  

  Romain Brenguier

  committed
  9fed105

  Copy full SHA for 9fed105

Commits on Oct 27, 2016

• changing from malloc to new[] for the char array of string

  

  Romain Brenguier

  committed
  25351e7

  Copy full SHA for 25351e7

• Using new version of utf8 to utf16

  

  Romain Brenguier

  committed
  18d0af2

  Copy full SHA for 18d0af2

• Using a new[] instead for the data part of array in toCharArray

  

  Romain Brenguier

  committed
  4b1eed8

  Copy full SHA for 4b1eed8

• simplification of some methods in PASS preprocessing

  

  Romain Brenguier

  committed
  e475213

  Copy full SHA for e475213

Commits on Oct 28, 2016

• correcting the constraint generation from the of_char_array function

  

  Romain Brenguier

  committed
  dec2cbd

  Copy full SHA for dec2cbd

• tests for the of_char_array function

  

  Romain Brenguier

  committed
  4114064

  Copy full SHA for 4114064

• string initialisation from char array with offset and count arguments

  

  Romain Brenguier

  committed
  f951abb

  Copy full SHA for f951abb

• string.valueOf for char arrays

  

  Romain Brenguier

  committed
  46fcfb4

  Copy full SHA for 46fcfb4

Commits on Oct 31, 2016

• corrected the goto program for String.valueOf for char arrays

  

  Romain Brenguier

  committed
  abf01a9

  Copy full SHA for abf01a9

• tests for String.valueOf

  

  Romain Brenguier

  committed
  32824e2

  Copy full SHA for 32824e2

• setting String.copyValueOf to be the same than valueOf

  

  Romain Brenguier

  committed
  c2c33bf

  Copy full SHA for c2c33bf

• adding the StringBuilder.insert(I[C) function

  

  Romain Brenguier

  committed
  88fcf74

  Copy full SHA for 88fcf74

• adding String.format to the goto program

  

  Romain Brenguier

  committed
  556de11

  Copy full SHA for 556de11

• adding String.format to the goto program

  

  Romain Brenguier

  committed
  51d0bc9

  Copy full SHA for 51d0bc9

Commits on Nov 1, 2016

• clearing a bit the make_to_char_array_function function in pass preprocessing

  

  Romain Brenguier

  committed
  24bbc4c

  Copy full SHA for 24bbc4c

• cleaning pass preprocess functions of useless arguments

  

  Romain Brenguier

  committed
  894d502

  Copy full SHA for 894d502

• cleaning the code from codes for functions that are not yet supported

  

  Romain Brenguier

  committed
  aaf2b89

  Copy full SHA for aaf2b89

• cleaning the code from format functions which are not yet working

  

  Romain Brenguier

  committed
  3764761

  Copy full SHA for 3764761

• removing tests which are in the wrong directory

  

  Romain Brenguier

  committed
  0aefe60

  Copy full SHA for 0aefe60

Commits on Nov 11, 2016

• unimportant spacing changes

  

  Romain Brenguier

  committed
  0c60215

  Copy full SHA for 0c60215

Commits on Nov 21, 2016

• small cleaning

  romainbrenguier

  committed
  e35d93a

  Copy full SHA for e35d93a

Commits on Dec 2, 2016

• Adapting regression test to the actual output of cbmc

  romainbrenguier

  committed
  f36b5e2

  Copy full SHA for f36b5e2

Commits on Dec 6, 2016

• Changes to the push request as suggested by Michael

  

  Romain Brenguier

  authored and

  romainbrenguier

  committed
  bb7ae0e

  Copy full SHA for bb7ae0e

• setting pass option necessary to select the right solver

  

  Romain Brenguier

  authored and

  romainbrenguier

  committed
  4119d1c

  Copy full SHA for 4119d1c

• Adapting regression test to CBMC ouput

  romainbrenguier

  committed
  3513290

  Copy full SHA for 3513290

• Merge branch 'string-solver-experiments' of github.com:romainbrenguier/cbmc into string-solver-experiments

  romainbrenguier

  committed
  176b016

  Copy full SHA for 176b016

• Merge remote-tracking branch 'origin/string-solver' into string-solver-experiments

  romainbrenguier

  committed
  b09b7a4

  Copy full SHA for b09b7a4

Commits on Dec 8, 2016

• Merge remote-tracking branch 'diffblue/master' into string-solver-experiments

  romainbrenguier

  committed
  fcde5b5

  Copy full SHA for fcde5b5

• Deleted trailing whitespaces

  romainbrenguier

  committed
  0c5b1c8

  Copy full SHA for 0c5b1c8

Commits on Dec 12, 2016

• Renaming make_of_char_array... functions to make_char_array...

  romainbrenguier

  committed
  54b6947

  Copy full SHA for 54b6947

• Catching java.lang.String in string refinement

  Show description for ab4c970
  romainbrenguier

  committed
  ab4c970

  Copy full SHA for ab4c970

• Renaming STRING_SOLVER CHAR_WIDTH symbols

  Show description for f87e148
  romainbrenguier

  committed
  f87e148

  Copy full SHA for f87e148

• using from_integer instead of calls to integer2binary

  romainbrenguier

  committed
  3921568

  Copy full SHA for 3921568

• Renamed forall and exists methods to with_forall and with_exists

  romainbrenguier

  committed
  ed0f02c

  Copy full SHA for ed0f02c

• Renamed not_contains method to create_not_contains

  Show description for 880812d
  romainbrenguier

  committed
  880812d

  Copy full SHA for 880812d

• Changing the structure of string_constraintt

  Show description for 0f6409c
  romainbrenguier

  committed
  0f6409c

  Copy full SHA for 0f6409c

• Removed previously commented code

  romainbrenguier

  committed
  1035bd2

  Copy full SHA for 1035bd2

Commits on Dec 13, 2016

• Using from_integer for constant integer

  Show description for b049bc9
  romainbrenguier

  committed
  b049bc9

  Copy full SHA for b049bc9

• Function to detect and set the language for string refinement

  romainbrenguier

  committed
  3c1daf0

  Copy full SHA for 3c1daf0

• Renaming functions of string constraint generator

  Show description for 91ebe61
  romainbrenguier

  committed
  91ebe61

  Copy full SHA for 91ebe61

• Using from_integer function from arith_tools.h

  Show description for 4c5d352
  romainbrenguier

  committed
  4c5d352

  Copy full SHA for 4c5d352

• Removing duplicate of has_prefix

  Show description for 9efef8f
  romainbrenguier

  committed
  9efef8f

  Copy full SHA for 9efef8f

Commits on Dec 15, 2016

• Defining ids for string function in util/irep

  Show description for c81641a
  romainbrenguier

  committed
  c81641a

  Copy full SHA for c81641a

• Replaced --pass option by --refine-string

  Show description for 31b20a5
  romainbrenguier

  committed
  31b20a5

  Copy full SHA for 31b20a5

• Moved the pass* files to string_refine* and renamed classes

  Show description for 16e58db
  romainbrenguier

  committed
  16e58db

  Copy full SHA for 16e58db

• Using from_expr from langapi/language_util.h

  Show description for d39d014
  romainbrenguier

  committed
  d39d014

  Copy full SHA for d39d014

• Use arith-tools.h functions to convert expressions to integer

  romainbrenguier

  committed
  6b73f41

  Copy full SHA for 6b73f41

• Made integer_of_expr to correctly deal with negative numbers

  romainbrenguier

  committed
  2ab3e49

  Copy full SHA for 2ab3e49

Commits on Dec 16, 2016

• Setting the default of integer_of_expr to 0

  Show description for 95d089d
  romainbrenguier

  committed
  95d089d

  Copy full SHA for 95d089d

• Cleaner version of extract_java_string

  romainbrenguier

  committed
  2e7f98a

  Copy full SHA for 2e7f98a

• Removed changes to remove_returns used for debuging

  romainbrenguier

  committed
  582547d

  Copy full SHA for 582547d

Commits on Dec 19, 2016

• Following coding guidelines in string preprocessing

  Show description for d6d4627
  romainbrenguier

  committed
  d6d4627

  Copy full SHA for d6d4627

Commits on Dec 20, 2016

• Adding more comments in refined_string_type and string_constraint

  Show description for ffdef62
  romainbrenguier

  committed
  ffdef62

  Copy full SHA for ffdef62

• Removed unecessary use of a variable length array

  romainbrenguier

  committed
  2cd5def

  Copy full SHA for 2cd5def