For Java skip the check for dereference of a deallocated or dead object#89

Closed

cristina-david wants to merge 129 commits intodiffblue:masterfrom

cristina-david:java_pointer_checks

Commits on Apr 3, 2016

Permit linking of functions with ellipsis against fixed argument length
tautschnig
committed
Handle more cases of transparent-union vs. member type linking conflicts
tautschnig
committed

Commits on Apr 11, 2016

Support klibc's version of __assert_fail, cleanup of assert handling
tautschnig
committed

Commits on Apr 12, 2016

Permit preprocessor command within __attribute__
tautschnig
committed

Commits on May 8, 2016

package creation for El Capitan
Daniel Kroening
committed

Commits on May 10, 2016

Merge branch 'master' of https://www.github.com/diffblue/cbmc
Daniel Kroening
committed
Merge branch 'master' of https://www.github.com/diffblue/cbmc
Daniel Kroening
committed

Commits on May 12, 2016

Commits on May 13, 2016

+ regression test for NULL object dereferencing in Java
cristina-david
committed

Commits on May 14, 2016

return something in ctime and asctime
Daniel Kroening
committed
return something in strerror
Daniel Kroening
committed
return something in setlocale and localeconv
Daniel Kroening
committed
missing object file
Daniel Kroening
committed

Commits on May 16, 2016

source locations in location coverage
Daniel Kroening
committed
decision and condition coverage
Daniel Kroening
committed
Started type checking jsil programs

Daiva Naudziuniene
authored and
tautschnig
committed
Improvements to Jsil type checking

Daiva Naudziuniene
authored and
tautschnig
committed
Added jsil mode to be supported by goto_convert_functions

Daiva Naudziuniene
authored and
tautschnig
committed
Modified taint analysis to match procedure calls from languages other than Java

Daiva Naudziuniene
authored and
tautschnig
committed

Commits on May 17, 2016

goto-gcc: stop early on errors, minor cleanup
tautschnig
committed
Extend goto-gcc to also work as a wrapper for more compiler names
tautschnig
committed
Properly handle extended ld names
tautschnig
committed
Run ld where required
tautschnig
committed
Properly identify the base name of a file
tautschnig
committed
No hyrid binary if /dev/null when is goto-gcc's output file
tautschnig
committed
GCC's -m16 is actually a 32-bit machine emulation!
tautschnig
committed
get_base_name is semantically equivalent to translation_unit
tautschnig
committed
goto-cc: when input file is stdin, copy it into a file to replay multiple times
tautschnig
committed
Ensure that cleanup of .saved temporary files happens even if gcc fails
tautschnig
committed
Add -z option handling to goto-gcc

Norbert Manthey
authored and
tautschnig
committed
beautify coverage output
Daniel Kroening
committed
Merge pull request #91 from tautschnig/jsil-type-checking
Daniel Kroening
committed
Merge pull request #83 from tautschnig/list-eloc
Daniel Kroening
committed
Merge pull request #75 from tautschnig/full-path
Daniel Kroening
committed
remove tabs
Daniel Kroening
committed
Merge branch 'tautschnig-whitespace-cleanup'
Daniel Kroening
committed

Commits on May 18, 2016

Merge pull request #52 from tautschnig/linking-functions
Daniel Kroening
committed
Merge pull request #36 from tautschnig/goto-gcc-bugfixes-extensions
Daniel Kroening
committed
new interface for run()
Daniel Kroening
committed
do generate dummy code for empty ifthenelse
Daniel Kroening
committed
conjunction and disjunction on lists
Daniel Kroening
committed
fix output of literal expressions
Daniel Kroening
committed
conjunction and disjunction now take initializer_lists
Daniel Kroening
committed
get rid of conjunction and disjunction taking initializer_lists
Daniel Kroening
committed
fix for bmc_cover
Daniel Kroening
committed
Support __attribute__((constructor))
tautschnig
committed
Extended linking conflict reporting
tautschnig
committed
Permit some (ab)use of void f(void) in place of a full function declaration
tautschnig
committed
Fix type renaming of array types with non-constant size
tautschnig
committed
Array-size symbols may also trigger a type renaming
tautschnig
committed
Cleanup
tautschnig
committed
Removed unused include
tautschnig
committed
Transparent unions require argument conversion, do this for all union types
tautschnig
committed
Do not skip attributes of pointer types
tautschnig
committed
Linking for weak symbols
tautschnig
committed
weak symbols need not necessarily be treated as file-local
tautschnig
committed
Further weak-symbol-linking fixes
tautschnig
committed

