Skip to content

Figure out how time distribution is computed on harness module or function module #136

@zjp-CN

Description

@zjp-CN

core::f64 module has time distribution, but there are no harness under it.
The time matrix is probably computed for a function module, instead of harness module.
However, it'd be weird to have zero harness on the right chart with verification time on the left.
Maybe it'd be good to compute time merely on harness module.

Harness Name: 
convert::num::verify::check_f16_to_int_unchecked::f64::i128::check_float_to_int_unchecked
Crate: core
Harness File: core/src/convert/num.rs
Harness Hash: 1797053298718753334516989592935679000737
Proof Kind: Contract
Total Properties: 48
Execution Time: 89ms

Verified Function: 
f64::<impl f64>::to_int_unchecked
Function File: core/src/num/f64.rs
Image Image

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions