Simplifier 20160305#12

Closed

tautschnig wants to merge 6193 commits intodiffblue:masterfrom

tautschnig:simplifier-20160305

This pull request is big! We're only showing the most recent 250 commits

Commits on Dec 30, 2015

edited some spaces
kroening
committed

Commits on Jan 1, 2016

avoid variables generated when not needed
kroening
committed

Commits on Jan 3, 2016

constants in assumptions
kroening
committed
clean up terminology in SAT messages
kroening
committed
ignore attepmts to freeze constants
kroening
committed
ignore attepmts to freeze constants
kroening
committed

Commits on Jan 4, 2016

Restore RETURN instructions before invoking dump-c
kroening
committed
compile on MINGW
kroening
committed
more support for verilog types
kroening
committed
typing for boolbvt::convert_typecast
kroening
committed
use typing
kroening
committed
added boolbvt::convert_power
kroening
committed
added boolbvt::convert_not
kroening
committed
make has_start_thread local
kroening
committed
instrumentation for mutex init via initialiser
kroening
committed

Commits on Jan 5, 2016

integer_address_object printed
kroening
committed
return aliases of address_of expresions
kroening
committed
skip through pointer type casts
kroening
committed

Commits on Jan 8, 2016

give error when --partial-loops and --unwinding-assertions are both set
kroening
committed

Commits on Jan 9, 2016

moved flow_insensitive_analysis.h to analyses
kroening
committed
moved flow_insensitive_analysis.h to analyses
kroening
committed

Commits on Jan 10, 2016

fi
kroening
committed

Commits on Jan 12, 2016

better advice for Macs
kroening
committed

Commits on Jan 14, 2016

C++11 initialize expressions
kroening
committed
test list initialisation
kroening
committed
allocate initialisers can omit ( )
kroening
committed
allocate initialisers can omit ( )
kroening
committed
use static_cast
kroening
committed
test more
kroening
committed
C++11 list initializers
kroening
committed
C++11 list initializers
kroening
committed
ID_function_type added
kroening
committed
more on C++11 initializer lists
kroening
committed
another case
kroening
committed

Commits on Jan 15, 2016

do escape analysis before full inlining
kroening
committed
remove CRs
kroening
committed
remove the tabs
kroening
committed
Removing remaining tabs
kroening
committed
avoid warning
kroening
committed

Commits on Jan 16, 2016

fix for location of goto guards
kroening
committed
fix indentation
kroening
committed
fix warning
kroening
committed

Commits on Jan 17, 2016

moved goto-instrument-wmm-full tests into a tarball
kroening
committed

Commits on Jan 19, 2016

Compare base objects when testing for null-pointer
kroening
committed
restore returns: ignore function pointers, avoid
kroening
committed
Proper dump of return statements in v3 goto programs
kroening
committed

Commits on Jan 20, 2016

Move sort_and_join to simplify_utils as it is of
kroening
committed
Do not use the size of guards to restore a previous
kroening
committed
Make guardt an exprt with additional operations
kroening
committed
Test works as of r6081
kroening
committed
Test of virtual functions
kroening
committed
missing header
kroening
committed
missing header
kroening
committed
Do not rely on irept implementation details
kroening
committed
Do not read uninitialised memory
kroening
committed
regression test from mailing list post
kroening
committed
Moved read_object&linking code from goto-cc to
kroening
committed
CBMC: support loading multiple goto binaries or a mix of
kroening
committed

Commits on Jan 24, 2016

switch to pkgbuild
kroening
committed

Commits on Jan 26, 2016

added rol and ror
kroening
committed
added bzero model
kroening
committed

Commits on Jan 30, 2016

missing headers
kroening
committed
missing headers
kroening
committed

Commits on Jan 31, 2016

comment
kroening
committed
fix recursive locking detection and pthread_cond_signal model
kroening
committed
recursive mutexes
kroening
committed
move eval into domain
kroening
committed
look into GOTO guards
kroening
committed

Commits on Feb 1, 2016

assignments to non-pointers
kroening
committed
pthread-id checks
kroening
committed
typo
kroening
committed

Commits on Feb 2, 2016

avoid warning
kroening
committed
bugfix
kroening
committed
avoid a warning
kroening
committed
more headers missing in cegis
kroening
committed
more headers missing in cegis
kroening
committed

Commits on Feb 5, 2016

