CBMC

cbmc:java-struct-tag

  1. Git
  2. lp:cbmc
  3. java-struct-tag
Last commit made on 2018-11-30
Get this branch:
git clone -b java-struct-tag https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
java-struct-tag
Repository:
lp:cbmc

Recent commits

ddcf2c8... by Daniel Kroening <email address hidden>

java frontend: symbol_type -> struct_tag

83ad3c2... by Daniel Kroening <email address hidden>

C++: bases are now struct tags

7523aeb... by Daniel Kroening <email address hidden>

use a struct_tag to identify base classes

1eb1df6... by Peter Schrammel <email address hidden>

Merge pull request #2786 from LAJW/lajw/document-remove-virtual-functions

Document remove_virtual_functions [DOC-85]

f14b163... by "Lukasz A.J. Wrona" <email address hidden>

Document all functions

61b202a... by hannes-steffenhagen-diffblue <email address hidden>

Merge pull request #3473 from hannes-steffenhagen-diffblue/feature-optional_map_lookup

Add optional_lookup utility function

5b66cd3... by Michael Tautschnig

Merge pull request #3296 from JohnDumbell/jd/enhancement/find_free_suffix_improvement

Adding smallest_unused_suffix cache

6425eb1... by johndumbell <email address hidden>

Wrap incoming symbol tables in suffix-aware versions

Tests were done on a c method with 10,000 lines of x += argc ? f() : g(); to generate a large amount of temp symbols needing to be created, and with this change applied it took 1:11 (m:s) to finish generating the GOTO before it got stuck on symex, and without it the generation ran longer than 30 minutes.

In attempting to recreate the issue in Java it only got around a 5% reduction in run-time due to bytecode per method limitation and me not knowing the absolute best way to generate as many temporaries as possible, but I also didn't recognise any noticeable slowdown either. In the Java instance where this issue was first recognized it was building a similar number of temporaries as the C program, but directly benchmarking that is problematic because there is likely other issues causing it to require this number of temporaries in the first place.

But it would cause similar speed increases in any language that requires a large amount of symbols to be created that have a clashing prefix.

bf1dd6d... by johndumbell <email address hidden>

Changing namespacet to take symbol_table_baset instead of symbol_tablet

a568dc3... by johndumbell <email address hidden>

Get journalling_symbol_table to call wrapped objects next_unused_suffix

Due to the inclusion of an additional overridable method on symbol_table_baset we just need to make sure any calls to this wrapper are routed to the wrapped table and not to the base instance.