File tree Expand file tree Collapse file tree 4 files changed +23
-16
lines changed Expand file tree Collapse file tree 4 files changed +23
-16
lines changed Original file line number Diff line number Diff line change 4
4
use anyhow:: { bail, Result } ;
5
5
use std:: collections:: BTreeMap ;
6
6
use std:: ffi:: OsString ;
7
+ use std:: path:: PathBuf ;
8
+ use std:: process:: Command ;
7
9
use toml:: value:: Table ;
8
10
use toml:: Value ;
9
11
10
12
/// Produces a set of arguments to pass to ourself (cargo-kani) from a Cargo.toml project file
11
13
pub fn config_toml_to_args ( ) -> Result < Vec < OsString > > {
12
- // TODO: `cargo locate-project` maybe?
13
- let file = std:: fs:: read_to_string ( "Cargo.toml" ) ;
14
- if let Ok ( file) = file {
15
- toml_to_args ( & file)
16
- } else {
17
- // Suppress the error if we can't find it, for now.
18
- Ok ( vec ! [ ] )
14
+ let file = std:: fs:: read_to_string ( cargo_locate_project ( ) ?) ?;
15
+ toml_to_args ( & file)
16
+ }
17
+
18
+ /// `locate-project` produces a response like: `/full/path/to/src/cargo-kani/Cargo.toml`
19
+ fn cargo_locate_project ( ) -> Result < PathBuf > {
20
+ let cmd =
21
+ Command :: new ( "cargo" ) . args ( [ "locate-project" , "--message-format" , "plain" ] ) . output ( ) ?;
22
+ if !cmd. status . success ( ) {
23
+ let err = std:: str:: from_utf8 ( & cmd. stderr ) ?;
24
+ bail ! ( "{}" , err) ;
19
25
}
26
+ let path = std:: str:: from_utf8 ( & cmd. stdout ) ?;
27
+ // A trim is essential: remove the trailing newline
28
+ Ok ( path. trim ( ) . into ( ) )
20
29
}
21
30
22
31
/// Parse a config toml string and extract the cargo-kani arguments we should try injecting
Original file line number Diff line number Diff line change @@ -109,6 +109,10 @@ impl KaniSession {
109
109
args. push ( "--nan-check" . into ( ) ) ;
110
110
args. push ( "--pointer-overflow-check" . into ( ) ) ;
111
111
args. push ( "--undefined-shift-check" . into ( ) ) ;
112
+ // With PR #647 we use Rust's `-C overflow-checks=on` instead of:
113
+ // --unsigned-overflow-check
114
+ // --signed-overflow-check
115
+ // So these options are deliberately skipped to avoid erroneously re-checking operations.
112
116
}
113
117
if self . args . checks . unwinding_on ( ) {
114
118
args. push ( "--unwinding-assertions" . into ( ) ) ;
Original file line number Diff line number Diff line change @@ -25,12 +25,8 @@ impl KaniSession {
25
25
26
26
// Special case hack for handling the "c-ffi" abs-type
27
27
if self . args . use_abs && self . args . abs_type == AbstractionType :: CFfi {
28
- let mut vec = self . kani_c_stubs . clone ( ) ;
29
- vec. push ( "vec" ) ;
30
- vec. push ( "vec.c" ) ;
31
- let mut hashset = self . kani_c_stubs . clone ( ) ;
32
- hashset. push ( "hashset" ) ;
33
- hashset. push ( "hashset.c" ) ;
28
+ let vec = self . kani_c_stubs . join ( "vec/vec.c" ) ;
29
+ let hashset = self . kani_c_stubs . join ( "hashset/hashset.c" ) ;
34
30
35
31
args. push ( vec. into_os_string ( ) ) ;
36
32
args. push ( hashset. into_os_string ( ) ) ;
Original file line number Diff line number Diff line change @@ -8,9 +8,7 @@ use std::process::Command;
8
8
9
9
/// Replace an extension with another one, in a new PathBuf. (See tests for examples)
10
10
pub fn alter_extension ( path : & Path , ext : & str ) -> PathBuf {
11
- let mut result = path. to_owned ( ) ;
12
- result. set_extension ( ext) ;
13
- result
11
+ path. with_extension ( ext)
14
12
}
15
13
16
14
/// Add an extension to an existing file path (amazingly Rust doesn't support this well)
You can’t perform that action at this time.
0 commit comments