Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

-dc -dparse don't work for clightgen #298

Closed
bcip opened this issue Jun 21, 2019 · 1 comment
Closed

-dc -dparse don't work for clightgen #298

bcip opened this issue Jun 21, 2019 · 1 comment

Comments

@bcip
Copy link

bcip commented Jun 21, 2019

I am working on my own copy but there should be the same issue in master branch. When using clightgen, flags -dc and -dparse don't have any actual effect. The following modification should fix this problem.

In compile_c_file of exportclight/Clightgen.ml, add the following lines:

let set_dest dst opt ext =
    dst := if !opt then Some (output_filename sourcename ".c" ext)
      else None in
  set_dest Cprint.destination option_dparse ".parsed.c";
  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
  set_dest PrintClight.destination option_dclight ".light.c";
@bschommer
Copy link
Member

Should be fixed by commit 1574cf2.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants