Skip to content

First1 is hard-coded as a struct member name #127

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
xbauch opened this issue Feb 18, 2019 · 0 comments
Open

First1 is hard-coded as a struct member name #127

xbauch opened this issue Feb 18, 2019 · 0 comments

Comments

@xbauch
Copy link
Contributor

xbauch commented Feb 18, 2019 •
edited
Loading

And that's probably not correct for multi-dimensional arrays. Running test-case arrays.adb (in PR#124) now gives:

Starting program: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc arrays.json_symtab
CBMC version 5.11 (cbmc-5.11-850-g71bdebf63) 64-bit x86_64 linux
Parsing arrays.json_symtab
Converting
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
--- begin invariant violation report ---
Invariant check failed
File: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/simplify_expr_struct.cpp:143 function: simplify_member
Condition: base_type_eq(op.operands()[number].type(), expr.type(), ns)
Reason: member expression type must match component type
Backtrace:
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(print_backtrace(std::ostream&)+0x4d) [0x55555614c3ba]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(get_backtrace[abi:cxx11]()+0x45) [0x55555614c5c1]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x4c) [0x555555b74689]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(+0x61f165) [0x555555b73165]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(simplify_exprt::simplify_member(exprt&)+0x953) [0x5555561ad7eb]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(simplify_exprt::simplify_node(exprt&)+0x372) [0x55555618ebc8]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(simplify_exprt::simplify_rec(exprt&)+0x60) [0x55555618f9be]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(simplify_exprt::simplify(exprt&)+0x23) [0x55555618fa53]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(simplify(exprt&, namespacet const&)+0x46) [0x55555618faa2]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(value_sett::make_member(exprt const&, dstringt const&, namespacet const&)+0xb4) [0x555555f42798]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(value_sett::assign(exprt const&, exprt const&, namespacet const&, bool, bool)+0x428) [0x555555f3fada]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symex_statet::assignment(ssa_exprt&, exprt const&, namespacet const&, bool, bool, bool)+0x866) [0x555555db9bfe]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_assign_symbol(goto_symex_statet&, ssa_exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet)+0x1b2) [0x555555e1ec40]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_assign_rec(goto_symex_statet&, exprt const&, exprt const&, exprt const&, guardt&, symex_targett::assignment_typet)+0xe4) [0x555555e1e068]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_assign(goto_symex_statet&, code_assignt const&)+0x6ac) [0x555555e1d438]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&)+0x742) [0x555555e0f3f4]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(symex_bmct::symex_step(std::function<goto_functiont const& (dstringt const&)> const&, goto_symex_statet&)+0x362) [0x555555bd8b28]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_threaded_step(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&)+0x34) [0x555555e0e492]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_with_state(goto_symex_statet&, std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&)+0x212) [0x555555e0e86a]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(goto_symext::symex_from_entry_point_of(std::function<goto_functiont const& (dstringt const&)> const&, symbol_tablet&)+0x10f) [0x555555e0eb85]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::perform_symbolic_execution(std::function<goto_functiont const& (dstringt const&)>)+0x5b) [0x555555b8b985]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::execute(abstract_goto_modelt&)+0x7f) [0x555555b8911b]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::run(abstract_goto_modelt&)+0xb4) [0x555555b89e6a]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::do_language_agnostic_bmc(optionst const&, abstract_goto_modelt&, ui_message_handlert&, std::function<void (bmct&, symbol_tablet const&)>, std::function<bool ()>)+0x2d3) [0x555555b8a8b3]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(cbmc_parse_optionst::doit()+0xa1b) [0x555555b7c53f]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(parse_options_baset::main()+0x10f) [0x5555561718a7]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(main+0x55) [0x555555b72ebf]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7ffff70c6b97]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(_start+0x2a) [0x555555b72d8a]


--- end invariant violation report ---

Program received signal SIGABRT, Aborted.
__GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:51
51	../sysdeps/unix/sysv/linux/raise.c: No such file or directory.
(gdb) up
#1  0x00007ffff70e5801 in __GI_abort () at abort.c:79
79	abort.c: No such file or directory.
(gdb) 
#2  0x0000555555b746f0 in invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&> (
    file="/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/simplify_expr_struct.cpp", function="simplify_member", line=143, 
    condition="base_type_eq(op.operands()[number].type(), expr.type(), ns)", params#0="member expression type must match component type")
    at /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/invariant.h:236
236	  abort();
(gdb) 
#3  0x0000555555b73165 in invariant_violated_string (file="/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/simplify_expr_struct.cpp", function="simplify_member", line=143, 
    condition="base_type_eq(op.operands()[number].type(), expr.type(), ns)", reason="member expression type must match component type")
    at /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/invariant.h:257
257	  invariant_violated_structured<invariant_failedt>(
(gdb) 
#4  0x00005555561ad7eb in simplify_exprt::simplify_member (this=0x7fffffffbaa0, expr=...) at /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/simplify_expr_struct.cpp:141
141	        DATA_INVARIANT(
(gdb) call puts(expr.pretty(0,0).c_str())
member
  * type: signedbv
      * width: 32
  * component_name: first2
  0: struct
      * type: struct
          * tag: arrays__Tarr7B
          * components: 
            0: 
              * type: signedbv
                  * width: 32
              * #source_location: source_location
              * #is_padding: 0
              * name: first1
              * access: public
              * anonymous: 0
              * range_check: 0
              * baseName: first1
              * prettyName: first1
            1: 
              * type: signedbv
                  * width: 32
              * #source_location: source_location
              * #is_padding: 0
              * name: last1
              * access: public
              * anonymous: 0
              * range_check: 0
              * baseName: last1
              * prettyName: last1
            2: 
              * type: signedbv
                  * width: 32
              * #source_location: source_location
              * #is_padding: 0
              * name: first2
              * access: public
              * anonymous: 0
              * range_check: 0
              * baseName: first2
              * prettyName: first2
            3: 
              * type: signedbv
                  * width: 32
              * #source_location: source_location
              * #is_padding: 0
              * name: last2
              * access: public
              * anonymous: 0
              * range_check: 0
              * baseName: last2
              * prettyName: last2
            4: 
              * type: pointer
                  * width: 64
                  0: signedbv
                      * width: 32
              * #source_location: source_location
              * #is_padding: 0
              * name: data
              * access: public
              * anonymous: 0
              * range_check: 0
              * baseName: data
              * prettyName: data
      * #source_location: source_location
          * file: arrays.adb
          * line: 19
          * column: 32
      * range_check: 0
      0: constant
          * type: signedbv
              * width: 32
          * #source_location: source_location
              * file: arrays.adb
              * line: 10
              * column: 32
          * value: 1
          * range_check: 0
      1: constant
          * type: signedbv
              * width: 32
          * #source_location: source_location
              * file: arrays.adb
              * line: 19
              * column: 32
          * value: 3
          * range_check: 0
      2: typecast
          * type: pointer
              * width: 64
              0: signedbv
                  * width: 32
          * #source_location: source_location
              * file: arrays.adb
              * line: 19
              * column: 32
          * range_check: 0
          0: address_of
              * type: pointer
                  * width: 64
                  0: unsignedbv
                      * width: 8
                      * #c_type: unsigned_char
              0: index
                  * type: unsignedbv
                      * width: 8
                      * #c_type: unsigned_char
                  0: symbol
                      * type: array
                          * size: constant
                              * type: unsignedbv
                                  * width: 64
                              * value: C
                          * #dynamic: 1
                          0: unsignedbv
                              * width: 8
                              * #c_type: unsigned_char
                      * identifier: symex_dynamic::dynamic_object5
                      * expression: symbol
                          * type: array
                              * size: constant
                                  * type: unsignedbv
                                      * width: 64
                                  * value: C
                              * #dynamic: 1
                              0: unsignedbv
                                  * width: 8
                                  * #c_type: unsigned_char
                          * identifier: symex_dynamic::dynamic_object5
                      * #SSA_symbol: 1
                      * L1_object_identifier: symex_dynamic::dynamic_object5
                  1: constant
                      * type: signedbv
                          * width: 64
                          * #c_type: signed_long_int
                      * value: 0
$1 = 4536
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@xbauch