pragma checks on array simple assignment cause invariant failure

[sonodtt]

This issue is within the context of PR 83 and will hopefully be short-lived, so documentation will be a bit more brief.

pragma checks on array simple assignment cause invariant failure

• pragma on array assignment with malloc causes invariant failure
• pragma on array simple assignment via alloc causes invariant failure

e.g.

• "unimplemented"

Invariant check failed
File: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/flattening/boolbv_width.cpp:202 function: get_entry
Condition: false
Reason: Unimplemented
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4d) [0x55cd669c84aa]
cbmc(get_backtraceabi:cxx11+0x45) [0x55cd669c86b1]
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, std::allocator > const&>(std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, int, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&)+0x4c) [0x55cd66416851]
cbmc(+0x60936b) [0x55cd6641536b]
cbmc(boolbv_widtht::get_entry(typet const&) const+0x130a) [0x55cd6683723e]
cbmc(boolbv_widtht::operator()(typet const&) const+0x23) [0x55cd66802855]
cbmc(bv_pointerst::convert_bitvector(exprt const&)+0xe82) [0x55cd66843838]
cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional)+0x100) [0x55cd667f80fe]
cbmc(boolbvt::boolbv_set_equality_to_true(equal_exprt const&)+0x17f) [0x55cd667fd6a3]
cbmc(boolbvt::set_to(exprt const&, bool)+0x181) [0x55cd667fd8e5]
cbmc(decision_proceduret::set_to_true(exprt const&)+0x30) [0x55cd6669f438]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&) const+0x104) [0x55cd6669ad1c]
cbmc(symex_target_equationt::convert(prop_convt&)+0x48) [0x55cd6669aa92]
cbmc(bmct::do_conversion()+0x5a) [0x55cd6641e00c]
cbmc(bmc_all_propertiest::operator()()+0x11a) [0x55cd6646cad4]
cbmc(bmct::all_properties(goto_functionst const&, prop_convt&)+0x8b) [0x55cd6646eb3f]
cbmc(bmct::decide(goto_functionst const&, prop_convt&)+0xe2) [0x55cd664203be]
cbmc(bmct::execute(abstract_goto_modelt&)+0x855) [0x55cd6641f77d]
cbmc(bmct::run(abstract_goto_modelt&)+0x2f) [0x55cd664202d9]
cbmc(bmct::do_language_agnostic_bmc(path_strategy_choosert const&, optionst const&, abstract_goto_modelt&, ui_message_handlert&, std::function<void (bmct&, symbol_tablet const&)>, std::function<bool ()>)+0x42d) [0x55cd66420eef]
cbmc(cbmc_parse_optionst::doit()+0x842) [0x55cd66412f4a]
cbmc(parse_options_baset::main()+0xe8) [0x55cd669f3288]
cbmc(main+0x55) [0x55cd6640bc1f]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f3a0ce58b97]
cbmc(_start+0x2a) [0x55cd6640baea]

--- end invariant violation report ---

=========================================

• "type clash"

Invariant check failed
File: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/flattening/boolbv_equality.cpp:27 function: convert_equality
Condition: types of expressions on each side of equality should match
Reason: is_base_type_eq
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x4d) [0x55e60d3864aa]
cbmc(get_backtraceabi:cxx11+0x45) [0x55e60d3866b1]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_with_diagnostics_failedt>::value, void>::type invariant_violated_structured<invariant_with_diagnostics_failedt, std::__cxx11::basic_string<char, std::char_traits, std::allocator >&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > >(std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, int, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator >&, std::__cxx11::basic_string<char, std::char_traits, std::allocator >&&)+0x53) [0x55e60cf50973]
cbmc(void report_invariant_failure<irep_pretty_diagnosticst, irep_pretty_diagnosticst>(std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, std::__cxx11::basic_string<char, std::char_traits, std::allocator > const&, int, std::__cxx11::basic_string<char, std::char_traits, std::allocator >, std::__cxx11::basic_string<char, std::char_traits, std::allocator >, irep_pretty_diagnosticst&&, irep_pretty_diagnosticst&&)+0x8c) [0x55e60d1d235d]
cbmc(boolbvt::convert_equality(equal_exprt const&)+0x1c5) [0x55e60d1d1425]
cbmc(boolbvt::convert_rest(exprt const&)+0x1fe) [0x55e60d1b8ff4]
cbmc(bv_pointerst::convert_rest(exprt const&)+0x898) [0x55e60d1fc7b2]
cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x1404) [0x55e60d230ee6]
cbmc(prop_conv_solvert::convert(exprt const&)+0x19d) [0x55e60d22fa31]
cbmc(prop_conv_solvert::set_to(exprt const&, bool)+0x797) [0x55e60d231c23]
cbmc(boolbvt::set_to(exprt const&, bool)+0x1bc) [0x55e60d1bb920]
cbmc(decision_proceduret::set_to_true(exprt const&)+0x30) [0x55e60d05d438]
cbmc(symex_target_equationt::convert_assignments(decision_proceduret&) const+0x104) [0x55e60d058d1c]
cbmc(symex_target_equationt::convert(prop_convt&)+0x48) [0x55e60d058a92]
cbmc(bmct::do_conversion()+0x5a) [0x55e60cddc00c]
cbmc(bmc_all_propertiest::operator()()+0x11a) [0x55e60ce2aad4]
cbmc(bmct::all_properties(goto_functionst const&, prop_convt&)+0x8b) [0x55e60ce2cb3f]
cbmc(bmct::decide(goto_functionst const&, prop_convt&)+0xe2) [0x55e60cdde3be]
cbmc(bmct::execute(abstract_goto_modelt&)+0x855) [0x55e60cddd77d]
cbmc(bmct::run(abstract_goto_modelt&)+0x2f) [0x55e60cdde2d9]
cbmc(bmct::do_language_agnostic_bmc(path_strategy_choosert const&, optionst const&, abstract_goto_modelt&, ui_message_handlert&, std::function<void (bmct&, symbol_tablet const&)>, std::function<bool ()>)+0x42d) [0x55e60cddeeef]
cbmc(cbmc_parse_optionst::doit()+0x842) [0x55e60cdd0f4a]
cbmc(parse_options_baset::main()+0xe8) [0x55e60d3b1288]
cbmc(main+0x55) [0x55e60cdc9c1f]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7f7072a7db97]
cbmc(_start+0x2a) [0x55e60cdc9aea]
Diagnostics:
<< EXTRA DIAGNOSTICS >>
symbol

• type: pointer
  • width: 64
    0: signedbv
    • width: 32
• identifier: __new_array2!0@1#2
• expression: symbol
  • type: pointer
    • width: 64
      0: signedbv
      • width: 32
  • identifier: __new_array2
  • range_check: 0
  • #source_location: source_location
• L0: 0
• L1: 1
• L2: 2
• L1_object_identifier: __new_array2!0@1
• #SSA_symbol: 1
  code
• type: pointer
  • width: 64
    0: empty
• statement: function_call
• range_check: 0
• #source_location: source_location
  0: symbol
  • type: code
    • return_type: nil
    • ellipsis: 0
    • parameters: nil
    • #inlined: 0
    • #KnR: 0
  • identifier: malloc
  • range_check: 0
  • #source_location: source_location
    1: arguments
  • type:
    0: *
    • type: integer
    • range_check: 0
    • overflow_check: 0
    • #source_location: source_location
      0: constant
      • type: signedbv
        • width: 32
      • value: 3
        1: constant
      • type: signedbv
        • width: 32
      • value: 00000000000000000000000000100000
      • range_check: 0
      • #source_location: source_location
        << END EXTRA DIAGNOSTICS >>
        --- end invariant violation report

[xbauch]

With the new implementation of arrays, this no longer occurs.