Corrections for 675#687

Closed

allredj wants to merge 148 commits intodiffblue:masterfrom

allredj:testgen-corrections-for-675

Commits on Mar 2, 2017

added test cases related to classes pattern and matcher

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to string methods replaceFirst, replaceAll and split

lucasccordeiro
authored and
peterschrammel
committed
added character static methods for testing characters and converting case

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to sringBuilder append methods

lucasccordeiro
authored and
peterschrammel
committed
added stringBuilder methods length, setLength, capacity and ensureCapacity

lucasccordeiro
authored and
peterschrammel
committed
added stringBuilder methods charAt, setCharAt, getChars and reverse

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to stringBuilder constructors

lucasccordeiro
authored and
peterschrammel
committed
added stringBuilder methods insert, delete and deleteCharAt

lucasccordeiro
authored and
peterschrammel
committed
added string methods equals, equalsIgnoreCase, compareTo and regionMatches

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to string method concat

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to string class constructors

lucasccordeiro
authored and
peterschrammel
committed
added string searching methods indexOf and lastIndexOf

lucasccordeiro
authored and
peterschrammel
committed
added string methods length, position, replace, toUpperCase, toLowerCase, and trim

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to string startsWith and endsWith

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to string valueOf methods

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to string class substring methods

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to StringTokenizer object used to tokenize strings

lucasccordeiro
authored and
peterschrammel
committed
added test cases related to validate data from user using the ValidateInput class

lucasccordeiro
authored and
peterschrammel
committed
cleanup aa-path-symex and aa-symex

kroening
authored and
peterschrammel
committed
Fix failing travis tests after removal of aa-symex.

Vlastimil Zeman
authored and
peterschrammel
committed
Skip already-loaded Java classes

smowton
authored and
peterschrammel
committed
Convert Java methods only when they have a caller

smowton
authored and
peterschrammel
committed
Remove dead global variables

smowton
authored and
peterschrammel
committed
Restrict virtual method targets to known-created types

smowton
authored and
peterschrammel
committed
Mark all classes in root jar reachable if it doesn't declare a main function

smowton
authored and
peterschrammel
committed
Add this-parameter before determining needed classes

smowton
authored and
peterschrammel
committed
Lazy method conversion: load callee parent classes

smowton
authored and
peterschrammel
committed
Always assume String, Class and Object are callable

smowton
authored and
peterschrammel
committed
Don't try to call an abstract function

smowton
authored and
peterschrammel
committed
Make lazy method loading optional

smowton
authored and
peterschrammel
committed
Add CBMC lazy-methods parameter

smowton
authored and
peterschrammel
committed
Document lazy methods

smowton
authored and
peterschrammel
committed
Style fixes

smowton
authored and
peterschrammel
committed
Add lazy loading tests

smowton
authored and
peterschrammel
committed
Improve code style

smowton
authored and
peterschrammel
committed
Use safe pointers for optional arguments

smowton
authored and
peterschrammel
committed
Add lazy conversion documentation

smowton
authored and
peterschrammel
committed
Improve failed test printer

smowton
authored and
peterschrammel
committed
Remove aa-symex from DIRS variable in Makefile

Norbert Manthey
authored and
peterschrammel
committed
Don't allowing functions called from _Start to be inlined

thk123
authored and
peterschrammel
committed
Get symbol of member expression

dcattaruzza
authored and
peterschrammel
committed
Auxiliary function to check if the ssa has enough data to build an identifier

dcattaruzza
authored and
peterschrammel
committed
Bitwise operators for mpinteger

dcattaruzza
authored and
peterschrammel
committed
Auxiliary function to retrieve tail of trace and added dead command to trace

dcattaruzza
authored and
peterschrammel
committed
Fix arithmetic shift operators

smowton
authored and
peterschrammel
committed
Added a new class for handling the internals

thk123
authored and
peterschrammel
committed
Adding more symbols that should be excluded

thk123
authored and
peterschrammel
committed
Autocomplete script for bash

forejtv
authored and
peterschrammel
committed
Factor class identifier extraction out of remove virtuals

smowton
authored and
peterschrammel
committed
Discover lexical scopes for anonymous variables

