tool: add --viper-output option#534
Conversation
|
Not sure why the DCO check fails, it looks like all new commits are signed off. I expect a possible |
|
If you click on DCO it tells you why:
Though admittedly I don't know why that commit exists still |
zaklogician
force-pushed
the
viper/export-final
branch
from
4ed2707 to
f22260f
Compare
|
Okay, the DCO issue should be fixed now. |
midnightveil
left a comment
midnightveil
left a comment
There was a problem hiding this comment.
LGTM. Few extra things to fix up but once done will merge.
|
Not sure why GitHub is suggesting the github no-reply address, but I should point out that the no-reply address is generally not an acceptable DCO sign-off (unless the change is trivial in which case we don't really care). The DCO is a legal copyright declaration, so it should ideally be from the employer email address if it is done under an employer who has copyright claims, or at least some other contactable email address. |
zaklogician
force-pushed
the
viper/export-final
branch
from
d1d3e42 to
7eccdf5
Compare
|
@lsf37 Thanks for letting me know. I will need a source from an official place which states that, otherwise I'll leave it as it is. |
zaklogician
force-pushed
the
viper/export-final
branch
from
7eccdf5 to
c9dc969
Compare
zaklogician
force-pushed
the
viper/export-final
branch
2 times, most recently
from
196f857 to
acd7ae9
Compare
This resolves a rebase issue which comes from the requirement to have the current working directory as part of the search paths. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
We implement the `--viper-output` command line argument which lets one dump the capability table of a PD into a Viper file for verification purposes. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Add a section to the manual explaining the new viper output options. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
We add --viper-output to the hello example. This will let us test that future changes do not break the Viper export functionality. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
midnightveil
force-pushed
the
viper/export-final
branch
from
acd7ae9 to
0519d8d
Compare
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Looks like the DCO checker is just dumb. I'd recommend using the same address as the committer just to avoid the annoyance in the future, but the DCO requirement as such is fine. I can set it to passing manually.
|
I've just force pushed and made the sign-off/committer me because it was complaining about that (Zoltan does not wish to link UNSW email to GitHub for authorship) If you're happy to press the DCO bypass button again I can make the sign-off Zoltan's again, but I don't know if it matters that much. |
You signing off on behalf of Zoltan is fine, the DCO explicitly allows that. |
|
@zaklogician not sure what your reason is, but if it is spam protection, an option might be to set up an alias or another address that you can filter on. The requirement is that it is contactable, it doesn't have to be real name (or from the employer, even though that would be preferable). The problem with GitHub's no-reply address is the "no reply" part of it. |
3 participants
As part of a series of patches which upstream Viper export to Microkit, we add the
--viper-output VIPER_OUTPUT_DIRcommand line option to the Microkit tool.If this option is set, then after the systems is built, the tool will emit
VIPER_OUTPUT_DIR/name.vprfor each protection domainnamespecified in the system description file. The output consists of a description of the capability table of the given PD in the Viper verification language, generated from the same output that the CapDL loader uses. This makes the capability tables available for verification tasks.