Additional functions for processing Java annotations#2247
Additional functions for processing Java annotations#2247romainbrenguier merged 4 commits intodiffblue:developfrom
Conversation
| java_bytecode_parse_treet::annotationt::element_value_pairt(); | ||
| element_value_pair.element_name = value.get_name(); | ||
| element_value_pair.value = value.get_value(); | ||
| return element_value_pair; |
There was a problem hiding this comment.
maybe possible to initialize element_value_pair directly using element_value_pairt{value.get_name(), value.get_value()}
There was a problem hiding this comment.
And then I can just return that directly without creating a variable for it. Thanks, done!
| const auto &element_name = element_value_pair.element_name; | ||
| REQUIRE(id2string(element_name) == "value"); | ||
| const auto &expr = element_value_pair.value; | ||
| const auto &comp_expr = from_integer(6, java_int_type()); |
There was a problem hiding this comment.
& not required here (from_integer returns a new expression)
There was a problem hiding this comment.
Thanks, removed it.
| { | ||
| if(annotation.type.id() != ID_pointer) | ||
| return false; | ||
| typet type = annotation.type.subtype(); |
There was a problem hiding this comment.
I had actually only changed the indentation on this line, but you're right it should be const and & so I changed that now.
c3c93d9 to
ee04723
Compare
ee6ffa8 to
b9e7ea3
Compare
|
@peterschrammel The lint build is failing with |
|
It looks like |
This makes it easier to distinguish between variables of type annotationt and java_annotationt.
c6de111 to
9905440
Compare
| const auto &element_name = element_value_pair.element_name; | ||
| REQUIRE(id2string(element_name) == "value"); | ||
| const auto &expr = element_value_pair.value; | ||
| const auto comp_expr = from_integer(6, java_int_type()); |
There was a problem hiding this comment.
to follow on @mgudemann comment you could comment on this in the WHEN section, for instance:
WHEN("Parsing a class with a class-level annotation MyClassAnnotation(6)") it would make it clear where this 6 comes from.
There was a problem hiding this comment.
That makes sense, I added that for both the class and method annotation.
This function can be used to retrieve annotations from a symbol table. A unit test is added for this functionality.
Making the function return an optionalt instead of a boolean provides some additional functionality without adding much complexity to the existing code that calls it.
This is required for a new check in cpplint.
9905440 to
3a7135a
Compare
8de6a33 Merge pull request diffblue#2006 from tautschnig/opt-no-self-loops 6605699 Merge pull request diffblue#2217 from diffblue/c-preprocessing-cleanout f1d787b Merge pull request diffblue#2166 from tautschnig/out-of-bounds 25339d5 Add option not to transform self-loops into assumes 5e6a3af Merge pull request diffblue#2249 from tautschnig/attribute-used d3d888b Bounds check for flexible array members 41003e8 Handle negative byte_extract offsets efea5c4 Fix flattening of access beyond type-specified bounds 0ec87c8 Merge pull request diffblue#2271 from diffblue/letification 090790a Interpret GCC's attribute __used__ 7985716 Merge pull request diffblue#2252 from tautschnig/fresh-symbol-cleanup 022846a letify: use irep_hash_mapt when hashing is expensive 15dff7d Merge pull request diffblue#2260 from antlechner/antonia/annotation-class-value 9a0ffae added irep_hash_mapt da0adfe bugfix: irep_hash_containert now keeps a copy of the contained ireps 45436ce use std::size_t for container sizes 0c26a53 let_count_idt is now a struct e0a5142 Merge pull request diffblue#2206 from diffblue/use-get_identifier e0ad069 Add support for Java annotations with Class value 3817341 Merge pull request diffblue#2237 from smowton/smowton/feature/initialize-class-literals 25c097e use get_identifier() instead of get(ID_identifier) on symbols 4eda8ad Java class literals: init using a library hook when possible 70f13f3 Merge pull request diffblue#1906 from tautschnig/missing-return-semantics 57885a5 Merge pull request diffblue#1868 from tautschnig/fix-1867 b49822e Merge pull request diffblue#2028 from tautschnig/regression-fix 2815e84 Merge pull request diffblue#2259 from smowton/smowton/feature/note-abstract-methods 09b8cf7 Merge pull request diffblue#2014 from tautschnig/cadical-experiment f50237b Merge pull request diffblue#1967 from romainbrenguier/refactor/drop-constraint-inheritance2 3f951dd Merge pull request diffblue#2234 from nmanthey/upstream-fpr c6c2928 Drop inheritance from constraint on exprt 0ffd0ae Replace negation of constraint by a method f653dec use compiler defaults for gcc defines a31f530 remove need to do preprocessing on 16-bit test 24210e9 enable AWS Codebuild to do -m32 bfae4e3 enable Travis to do -m32 34a3d85 Merge pull request diffblue#2247 from antlechner/antonia/annotation-conversion 15ed961 Note when symbol-table entries are abstract methods 3a7135a Add module_dependencies.txt in test folder 1fa0b97 Generalize and rename does_annotation_exist 1db0af4 Define inverse function of convert_annotations ff25b2c get_max: do not parse every symbol name in the symbol table b603703 Add missing override 70da606 Merge pull request diffblue#2251 from tautschnig/rename-cleanup 49429cf Merge pull request diffblue#2257 from owen-jones-diffblue/owen-jones-diffblue/fix-cmake-macro 4b7a195 Improve naming of annotation variables 57d96e5 Fix CMake macro f9058e7 Merge pull request diffblue#2246 from diffblue/z3-fpa 6b0f265 Merge pull request diffblue#2248 from thk123/bugfix/doxygen-including-jbmc 72e99a0 Merge pull request diffblue#2201 from diffblue/remove-incomplete-type-constructors d4abbea smt2 implementation for popcount_exprt e8fa1c9 bswap_exprt now knows how many bits a byte has a6652d2 Merge pull request diffblue#2255 from tautschnig/speedup-no-pointer-check 4b0a2d6 goto_check: do not unnecessarily build size-of expressions 1fe7cd7 remove mathematical_typet() constructor, which produces an incomplete object 25d393b remove vector_typet() constructor, which produces an incomplete object e7c52e4 remove range_typet() constructor, which produces an incomplete object f92083d remove array_typet() constructor, which produces an incomplete object 72f63f3 remove tag_typet() constructor, which produces an incomplete object 516ed14 remove symbol_typet() constructor, which produces an incomplete object 4215f21 Consistently use get_fresh_aux_symbol instead of local implementations e6cd488 Remove unused goto_symext::new_name c24b820 Remove goto_convertt::lookup a816b26 Do not include rename.h when not using its functions 52ab088 called_functions: use unordered_set 157a12c Fix doxyfile to include JBMC documentation 026e93f function-pointer-removal: drop unused set b75fcbc smt2 implementation for bswap_exprt e276b27 Avoid extern/parameter name collisions in show-goto-functions/dump-c output 87c5948 C front-end: Record extern declarations in current scope a47941d perf-test: add -W/--witness-check to validate SV-COMP witness checking 5b0395f perf-test: Update Ubuntu AMI ids for latest version 1288ec7 perf-test: speed up builds just like e7bb127 did afccaec Provide goto-cc in performance tests f802d87 Support CaDiCaL in performance tests, remove redundant script 7872f7c Replace a missing return value by nondet 829068f Don't require the simplifier to solve this regression test git-subtree-dir: cbmc git-subtree-split: 8de6a33
Two new functions are added, one to convert a vector of
java_annotationtto a vector ofannotationt, and one to find an annotation of a given type in a vector ofannotationt. The second function replaces the previously defineddoes_annotation_exist.This new functionality is not used anywhere in cbmc yet, but will soon be used in Diffblue software, where we need to be able to retrieve Java annotations from a symbol table.