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.

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

Add support for MInt (machine integers) in k5 #50

Open
1 task
sdasgup3 opened this issue Feb 19, 2018 · 0 comments
Open
1 task

Add support for MInt (machine integers) in k5 #50

sdasgup3 opened this issue Feb 19, 2018 · 0 comments
Assignees
@sdasgup3
Labels
enhancement X86-64-Semantics
Projects
Formally definining x86-semantics
Milestone
Enable ocaml back...

Comments

@sdasgup3
Copy link
Owner

sdasgup3 commented Feb 19, 2018 •
edited
Loading

  • The ocaml backend of RuntimeVerification k (RV K) does not support MInt module. All the corresponding java hooks need to e ported in ocaml. This work help porting x-86-semantics project in RV K.
@sdasgup3 sdasgup3 self-assigned this Feb 19, 2018
@sdasgup3 sdasgup3 added this to To Do in Formally definining x86-semantics via automation Feb 19, 2018
@sdasgup3 sdasgup3 changed the title Add support for MInt (mahine integers) in RuntimeVerifiacation K Add support for MInt (machine integers) in RuntimeVerifiacation K Feb 19, 2018
@sdasgup3 sdasgup3 added this to the Enable RV K for x-86 semantics project milestone Feb 19, 2018
@sdasgup3 sdasgup3 changed the title Add support for MInt (machine integers) in RuntimeVerifiacation K Add support for MInt (machine integers) in k5 May 1, 2018
@sdasgup3 sdasgup3 moved this from To Do to In Progress in Formally definining x86-semantics Jun 4, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@sdasgup3 sdasgup3

Labels
enhancement X86-64-Semantics
Projects
Formally definining x86-semantics
  
In Progress
Milestone
Enable ocaml backend for x-86 semanti...
Development

No branches or pull requests
1 participant
@sdasgup3