remove_java_new_tc : lp:cbmc : Git : Code : CBMC

Get this branch:: git clone -b remove_java_new_tc https://git.launchpad.net/cbmc

Branch information

b6cae86... by Daniel Kroening <email address hidden> on 2019-05-30

remove_java_new can now follow one typecast

statements such as

var = (type) java_new(....)

can now be lowered. This removes the requirement to introduce a temporary
just to do the typecast.

d8598f8... by Romain Brenguier <email address hidden> on 2019-06-03

Merge pull request #4735 from romainbrenguier/clean-up/symex-assign

Clean-up symex assignments

4c38989... by Daniel Kroening <email address hidden> on 2019-06-03

Merge pull request #4718 from romainbrenguier/ci/clang

Add CI compilation with clang++-3.8

798f651... by Michael Tautschnig <email address hidden> on 2019-06-03

Merge pull request #4703 from hannes-steffenhagen-diffblue/feature/goto-analyzer-usability

Preparation to make goto-analyzer work with the goto_verifiert framework

make_and simplifies trivial expressions

This is to avoid generating expressions like TRUE && TRUE

Add missing const

Avoid modifying guard argument in symex assign

This allows guard to be constant in the signatures which makes it
explicit that it is left unmodified by the function.

Move make_and to expr_util

This can be useful in other modules than BDDs.

Add an SSA_assignment_stept class with constructor

Without this, it is not clear what are the fields of SSA_stept which are
required to describe an assignement.

Add missing const

Makes explicit that these won't be changed.

»