Skip to content

Commit

Permalink
Fix rmc behavior that wasn't deleting .goto files (rust-lang#587)
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval authored and tedinski committed Oct 27, 2021
1 parent 608f769 commit a60612d
Show file tree
Hide file tree
Showing 4 changed files with 16 additions and 5 deletions.
12 changes: 10 additions & 2 deletions scripts/cargo-rmc
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ def main():
out_files = rmc.symbol_table_to_gotoc(symbol_table_jsons, args.verbose, args.keep_temps, args.dry_run)

rmc.link_c_lib(out_files, cbmc_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function,
args.dry_run)
args.dry_run, args.keep_temps)

if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_runnable_filename, c_runnable_filename, args.verbose, args.dry_run):
return 1
Expand All @@ -61,7 +61,15 @@ def main():

args.c_lib.append(str(RMC_C_LIB))

rmc.link_c_lib(out_files, cbmc_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run)
rmc.link_c_lib(
out_files,
cbmc_filename,
args.c_lib,
args.verbose,
args.quiet,
args.function,
args.dry_run,
args.keep_temps)

if args.gen_c:
if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose, args.dry_run):
Expand Down
5 changes: 3 additions & 2 deletions scripts/rmc
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ def main():
out_files = rmc.symbol_table_to_gotoc([json_runnable_filename], args.verbose, args.keep_temps, args.dry_run)

rmc.link_c_lib(out_files, goto_runnable_filename, args.c_lib, args.verbose, args.quiet, args.function,
args.dry_run)
args.dry_run, args.keep_temps)

if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_runnable_filename, c_runnable_filename, args.verbose, args.dry_run):
return 1
Expand Down Expand Up @@ -81,7 +81,8 @@ def main():
RMC_C_HASHSET = RMC_C_STUB / "hashset" / "hashset.c"
args.c_lib.append(str(RMC_C_HASHSET))

rmc.link_c_lib(out_files, goto_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run)
rmc.link_c_lib(out_files, goto_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run,
args.keep_temps)

if args.gen_c:
if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose, args.dry_run):
Expand Down
4 changes: 3 additions & 1 deletion scripts/rmc.py
Original file line number Diff line number Diff line change
Expand Up @@ -227,8 +227,10 @@ def symbol_table_to_gotoc(json_files, verbose=False, keep_temps=False, dry_run=F
return out_files

# Links in external C programs into a goto program
def link_c_lib(srcs, dst, c_lib, verbose=False, quiet=False, function="main", dry_run=False):
def link_c_lib(srcs, dst, c_lib, verbose=False, quiet=False, function="main", dry_run=False, keep_temps=False):
cmd = ["goto-cc"] + ["--function", function] + srcs + c_lib + ["-o", dst]
if not keep_temps:
atexit.register(delete_file, dst)
if run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run) != EXIT_CODE_SUCCESS:
raise Exception("Failed to run command: {}".format(" ".join(cmd)))

Expand Down
File renamed without changes.

0 comments on commit a60612d

Please sign in to comment.