File tree Expand file tree Collapse file tree 2 files changed +31
-3
lines changed Expand file tree Collapse file tree 2 files changed +31
-3
lines changed Original file line number Diff line number Diff line change @@ -256,10 +256,10 @@ if(WITH_JBMC)
256
256
add_subdirectory (jbmc )
257
257
endif ()
258
258
259
- option (WITH_RUST_API "Build with the CPROVER Rust API" ON )
260
- if (${CMAKE_VERSION} VERSION_LESS "3.19.0" )
259
+ option (WITH_RUST_API "Build with the CPROVER Rust API" OFF )
260
+ if (${CMAKE_VERSION} VERSION_LESS "3.19.0" AND WITH_RUST_API )
261
261
message ("Unable to build the Rust API without version CMake 3.19.0" )
262
- message ("(The Rust build depends on CMake plugins with dependencies on CMake 3.19.0 and above)" )
262
+ message (FATAL_ERROR "(The Rust build depends on CMake plugins with dependencies on CMake 3.19.0 and above)" )
263
263
else ()
264
264
if (WITH_RUST_API )
265
265
include (FetchContent )
Original file line number Diff line number Diff line change @@ -562,3 +562,31 @@ then run make as follows.
562
562
cd unit
563
563
make test
564
564
```
565
+
566
+ ## Rust API
567
+
568
+ CBMC is now offering a [ Rust API] ( src/libcprover-rust/ ) . To build that along with
569
+ CBMC, you need two things:
570
+
571
+ - Rust/Cargo, instructions the installation of which can be found [ here] ( https://www.rust-lang.org/tools/install ) , and
572
+ - CMake (the Rust API doesn't support being built with ` Make ` yet)
573
+ - Version ` 3.19.0 ` + is required for the build, because of a dependency on CMake modules
574
+ that need the higher version themselves.
575
+
576
+ Provided these two are available, you can perform a CBMC build * including*
577
+ the Rust API by passing in the option ` WITH_RUST_API ` to ` CMake ` like this:
578
+
579
+ ``` sh
580
+ $ cmake -S. -Bbuild -DWITH_RUST_API=ON < other_options>
581
+ [...]
582
+ -- Rust Target: aarch64-apple-darwin
583
+ -- Found Rust: /opt/homebrew/bin/rustc (found version " 1.66.1" )
584
+ -- Using Corrosion as a subdirectory
585
+ -- Configuring done
586
+ -- Generating done
587
+ -- Build files have been written to: cbmc/build
588
+ ```
589
+
590
+ If you come across any issues during the configuration or the build of the Rust API,
591
+ please let us know by filing a [ bug report] ( https://github.com/diffblue/cbmc/issues/new )
592
+ and mark it with the label ` Rust API ` if possible.
You can’t perform that action at this time.
0 commit comments