smowton
authored and
peterschrammel
committed
loop unwinding in static init of Java enum

mgudemann
authored and
peterschrammel
committed
Support for Java assume

cristina-david
authored and
peterschrammel
committed
Regression tests for Java assume

cristina-david
authored and
peterschrammel
committed
Remove assume as coverage target

cristina-david
authored and
peterschrammel
committed
output covered lines as CSV in show_properties

Matthias Güdemann
authored and
peterschrammel
committed
compress list of lines into line ranges

Matthias Güdemann
authored and
peterschrammel
committed
add regression test for coverage lines

Matthias Güdemann
authored and
peterschrammel
committed
fix problem with missing comma / range fix for reaching end

Matthias Güdemann
authored and
peterschrammel
committed
Updated dump-C to use the new class

thk123
authored and
peterschrammel
committed
Merge pull request #579 from peterschrammel/test-gen-support
peterschrammel
authored
update interpreter
Matthias Güdemann
committed
Merge pull request #580 from mgudemann/update_interpreter
peterschrammel
authored
Merge branch 'master' of github.com:diffblue/cbmc into update-from-master
peterschrammel
committed

Commits on Mar 3, 2017

Merge pull request #582 from peterschrammel/update-from-master
peterschrammel
authored

Commits on Mar 10, 2017

Generate stub method for opaque functions

thk123
authored and
peterschrammel
committed
Don't create stub for CPROVER_ functions

thk123
authored and
peterschrammel
committed
Create stub argument identifiers for functions with parameters

thk123
authored and
peterschrammel
committed
Pass the whole parameter in when generating the symbol

thk123
authored and
peterschrammel
committed
Refactored method for generating return symbol name to languaget

thk123
authored and
peterschrammel
committed
Added a flag for enabling opaque method stubs

thk123
authored and
peterschrammel
committed
Use the system_library_symbols when generating stubs

thk123
authored and
peterschrammel
committed
Added comment explaining the type of symbols we aren't stubbing

thk123
authored and
peterschrammel
committed
Adding simple regression for struct function

thk123
authored and
peterschrammel
committed
Use the symbol in expr2c

thk123
authored and
peterschrammel
committed
Call the generate_opqaue_stubs from final

thk123
authored and
peterschrammel
committed

Commits on Mar 14, 2017

Changes to get java compiling

thk123
authored and
peterschrammel
committed
extend java_bytecode for test-gen-support

Matthias Güdemann
authored and
peterschrammel
committed

Commits on Mar 15, 2017

generate goals only if they do not exist in the json file

lucasccordeiro
authored and
peterschrammel
committed
add more test cases to check existing coverage

lucasccordeiro
authored and
peterschrammel
committed
default variant of instrument_cover_goals that uses an empty set of existing goals

lucasccordeiro
authored and
peterschrammel
committed
a goal should be identified by a source_locationt

lucasccordeiro
authored and
peterschrammel
committed
implement get_coverage method

lucasccordeiro
authored and
peterschrammel
committed
a goal should be identified by a source_locationt

lucasccordeiro
authored and
peterschrammel
committed
method to construct a coverage_goalst object

lucasccordeiro
authored and
peterschrammel
committed
use json file suggested at github issue #187

lucasccordeiro
authored and
peterschrammel
committed
add consider_goals method

lucasccordeiro
authored and
peterschrammel
committed
add the --no-trivial-tests option to CBMC

lucasccordeiro
authored and
peterschrammel
committed
do not produce test goals for constructor and destructor methods

lucasccordeiro
authored and
peterschrammel
committed
added CPROVER_initialize

lucasccordeiro
authored and
peterschrammel
committed
added json to cegis makefile

lucasccordeiro
authored and
peterschrammel
committed
Add json->irep deserialization routine

smowton
authored and
thk123
committed
set EXIT to 10 to all failing string-solver test cases

lucasccordeiro
authored and
thk123
committed
Java checkcast: fix stack when check disabled

smowton
authored and
thk123
committed
initial support for miniz

Matthias Güdemann
authored and
thk123
committed
use amalgamated files from release tarball

Matthias Güdemann
authored and
thk123
committed
type cleanup in miniz

