Skip to content

Commit

Permalink
Don't define Rust-related .bc Makefile rules on CI
Browse files Browse the repository at this point in the history
This avoids the potential for spurious rebuilding in certain situations where
the `.bc` files have different created and modified timestamps.

Fixes #1801.
  • Loading branch information
RyanGlScott committed Jan 17, 2023
1 parent bbdbd5c commit 7842ec0
Showing 1 changed file with 14 additions and 7 deletions.
21 changes: 14 additions & 7 deletions heapster-saw/examples/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -16,22 +16,29 @@ ifeq ($(SAW),)
endif
endif

# If running in GitHub Actions, the $CI environment variable will be defined
# (see https://docs.github.com/en/actions/learn-github-actions/variables#default-environment-variables)
# and these Makefile rules will not be defined. As a consequence, Make will
# /never/ rebuild .bc files. This ensures that the CI will always test the .bc
# files that were checked into version control. (See #1801 for an example of
# what can go wrong if CI rebuilds .bc files with different compilers from what
# were used to originally produce them.)
ifeq ($(CI),)
%.bc: %.c
clang -emit-llvm -g -c $<
endif

%_gen.v: %.saw %.bc
$(SAW) $<

xor_swap_rust.bc: xor_swap_rust.rs
xor_swap_rust.bc: xor_swap_rust.rs
rustc --crate-type=lib --emit=llvm-bc xor_swap_rust.rs

rust_data.bc: rust_data.rs
rust_data.bc: rust_data.rs
rustc --crate-type=lib --emit=llvm-bc rust_data.rs

rust_lifetimes.bc: rust_lifetimes.rs
rust_lifetimes.bc: rust_lifetimes.rs
rustc --crate-type=lib --emit=llvm-bc rust_lifetimes.rs
endif

%_gen.v: %.saw %.bc
$(SAW) $<

# Lists all the Mr Solver tests, without their ".saw" suffix
MR_SOLVER_TESTS = # arrays_mr_solver linked_list_mr_solver sha512_mr_solver
Expand Down

0 comments on commit 7842ec0

Please sign in to comment.