Clippy Compliance within Kani

[YoshikiTakashima]

As noted by @giltho & @celinval, there is a lot of clippy warnings in
Kani. This issue is for tracking compliance and tasks related to
measuring compliance.

• Figure out which parts of Kani have Clippy warnings, and how many.
  • All 32 top-level hard errors come from kani-compiler.
    • This result does not conflict with people getting 100+ issues
      since these are top-level errors. Some errors may contain
      sub-errors, and we exclude all warnings.
  • When warnings are included, the breakdown is as follows.
    

{'library/kani': 3,
 'src': 55,
 'cprover_bindings': 17,
 'kani-driver': 6,
 'kani-compiler': 23,
 'tools/bookrunner': 5,
 'tools/compiletest': 44}

• Add Clippy warnings to script/kani-regressions.sh. For now,
  explicitly ignore libraries that warnings, and incrementally
  remove them as they are fixed.

[YoshikiTakashima]

Commands

cargo clippy --all  --message-format=json > clippy-logs.json-lines
cat clippy-logs.json-lines | \
   jq 'select(.message!=null) | select(.message.rendered | test(".*error:.*")) | .message' | \
   grep 'file_name'

The first line generates the logs in line-delimited json. The second
line selects log items that have messages that match errors. Third
line selects grep for file name field. (note, some of the structures
are recursive so grep is a bit quicker

[YoshikiTakashima]

@celinval Shall we enable -D warnings for clippy as well? I recall they are enabled for cargo build.

P.S. Will enable.

[YoshikiTakashima]

For regression:

cargo clippy --all-targets --all-features -- -D warnings

[celinval]

Yes, please go ahead and add them to the regression!

[YoshikiTakashima]

As per discussion on #1389, we permanently will ignore these two.

@YoshikiTakashima The two lints are called expect_fun_call and or_fun_call.

[YoshikiTakashima]

For actual kinds of warnings:

cargo clippy --all --message-format=json  | \
jq 'select(.message!=null) | .message.code.code' | grep -v '^null$' | \
sort | uniq -c

Gives the following.

  54 "clippy::cargo_common_metadata"
   3 "clippy::collapsible_else_if"
   5 "clippy::derive_partial_eq_without_eq"
   1 "clippy::expect_fun_call"
   2 "clippy::format_push_string"
   1 "clippy::into_iter_on_ref"
   1 "clippy::iter_skip_next"
   1 "clippy::let_and_return"
   1 "clippy::manual_map"
   1 "clippy::manual_range_contains"
   1 "clippy::manual_strip"
   1 "clippy::missing_safety_doc"
   1 "clippy::module_inception"
   1 "clippy::needless_bool"
   3 "clippy::needless_borrow"
   1 "clippy::needless_range_loop"
   2 "clippy::new_without_default"
   3 "clippy::or_fun_call"
   1 "clippy::ptr_arg"
   1 "clippy::single_char_pattern"
   1 "clippy::vec_init_then_push"

[tedinski]

For the cargo metadata one, I was irritated that it issued those warnings for all crates when I tried enabling it for just one.

But the simple fix there seems like it will ignore crates that are publish = false, so that's probably the expedient fix for those.

[YoshikiTakashima]

After #1429

      5 "clippy::derive_partial_eq_without_eq"
      1 "clippy::manual_map"
      2 "clippy::map_entry"
      2 "clippy::module_inception"
      1 "clippy::new_ret_no_self"
      2 "clippy::new_without_default"
      1 "clippy::too_many_arguments"
      2 "clippy::type_complexity"