prepare for C++14
kroening
committed
pointer constants may have value NULL
kroening
committed
track aliases with global objects
kroening
committed
store architecture in symbol table
kroening
committed
store and restore OS and architecture
kroening
committed
nudge define
kroening
committed

Commits on Feb 6, 2016

architecture config is now a string
kroening
committed
pand, pandn, por, pxor take di arguments
kroening
committed
__builtin_ia32_pand also returns di
kroening
committed
revert
kroening
committed
save arch
kroening
committed
fix
kroening
committed
architecture -> arch
kroening
committed
fix linux os string
kroening
committed
proper order
kroening
committed
properly set architecture
kroening
committed
properly set architecture
kroening
committed
print architecture
kroening
committed
reference with width
kroening
committed
pointers will eventually need width
kroening
committed

Commits on Feb 7, 2016

List_initialization1 needs more work
kroening
committed
added VHDL ID
kroening
committed

Commits on Feb 9, 2016

accept string constants directly
kroening
committed
check if arch and os are there
kroening
committed

Commits on Feb 13, 2016

form
kroening
committed
constraints are now in aigt-derived data structure
kroening
committed
assert fails in case of out-of-bounds
kroening
committed

Commits on Feb 15, 2016

fix #ifndefs
kroening
committed
moved json to util
kroening
committed
handy methods
kroening
committed
JSON taces
kroening
committed
import of miniBDD
kroening
committed
fix
kroening
committed
Avoid iterated operator-- on mp_integer on large
kroening
committed
Promotion of bit-fields requires attention to their width
kroening
committed
Added failed-tests-printer.pl
kroening
committed
avoid NULL
kroening
committed
Translate exprt to/from miniBDD
kroening
committed
compound tags
kroening
committed

Commits on Feb 16, 2016

avoid invalidating an iterator
kroening
committed
refactoring of bitvector manipulation
kroening
committed
fix lock clearing on pthread_create
kroening
committed
BDDs: Added standard file headers, conversion test
kroening
committed
Moved unit tests to separate directory
kroening
committed
New transformation to skip over selected loops as
kroening
committed
Don't mark as threaded all code following calls to functions that may
kroening
committed
Remove redundant data member body_available, replaced
kroening
committed
.d files not be included in repository
kroening
committed
Make --program-only output more complete
kroening
committed
Parse C11 _Alignas
kroening
committed
fix extra ID_size
kroening
committed
dump-c: properly output '\\', improve char output
kroening
committed
dump-c: rewrite int x; x=foo(); to int x=foo(); to
kroening
committed
dump-c: Arrays of pointers don't introduce an
kroening
committed
No phi nodes across different threads
kroening
committed
endianness map for vector
kroening
committed
Minor cleanup of irept
kroening
committed
Optimisation of binary2integer
kroening
committed
further optimisation for binary2integer
kroening
committed
Switch debug output in simplifier on/off during
kroening
committed
fix for floating-point division for the case of normal / subnormal
kroening
committed
added has_subexpr()
kroening
committed
Extend checks to avoid unbounded recursion on
kroening
committed
Generalise operator-= and operator|= of guardt
kroening
committed
further test for FP divider
kroening
committed

Commits on Feb 17, 2016

