[SV-COMP'18 19/19] Fixing "identifier XYZ not found" error. #2008
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
smowton
reviewed
Apr 9, 2018
|
|
||
| int main() | ||
| { | ||
| dp83640_init(); |
There was a problem hiding this comment.
Cite the source for this (presumably some particular Linux kernel file?)
smowton
approved these changes
Apr 16, 2018
src/ansi-c/c_typecheck_base.cpp
Outdated
| @@ -717,7 +722,11 @@ void c_typecheck_baset::typecheck_declaration( | |||
| else | |||
| { | |||
| std::string asm_name; | |||
| asm_name=id2string(full_spec.section)+"$$"; | |||
| asm_name = id2string(full_spec.section); | |||
| std::string::size_type primary_section = asm_name.find('.', 1); | |||
There was a problem hiding this comment.
Worth an INVARIANT(asm_name.size() >= 1 && asm_name[0] == '.') to check you have the format you think you do?
The example taken from the Linux kernel shows that people mix weak aliases with section attributes. Not updating the alias name results in a namespace lookup failure. gcc_attributes11 is a reduced example taken from SV-COMP, where the same problem arises.
The Linux kernel first places `jiffies64` in .data, and later refines that to .data..cacheline_aligned. The latter still is within the .data section, though, so just use the .data part for renaming.
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
31c47c2 Merge pull request diffblue#2113 from diffblue/java_new_array_data fb3025d Merge pull request diffblue#2107 from thk123/feature/TG-3271/interpreter-tracking-mock-exceptions 32bf48e Merge pull request diffblue#2105 from tautschnig/determinise-test 7254a2a show java_new_array_data side effects 0f1482c Merge pull request diffblue#2094 from smowton/smowton/fix/tmp-object-factory-prefix 3cfec66 Merge pull request diffblue#2106 from diffblue/ptrmember_on_array bf4c39c Merge pull request diffblue#1966 from JohnDumbell/JohnDumbell/Update-Assertion-Validation 74a37c6 Merge pull request diffblue#1988 from tautschnig/cadical 74dc576 Merge pull request diffblue#2003 from tautschnig/bitfield-offset 8916906 Merge pull request diffblue#2008 from tautschnig/section-bug 0bd83ab Extension to interpreter class a0ca0ba fix array->f typechecking e1f4120 Make virtual function resolution independent of string table entry ordering 714ccff Merge pull request diffblue#2072 from danpoe/feature/small-shared-two-way-ptr 16b6c20 Merge pull request diffblue#2046 from thk123/gs_tg2922 04cb909 Merge pull request diffblue#2102 from thk123/formatting/sort-includes-clang-format 7070ba1 Sort includes using clang-format 9874a6b Reformatting touched output function f2a4054 Remove redundant default constructor 54fb9ab Use format rather than from_expr for output 781bf7c Introduce exceptions for all conversion steps. 21997b2 Add documentation to convert_bitvector 015b284 Test demonstrating logging with clause for dealing with Windows 9d41b0c Disable nested exception printing for Windows b866015 Provide the original goto statement in the error a97bc28 Introduce throwing a guard conversion exception 12f25c2 Introduce throwing bv_conversion expection 9bd5222 Convert flatten_byte_extract to use structured exceptions 3207291 Introduce nested exception printing 35c4be7 Small shared two way pointer 7d247da Merge pull request diffblue#2099 from mgudemann/bugfix/build/glucose_syrup 1776a9e Merge pull request diffblue#1950 from romainbrenguier/refactor/prop_conv_straightforward 4147243 Change set_variable_name API to consume irep_idt 2d8be06 Rename `it` to pair in boolbvt::print_assignment 4365c28 Simplify boolbvt::set_to b18109f Make make_(free_)bv_expr return exprt 5724a35 Simplify loop in prop_conv::get 4987f3a Remove useless comments 13e87a9 Simplify dec_solve a0500f6 Use standard algorithm for finding an element ba13c94 Use auto for iterator types 9179571 Remove useless includes a905a07 Replace throws by invariant or preconditions 7db44fc Remove virtual keyword where not needed 990f33e Initialize at declaration instead of construction c1a93b3 Renaming `it` to symbol 8eb20f6 Use ranged for dc799e0 Assert replaced by unreachable c34e073 Add support for CaDiCaL 1bd9efd Merge pull request diffblue#2097 from peterschrammel/java-cleanup-replace a079f46 Clang-format moved file 2eb3714 Move replace_java_nondet to java_bytecode 9a8c292 Remove unnecessary include c8cf100 Remove Java refs from ANSI-C docs 0090952 Merge pull request diffblue#2096 from diffblue/cleanout-java aa3caa3 Fix CMake build for Glucose Syrup 1156930 Merge pull request diffblue#1244 from tautschnig/goto-gcc-at-fix 706e391 Merge pull request diffblue#2093 from owen-jones-diffblue/owen-jones-diffblue/remove_unnecessary_irep_id_hash 290feb4 Merge pull request diffblue#2095 from diffblue/get_json_stream_precondition ac2df21 Merge pull request diffblue#2027 from tautschnig/linking-multiple-conflicts dd0d602 Merge pull request diffblue#2030 from tautschnig/goto-cc-linux-kernel 42e58d4 Merge pull request diffblue#2085 from tautschnig/from_expr-cleanup 692f92d remove dependency on java_bytecode 8c6165d precondition for get_json_stream() e28a662 Remove unused typedef 5626fb7 Merge pull request diffblue#2092 from smowton/smowton/cleanup/diffblue-spelling 4840154 Replace stack by deque and use range-based for loop 987edbe Use range-based for loops 92ac82c Remove redundant irep_id_hash for unordered maps dc2b436 Remove redundant irep_id_hash for sets 5aa2c2d Attribute main function arguments to __CPROVER_start b7ef5af Merge pull request diffblue#2053 from owen-jones-diffblue/owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions 252474f String tests: DiffBlue -> Diffblue de1915a Merge pull request diffblue#2074 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-no-candidate-callees d73f6bc Make directed callgraph include nodes with no edges 2a45e61 Only the top-level section should be considered for renaming 9c66a66 fixup! Support __attribute__((section("x")) e133964 C front-end: Section/ASM renaming also needs to be applied to aliases 0cfc72f Test --call-graph and --reachable-call-graph 1c34d22 Test lazy-loading when there are no candidates 289a439 Deal with virtual function calls with no candidate targets 9347615 Remove incorrect comment 18b1962 Fix order of parameters in function header 82058da Store virtual function calls instead of virtual call-sites 3653550 Use unordered set of irep_ids in ci_lazy_methods c31d43f Remove code duplication 945f885 Rename two variables and make one more local b7d70e7 Replace do-while loop with equally valid while loop 58b990d Use from_{expr,type} matching the language of the expression/type 177c8c1 goto-cc: support thin ar archives, refactoring e80008e goto-cc: support GCC's print-sysroot* options 38e6fa5 Accept the --build-id option in goto-ld f3bbb12 Linking: report multiple conflicts 495f109 Fixing member offset computation in presence of bitfields 5109eab Add @<file> arguments to the original command line 97d556e Update desc file to add pass variables. eea76ec Add a regression test. c14e907 Increase AssertionError arguments allowed from 2 to 3 git-subtree-dir: cbmc git-subtree-split: 31c47c2
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Do not merge: this actually needs debugging rather than hacking something away.