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.

Sign up for GitHub

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

Jump to bottom

Basic PowerPC support in Vale #1

Open

mamonet opened this issue May 20, 2022 · 0 comments

Owner

mamonet commented May 20, 2022

Adding basic support of PowerPC architecture to Vale which include the following modules:

fstar/specs/hardware/PPC64LE.Machine_s
fstar/specs/hardware/PPC64LE.Print_s
fstar/specs/hardware/PPC64LE.Semantics_s
fstar/code/arch/ppc64le/PPC64LE.Vale.Decls
fstar/code/arch/ppc64le/PPC64LE.Vale.State
fstar/code/arch/ppc64le/PPC64LE.Vale.Lemmas
fstar/code/arch/ppc64le/PPC64LE.Vale.StateLemmas
fstar/code/arch/ppc64le/PPC64LE.Vale.Regs
fstar/code/arch/ppc64le/PPC64LE.Vale.Vecs
fstar/code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf
fstar/code/arch/ppc64le/PPC64LE.Vale.InsBasic.vaf
fstar/code/arch/ppc64le/PPC64LE.Vale.InsVec.vaf
fstar/code/test/PPC64LE.Test.Memcpy.vaf
fstar/code/test/PPC64LE.Test.Basics.vaf
fstar/code/test/PowerTest.c
fstar/code/test/PowerTest.ml

The patch also integrates testing process to build system SCons that tests verified assembly modules.

The patch has been pushed to ppc-basic branch in https://github.com/mamonet/vale repository.

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment