-
Copy minexample.v and verif_minexample.v into VST/progs
-
Then, while in VST/progs, run coqc to create a .vo file:
coqc -Q ../../CompCert compcert -Q . VST.progs minexample.v
If you are using the compcert internal to VST, the following will likely work:
coqc -Q ../compcert compcert -Q . VST.progs minexample.v
Please note that I created this minimal example using the external CompCert.
-
Then you can open up my verif_minexample.v file.
anshumanmohan / gather_sep_issue Goto Github PK
View Code? Open in Web Editor NEWFlagging an issue in VST's gather_SEP