Commit f814676 1 parent eaab5cf commit f814676 Copy full SHA for f814676
File tree 9 files changed +23
-4
lines changed
kani-compiler/src/kani_middle
cargo_autoverify_contracts
cargo_autoverify_harnesses_fail
cargo_autoverify_loops_fixme
9 files changed +23
-4
lines changed Original file line number Diff line number Diff line change @@ -104,8 +104,8 @@ impl CodegenUnits {
104
104
// and these harnesses have no stubs.
105
105
units. extend (
106
106
automatic_harnesses
107
- . iter ( )
108
- . map ( |( harness, _ ) | CodegenUnit {
107
+ . keys ( )
108
+ . map ( |harness| CodegenUnit {
109
109
harnesses : vec ! [ * harness] ,
110
110
stubs : HashMap :: default ( ) ,
111
111
} )
Original file line number Diff line number Diff line change @@ -71,7 +71,7 @@ impl ValidateArgs for CargoAutoverifyArgs {
71
71
ErrorKind :: MissingRequiredArgument ,
72
72
format ! (
73
73
"The `autoverify` subcommand is unstable and requires -Z {}" ,
74
- UnstableFeature :: UnstableOptions . to_string ( )
74
+ UnstableFeature :: UnstableOptions
75
75
) ,
76
76
) ) ;
77
77
}
@@ -105,7 +105,7 @@ impl ValidateArgs for StandaloneAutoverifyArgs {
105
105
ErrorKind :: MissingRequiredArgument ,
106
106
format ! (
107
107
"The `autoverify` subcommand is unstable and requires -Z {}" ,
108
- UnstableFeature :: UnstableOptions . to_string ( )
108
+ UnstableFeature :: UnstableOptions
109
109
) ,
110
110
) ) ;
111
111
}
Original file line number Diff line number Diff line change @@ -228,6 +228,7 @@ pub mod tests {
228
228
goto_file : model_file,
229
229
contract : Default :: default ( ) ,
230
230
has_loop_contracts : false ,
231
+ is_automatically_generated : false ,
231
232
}
232
233
}
233
234
Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
1
4
[package ]
2
5
name = " cargo_autoverify_contracts"
3
6
version = " 0.1.0"
Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
1
4
[package ]
2
5
name = " cargo_autoverify_include"
3
6
version = " 0.1.0"
Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
1
4
[package ]
2
5
name = " cargo_autoverify_filter"
3
6
version = " 0.1.0"
Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
1
4
[package ]
2
5
name = " cargo_autoverify_harnesses_fail"
3
6
version = " 0.1.0"
Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
1
4
[package ]
2
5
name = " cargo_autoverify_include"
3
6
version = " 0.1.0"
Original file line number Diff line number Diff line change
1
+ # Copyright Kani Contributors
2
+ # SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
1
4
[package ]
2
5
name = " cargo_autoverify_loops_fixme"
3
6
version = " 0.1.0"
You can’t perform that action at this time.
0 commit comments