[BUG] Failure("TODO rearrange_start_inequality at 39:35")

[podhrmic]

When running cn test --output-dir=test -I include --include=include/wars.h --magic-comment-char-dollar components/actuation_unit.c on OpenSUT Mission Protection System I get the following error:

root@ac94c45769b6:/work/components/mission_protection_system/src# cn test --output-dir=test -I include --include=include/wars.h --magic-comment-char-dollar components/actuation_unit.c 
include/common.h:34:24: warning: experimental keyword 'cn_function' (use of experimental features is discouraged)
uint8_t c_NINSTR() /*$ cn_function NINSTR; $*/ { return NINSTR; }
                       ^~~~~~~~~~~ 
...
cn: internal error, uncaught exception:
    Failure("TODO rearrange_start_inequality at 39:35")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.generate_start_expr in file "backend/cn/lib/cn_internal_to_ail.ml", line 534, characters 11-53
    Called from Cn__Cn_internal_to_ail.cn_to_ail_resource_internal.(fun) in file "backend/cn/lib/cn_internal_to_ail.ml", line 2658, characters 21-61
    Called from Cn__Cn_internal_to_ail.cn_to_ail_lat_internal_2 in file "backend/cn/lib/cn_internal_to_ail.ml", line 3297, characters 6-81
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_aux_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3406-3412, characters 6-16
    Called from Cn__Cn_internal_to_ail.cn_to_ail_pre_post_internal in file "backend/cn/lib/cn_internal_to_ail.ml", lines 3434-3440, characters 6-16
    Called from Cn__Executable_spec_internal.generate_c_pres_and_posts_internal in file "backend/cn/lib/executable_spec_internal.ml", lines 73-79, characters 4-30
    Called from Stdlib__List.map in file "list.ml", line 87, characters 15-19
    Called from Stdlib__List.map in file "list.ml", line 88, characters 14-21
    Called from Cn__Executable_spec_internal.generate_c_specs_internal in file "backend/cn/lib/executable_spec_internal.ml", line 201, characters 14-59
    Called from Cn__Executable_spec.main in file "backend/cn/lib/executable_spec.ml", lines 221-227, characters 4-11
    Called from Dune__exe__Main.run_tests.(fun) in file "backend/cn/bin/main.ml", lines 495-504, characters 10-26
    Called from Cerb_colour.without_colour in file "util/cerb_colour.ml", line 40, characters 10-13
    Called from Dune__exe__Main.run_tests.(fun) in file "backend/cn/bin/main.ml", lines 476-531, characters 6-10
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", lines 157-168, characters 6-48
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 176, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

Note that actuation_unit.c proofs are passing (cn verify ...).

The same error (just different line number for the inequality) happens for instrumentation.c

[dc-mak]

Testing each (..) range constraints right now need a lower and an upper bound, even for unsigned integers where the intended lower bound is 0.

[dc-mak]

This is a known issue and will be fixed at some point.

[ZippeyKeys12]

Duplicate of #689