we really insist on C++11
kroening
committed
look at condition before recursing down an if_exprt
kroening
committed
added lift_if()
kroening
committed
Simplify byte_extract( ?:, ...)
kroening
committed
use lift_if
kroening
committed
Extend simplification of byte_extract(byte_update(...),
kroening
committed
Simplify byte_extract(array_of(...), ...)
kroening
committed
Simplify byte_extract(union, ...)
kroening
committed
Bug fixes for byte_extract(array/struct, ...)
kroening
committed
Distribute dereference across ?:
kroening
committed
Big endian support for unions in all contexts
kroening
committed
Completed bits2expr
kroening
committed
script needs to be executable
kroening
committed
make lift_if more robust
kroening
committed
simplify after lifting
kroening
committed
Simplify byte_extract(byte_extract(...), ...)
kroening
committed
Rewrite byte update of arrays
kroening
committed
Visual Studio still can't do constexpr in switch case
kroening
committed
make sure shifts are 64 bits wide
kroening
committed
needs a cast
kroening
committed
fix for enum return
kroening
committed
compile with Visual Studio
kroening
committed
Added detailed type conflict reporting
kroening
committed
Adding/extending support for ssa_exprt
kroening
committed
hide
kroening
committed
hide
kroening
committed
hide
kroening
committed
use ssa_exprt
kroening
committed
No phi nodes across different threads
kroening
committed
Ensure convergence of constant propagation for a.b == y
kroening
committed
Fix operator|= of guards (bug introduced in r6352)
kroening
committed
Support bounds check on vector types
kroening
committed
dump-c: fix arguments that are transparent-union
kroening
committed
Rename enum/struct/union tags in the same way as symbol
kroening
committed
type_to_name: canonic type names, language independent
kroening
committed
Parse C11 _Noreturn
kroening
committed
Simplifier does not modify out-of-bounds access
kroening
committed
numberings now use size_t
kroening
committed
use std::size_t for bit-vector widths and indices
kroening
committed

Commits on Feb 20, 2016

added is_tracked() method
kroening
committed
rename
kroening
committed
END_FUNCTION case
kroening
committed
rename
kroening
committed
rename
kroening
committed
returns no longer jump
kroening
committed

Commits on Feb 21, 2016

catch Minisat::OutOfMemoryException
kroening
committed
fix instruction type
kroening
committed
properly kill temporaries
kroening
committed

Commits on Feb 22, 2016

report that MathSAT doesn't do quantifiers
kroening
committed
CEGIS Patch from Pascal
kroening
committed
CEGIS Patch from Pascal
kroening
committed
unused function
kroening
committed
struct vs class
kroening
committed
CEGIS patch from Pascal
kroening
committed
use std::size_t for distances
kroening
committed
use std::size_t for widths
kroening
committed
missing headers
kroening
committed
use std::size_t for widths
kroening
committed
use std::size_t for widths
kroening
committed
use std::size_t
kroening
committed
use std::size_t
kroening
committed
use std::size_t where appropriate
kroening
committed
missing headers again
kroening
committed
split up add_cprover_library
kroening
committed
further split add_cprover_library
kroening
committed
missing headers again
kroening
committed
compile for now
kroening
committed
compile for now
kroening
committed
compile with MSVC
kroening
committed
compile with MSVC
kroening
committed
missing headers again
kroening
committed
pass the library check
kroening
committed
rename danger code
kroening
committed
fix
kroening
committed
cegis command-line options
kroening
committed
patch from Pascal
kroening
committed

Commits on Feb 23, 2016

test for ISSTA paper bug
kroening
committed
avoid gcc warning
kroening
committed
fix type of string constants
kroening
committed
tweak for else_case
kroening
committed
Typecheck else branch
kroening
committed
Removed redundant check and instruction
kroening
committed
Added support for GCC's __auto_type
kroening
committed
enum subtype is only stored in symbol table, never in enum_tag type
kroening
committed
API change
kroening
committed
Travis CI configuration
tautschnig
committed
Initial README.md, including Travis-CI information
tautschnig
committed
separate cegis executable
kroening
committed
removed cegis dependency
kroening
committed

Commits on Feb 24, 2016

associativity of plus
kroening
committed

Commits on Feb 25, 2016

- Fixed vtables in Java.
pkesseli
committed

Commits on Feb 26, 2016

Create README.md
Peter Schrammel
committed
typo __CPROVER_array_set
kroening
committed
uninterpreted functions and threads
kroening
committed

Commits on Mar 5, 2016

Create README.md
Peter Schrammel
committed
Merge branch 'master' of github.com:diffblue/cbmc
Peter Schrammel
committed
Create README.md
Peter Schrammel
committed
Merge branch 'master' of github.com:diffblue/cbmc
Peter Schrammel
committed
merged README.md
Peter Schrammel
committed
Merge branch 'tautschnig-travis-ci'
Peter Schrammel
committed
Removed unused jump table; we might use switch/case once Visual Studio fully supports constexpr
tautschnig
committed
Simplify input/output format arguments
tautschnig
committed
Extended simplify for byte_update, typing
tautschnig
committed
Simplify byte_extract: typing, added simplify_member call
tautschnig
committed
Simplify ID_with when index is known
tautschnig
committed
Simplify typecast of pointer arithmetic expression to integer
tautschnig
committed
Preparing typing of simplify_if, use lift_if
tautschnig
committed
New implementation of (still disabled) expression replacement in simplify_if
tautschnig
committed

Commits on Mar 6, 2016

null3 does have a VCC generated, fixed test.desc
tautschnig
committed