Add a Kani function that checks if the range of a float is valid for conversion to int #9021

	# Copyright Kani Contributors
	# SPDX-License-Identifier: Apache-2.0 OR MIT
	name: Kani Format Check
	on:
	pull_request:
	merge_group:
	push:
	# Not just any push, as that includes tags.
	# We don't want to re-trigger this workflow when tagging an existing commit.
	branches:
	- '**'

	jobs:
	format-check:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout Kani
	uses: actions/checkout@v4

	- name: Execute copyright check
	run: ./scripts/ci/run-copyright-check.sh

	# Ignore failures here for now until we can pindown a version.
	- name: Check C code formatting
	continue-on-error: true
	run: ./scripts/run-clang-format.sh -d

	- name: Check Python code formatting
	run: \|
	pip3 install --upgrade autopep8
	./scripts/run-autopep8.sh

	clippy-check:
	runs-on: ubuntu-20.04
	steps:
	- name: Checkout Kani
	uses: actions/checkout@v4

	- name: Setup Kani Dependencies
	uses: ./.github/actions/setup
	with:
	os: ubuntu-20.04

	- name: 'Install jq for parsing.'
	run: \|
	sudo apt-get install -y jq

	- name: 'Run Clippy'
	run: \|
	cargo clippy --workspace -- -D warnings

	- name: 'Print Clippy Statistics'
	run: \|
	rm .cargo/config.toml
	(cargo clippy --all --message-format=json 2>/dev/null \| \
	jq 'select(.message!=null) \| .message.code.code' \| grep -v '^null$' \| \
	sort \| uniq -c) \|\| true

Provide feedback