…2537)

This will ensure we run Kani extra validation checks in our libraries.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Celina G. Val <celinval@amazon.com>

The Kani attributes were being lazily evaluated in some cases. We have also been handling duplicated attribute inconsistently.

Instead, validate all the attributes upfront and print all the errors found. Also, for all attributes that multiple occurrences is redundant, we emit an error if user provides 2 or more.

…iler (#2552)

The tests below started failing as part of the latest toolchain update because the value produced by intrinsics is not used, and the compiler just removes them.

To avoid that to happen, we now wrap those calls with the black_box std function to avoid compiler optimizations.

This PR fixes a few flaky tests that started to fail in the ongoing toolchain update (#2551)

- The object bits test itself doesn't create that many objects since an array is represented as the same allocated object. Use LinkedList instead.
- Do not rely on property number.
- Do not rely on the order that failed checks is printed.

This was a regression introduced by #2439. We were still writing the result of the reachability algorithm to the same file for every harness. Thus, we could only see the MIR for the last harness that was processed.

Use the file name that is specific for the harness instead and generate one MIR file per harness like we do with other files generated by kani-compiler.

This fixes a Graphviz graph not being rendered in the Kani book.

This allows users to write their own custom visualization script to run
after running the benchmarks. Prior to this commit, visualizations had
to be checked into the Kani repository.

When run_command is specified as a visualization, benchcomp runs the
specified command and passes the result of the run as a JSON file on
stdin. The command can then process the result however it likes.

This resolves #2518.

Co-authored-by: Kareem Khazem <karkhaz@amazon.com>
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>