Making the instrumented clinit_wrapper function thread-safe#1786

Closed

Degiorgio wants to merge 93 commits intodiffblue:developfrom

cesaro:concurrency-support-for-clinit

Commits on May 2, 2018

Increase AssertionError arguments allowed from 2 to 3

JohnDumbell
authored and
Degiorgio
committed
Add a regression test.

JohnDumbell
authored and
Degiorgio
committed
Update desc file to add pass variables.

JohnDumbell
authored and
Degiorgio
committed
Fixing member offset computation in presence of bitfields

marek-trtik
authored and
Degiorgio
committed
Reset namespace after symbolic execution

tautschnig
authored and
Degiorgio
committed
C front-end: Section/ASM renaming also needs to be applied to aliases

tautschnig
authored and
Degiorgio
committed
fixup! Support __attribute__((section("x"))

tautschnig
authored and
Degiorgio
committed
Only the top-level section should be considered for renaming

tautschnig
authored and
Degiorgio
committed
Attribute main function arguments to __CPROVER_start

smowton
authored and
Degiorgio
committed
Fix CMake build for Glucose Syrup

Matthias Güdemann
authored and
Degiorgio
committed
Bugfix: Java array symbols must have mode ID_java

peterschrammel
authored and
Degiorgio
committed
Bugfix: Java symbol types must have mode ID_java

peterschrammel
authored and
Degiorgio
committed
Add support for CaDiCaL

tautschnig
authored and
Degiorgio
committed
Correct bound in test with long string

romainbrenguier
authored and
Degiorgio
committed
Remove unnecessary replace_expr

romainbrenguier
authored and
Degiorgio
committed
Use boolbvt for getting counter examples

romainbrenguier
authored and
Degiorgio
committed
Use string-max-length as default max input-length

romainbrenguier
authored and
Degiorgio
committed
Make get_array return nil for long strings

romainbrenguier
authored and
Degiorgio
committed
Weaken invariant for nil exprt as model of array

romainbrenguier
authored and
Degiorgio
committed
Assign 0 to string length for null Java String

romainbrenguier
authored and
Degiorgio
committed
Get rid of default axioms for strings

romainbrenguier
authored and
Degiorgio
committed
Make char_array_of_pointer return a reference

romainbrenguier
authored and
Degiorgio
committed
Get rid of string_max_length field

romainbrenguier
authored and
Degiorgio
committed
Add test for generics array and strings

romainbrenguier
authored and
Degiorgio
committed
Add tests showing the effect on string-max-length

romainbrenguier
authored and
Degiorgio
committed
Deprecate string-max-length option

romainbrenguier
authored and
Degiorgio
committed
Move MAX_CONCRETE_STRING_SIZE definition to magic

romainbrenguier
authored and
Degiorgio
committed
Small shared two way pointer

danpoe
authored and
Degiorgio
committed
Introduce nested exception printing

svorenova
authored and
Degiorgio
committed
Convert flatten_byte_extract to use structured exceptions

thk123
authored and
Degiorgio
committed
Introduce throwing bv_conversion expection

thk123
authored and
Degiorgio
committed
Introduce throwing a guard conversion exception

thk123
authored and
Degiorgio
committed
Provide the original goto statement in the error

thk123
authored and
Degiorgio
committed
Disable nested exception printing for Windows

thk123
authored and
Degiorgio
committed
Test demonstrating logging with clause for dealing with Windows

thk123
authored and
Degiorgio
committed
Add documentation to convert_bitvector

thk123
authored and
Degiorgio
committed
Introduce exceptions for all conversion steps.

thk123
authored and
Degiorgio
committed
Use format rather than from_expr for output

thk123
authored and
Degiorgio
committed
Remove redundant default constructor

thk123
authored and
Degiorgio
committed
Reformatting touched output function

thk123
authored and
Degiorgio
committed
Sort includes using clang-format

thk123
authored and
Degiorgio
committed
Make virtual function resolution independent of string table entry ordering

tautschnig
authored and
Degiorgio
committed
fix array->f typechecking

kroening
authored and
Degiorgio
committed
Extension to interpreter class

thk123
authored and
Degiorgio
committed
Update coding standard

Lukasz A.J. Wrona
authored and
Degiorgio
committed
Remove brace checking from cpplint

Lukasz A.J. Wrona
authored and
Degiorgio
committed
Remove NOLINTs for lambdas.

Lukasz A.J. Wrona
authored and
Degiorgio
committed
show java_new_array_data side effects

kroening
authored and
Degiorgio
committed
Replace asserts by invariants

peterschrammel
authored and
Degiorgio
committed
Set mode in goto_convert auxiliary symbols

peterschrammel
authored and
Degiorgio
committed
Bugfix: use proper language registration in unit tests

peterschrammel
authored and
Degiorgio
committed
Associate dynamic objects with respective language mode

peterschrammel
authored and
Degiorgio
committed
allow address_of of byte_extract expressions

kroening
authored and
Degiorgio
committed
Remove unused symbolt::{to,from}_irep

tautschnig
authored and
Degiorgio
committed
Use existing irep_idts instead of strings

tautschnig
authored and
Degiorgio
committed
Remove unused entries from the string table

tautschnig
authored and
Degiorgio
committed
Check that the string table does not include unused entries

tautschnig
authored and
Degiorgio
committed
Fix Doxygen syntax

tautschnig
authored and
Degiorgio
committed
Move enum idt to the single translation unit that actually requires it

tautschnig
authored and
Degiorgio
committed
Added an extension point for irep ids

tautschnig
authored and
Degiorgio
committed
Rephrase and justify curly brace alignment exceptions

Lukasz A.J. Wrona
authored and
Degiorgio
committed
array_size symbols: set mode and avoid redundant settings

tautschnig
authored and
Degiorgio
committed
symex_dynamic::dynamic_object_size* are constants

tautschnig
authored and
Degiorgio
committed
Utility functions to get mode and language

peterschrammel
authored and
Degiorgio
committed
Add more doxygen to language.h and mode.h

peterschrammel
authored and
Degiorgio
committed
Add Makefile dependency for smt2_solver

peterschrammel
authored and
Degiorgio
committed
Factor out java new removal into separate pass

peterschrammel
authored and
Degiorgio
committed
more files to ignore

kroening
authored and
Degiorgio
committed
Use remove_java_new

peterschrammel
authored and
Degiorgio
committed
Remove java_bytecode deps from Makefiles

peterschrammel
authored and
Degiorgio
committed
use optional<size_t> instead of -1 in cmdlinet

kroening
authored and
Degiorgio
committed
Use iosfwd instead of ostream where possible

tautschnig
authored and
Degiorgio
committed
Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_initialize

tautschnig
authored and
Degiorgio
committed
Use C++ streams instead of C-style snprintf

tautschnig
authored and
Degiorgio
committed
Set mode of if_exprt introduced in preprocessing

romainbrenguier
authored and
Degiorgio
committed
Add test where tmp_if_expr is introduced

romainbrenguier
authored and
Degiorgio
committed
Do not unnecessarily use C string functions

tautschnig
authored and
Degiorgio
committed
Move asserts to invariants (and provide suitable includes)

tautschnig
authored and
Degiorgio
committed
Use pointer_offset_bits instead of locally hacking up what it does anyway

tautschnig
authored and
Degiorgio
committed
Move definition of base_type_eqt to .cpp

tautschnig
authored and
Degiorgio
committed
Remove unused includes

tautschnig
authored and
Degiorgio
committed
Assign mode to invalid objects

peterschrammel
authored and
Degiorgio
committed
whitespace fix

kroening
authored and
Degiorgio
committed
remove do_unwind_module hook

kroening
authored and
Degiorgio
committed
remove unused includes

kroening
authored and
Degiorgio
committed
remove support for SMT1

kroening
authored and
Degiorgio
committed
remove OpenSMT

kroening
authored and
Degiorgio
committed
remove bmc_constraints

kroening
authored and
Degiorgio
committed
missing const for parameter

kroening
authored and
Degiorgio
committed
fix a comment

kroening
authored and
Degiorgio
committed
cleanup the includes in src/java_bytecode

kroening
authored and
Degiorgio
committed
Modifies the instrumented clinit_wrapper function
Degiorgio
committed
Added new cmd option to jbmc, 'java-threading'
Degiorgio
committed