cbmc:is_java_array_tag_signature

Branch merges

Related source package recipes

No recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related charm recipes

bdec3c8... by Daniel Kroening <email address hidden> on 2018-09-29

strengthen typing of is_java_array_tag

The new type is more restrictive, and avoids some unnecessary
transformation.

e24e948... by Michael Tautschnig on 2018-11-10

Merge pull request #3286 from tautschnig/lambda_method_handles

Use irept instead of symbol_exprt in java_lambda_method_handlest [blocks: #2310]

abdadf1... by Michael Tautschnig on 2018-11-10

Merge pull request #3307 from smowton/smowton/fix/remove-exceptions-after-convert-nondet

JBMC: run remove_exceptions after replace_java_nondet

68d7791... by Michael Tautschnig <email address hidden> on 2018-11-07

clang-format compatible line breaks

bd5b18f... by Michael Tautschnig <email address hidden> on 2018-11-06

Use irept instead of symbol_exprt in java_lambda_method_handlest

A java_lambda_method_handlest really is just a collection of identifiers - there
is no need to put them into a symbol_exprt, instead the identifier can directly
be used as the id of an irept. This reduces the memory footprint, but more
importantly avoids a warning of using a deprecated symbol_exprt constructor.
This warning is well placed, because those symbol_exprt would never have a type
set, which makes them invalid symbol_exprt anyway.

716ffec... by Daniel Kroening <email address hidden> on 2018-11-09

Merge pull request #3303 from chrisr-diffblue/throw-fix

Insert missing "throw" keyword

9d976e6... by Daniel Kroening <email address hidden> on 2018-11-09

Merge pull request #3308 from tautschnig/show-properties-fix

show-properties: do not skip functions marked for inlining

3b343a7... by Michael Tautschnig <email address hidden> on 2018-11-09

show-properties: do not skip functions marked for inlining

As of f443b1815e34bb we don't do (partial) inlining by default anymore. Thus
show-properties ended up with incomplete output.

c632625... by Michael Tautschnig on 2018-11-09

Merge pull request #3305 from tautschnig/expr2bits

to_bitvector_type must not be used on enum types

ec2933f... by Chris Smowton <email address hidden> on 2018-11-09

JBMC: run remove_exceptions after replace_java_nondet

The latter can introduce functions that need exception handlers, or more usually an ASSUME(@inflight_exception == null) guard
against accidentally propagated exceptions. When replace_java_nondet is run after exception removal we can get odd behaviour,
shown by the included test case, as the exception will be detected later than it should have been, or would escape from the
ASSUME guard implied by a @MustNotThrow annotation.