Commits on May 19, 2016

initialize cond_literal and guard_literal
Daniel Kroening
committed
make bmc_cover work, and test it
Daniel Kroening
committed
further work on --cover
Daniel Kroening
committed
fix Minisat 2.2.1 URL
Daniel Kroening
committed
java entry point with nondet structs
danpoe
committed
missing cassert header
Daniel Kroening
committed
another attempt at cassert
Daniel Kroening
committed

Commits on May 20, 2016

Commits on May 23, 2016

more work on MC/DC
Daniel Kroening
committed

Commits on May 24, 2016

missing header
Daniel Kroening
committed
another go at superflous deads
Daniel Kroening
committed
added script to run datastax benchmarks and changed test.pl to support inner class names
marcelosousa
committed
Merge branch 'master' of https://github.com/diffblue/cbmc
Daniel Kroening
committed
more work on unnecessary destructor calls
Daniel Kroening
committed

Commits on May 25, 2016

Commits on May 26, 2016

another test for branch coverage
Daniel Kroening
committed

Commits on May 27, 2016

Merge branch 'master' of https://github.com/diffblue/cbmc
Daniel Kroening
committed
do not cover existing assertions
Daniel Kroening
committed
more tests
Daniel Kroening
committed
test that assertions are ignore
Daniel Kroening
committed

Commits on May 30, 2016

Merge pull request #96 from marcelosousa/regression-script-changes
Daniel Kroening
committed
Merge pull request #77 from tautschnig/attribute-constructor
Daniel Kroening
committed
Merge pull request #66 from tautschnig/assert-cleanup
Daniel Kroening
committed
Merge pull request #20 from tautschnig/parser-cleanup
Daniel Kroening
committed
Merge pull request #38 from tautschnig/linking-arrays-and-compound-types
Daniel Kroening
committed
Merge pull request #49 from tautschnig/weak-symbols
Daniel Kroening
committed
Merge pull request #58 from tautschnig/transparent-union
Daniel Kroening
committed
Merge pull request #67 from tautschnig/attributes-preprocessor
Daniel Kroening
committed
Merge branch 'master' of https://www.github.com/diffblue/cbmc
Daniel Kroening
committed
make typecheckt API more similar to old one for transition
Daniel Kroening
committed
use new messaging API in typecheckers
Daniel Kroening
committed
use new messaging API in Java typechecker
Daniel Kroening
committed
Do not add unreachable instructions during goto conversion
tautschnig
committed
Dead code analysis: no need to skip known-dead instructions with recent fix
tautschnig
committed
Object descriptor should skip typecasts
tautschnig
committed
Do not require a constant member offset when building a byte-extract expression
tautschnig
committed
Merge pull request #73 from tautschnig/no-dead-instructions
Daniel Kroening
committed

Commits on Jun 1, 2016

more MC/DC
Daniel Kroening
committed
fix java_string_literals
Daniel Kroening
committed
more MC/DC
Daniel Kroening
committed

Commits on Jun 2, 2016

MC/DC now works
Daniel Kroening
committed

Commits on Jun 5, 2016

Commits on Jun 6, 2016

Fix java bytecode translation of control-flow joins
tautschnig
committed
Merge pull request #103 from tautschnig/java-bytecode-converter
Daniel Kroening
committed
test from \#104
Daniel Kroening
committed
Merge pull request #102 from tautschnig/attribute-constructor-bugfix
Daniel Kroening
committed
Merge pull request #33 from tautschnig/object-descriptor-build-fixes
Daniel Kroening
committed
Merge pull request #101 from tautschnig/ssa-level1-bugfix
Daniel Kroening
committed

Commits on Jun 7, 2016