Matthias Güdemann
authored and
thk123
committed
update Makefiles / remove all references to libzip/zlib

Matthias Güdemann
authored and
thk123
committed
regression test with multiple JARs/classpath

Matthias Güdemann
authored and
thk123
committed
disable unaligned load/store for g++

Matthias Güdemann
authored and
thk123
committed
auto-fix cpplint errors with generated sed script

Matthias Güdemann
authored and
thk123
committed
libzip/zlib download no longer needed

kroening
authored and
thk123
committed
Fixed compilation issues on MinGW

pkesseli
authored and
thk123
committed
remove `<regex>` from unapproved headers in cpplint

Matthias Güdemann
authored and
thk123
committed
Use remove_instanceof in driver programs

smowton
authored and
thk123
committed
Added a side effect expr that pushes/pops Java try-catch handlers + irep ids for Java exception handling

cristina-david
authored and
thk123
committed
Regression tests for exception handling

cristina-david
authored and
thk123
committed
Recreate the try-catch structure from the exception table

cristina-david
authored and
thk123
committed
Remove throw/try-catch and add the required instrumentation

cristina-david
authored and
thk123
committed
Moved Java exceptions regression tests

cristina-david
authored and
thk123
committed
Escaping brackets in test descriptions

cristina-david
authored and
thk123
committed
Fixed test description for cbmc-java/virtual7

cristina-david
authored and
thk123
committed
Recompute live ranges for local variables and add corresponding DEAD instructions

cristina-david
authored and
thk123
committed
Forced try-catch to start a new basic block

cristina-david
authored and
thk123
committed
Restructuring such that the exceptions instrumentation is added in one pass over the goto-program

cristina-david
authored and
thk123
committed
Add jump to the end of the current function if a function call throws an exception for which there is no handler

cristina-david
authored and
thk123
committed
Modified the expected goto-program for cbmc-java/virtual7 as exception handling instrumentation introduces new labels and GOTOs

cristina-david
authored and
thk123
committed
+ regression test for Java exception handling

cristina-david
authored and
thk123
committed
allow regex to limit class files loaded from JAR

Matthias Güdemann
authored and
thk123
committed
support class load configuration via JSON file

Matthias Güdemann
authored and
thk123
committed
add jars from JSON config to classpath

Matthias Güdemann
authored and
thk123
committed
add regression test

Matthias Güdemann
authored and
thk123
committed
take comments into account

Matthias Güdemann
authored and
thk123
committed
change from vector indices to map

Matthias Güdemann
authored and
thk123
committed
Explore matching nested bracketed stuff

rjmunro
authored and
thk123
committed
Fix ; after } errors

rjmunro
authored and
thk123
committed
Fix missing space after , errors

rjmunro
authored and
thk123
committed
Replace tabs globally within the line

rjmunro
authored and
thk123
committed
Add space after comma globally within the line

rjmunro
authored and
thk123
committed
Remove the top variable from the cfg_dominator analysis.

martin
authored and
thk123
committed
Support for Linux based on musl-libc.

Vlastimil Zeman
authored and
thk123
committed
Add test for Alpine linux (musl-libc).

Vlastimil Zeman
authored and
thk123
committed
Merge pull request #631 from peterschrammel/update-from-master
peterschrammel
authored

Commits on Mar 20, 2017

Update test-gen-support from master
peterschrammel
committed

Commits on Mar 21, 2017

Merge pull request #660 from peterschrammel/pull-from-master
forejtv
authored

Commits on Mar 22, 2017

Merge pull request #669 from romainbrenguier/string-refine-preprocessing
forejtv
authored
Making add_string_type more generic

romainbrenguier
authored and
Joel Allred
committed
new identifier for converting char pointer to array

romainbrenguier
authored and
Joel Allred
committed
Many corrections in preprocessing of strings

romainbrenguier
authored and
Joel Allred
committed
Many corrections in string refinement

romainbrenguier
authored and
Joel Allred
committed
Need to assign length before calls since it can be overwritten by functions with side-effect

romainbrenguier
authored and
Joel Allred
committed
Merge pull request #679 from diffblue/master
forejtv
authored

Commits on Mar 23, 2017