Skip to content
Snippets Groups Projects
Commit 6a2ade56 authored by andrew_miranti's avatar andrew_miranti
Browse files

Merge branch 'master' into integration

parents 9482fa2a 4b3a50c5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
decoder.k
+ 3
− 0
View file @ 6a2ade56
...@@ -512,15 +512,18 @@ module DECODER ...@@ -512,15 +512,18 @@ module DECODER
requires I:Int =/=Int 0 // Already saw VEX, bail out. requires I:Int =/=Int 0 // Already saw VEX, bail out.
rule <k> ScanForEVEX => DecoderOutOfBytes ... </k> rule <k> ScanForEVEX => DecoderOutOfBytes ... </k>
<VEXVALID> 0 </VEXVALID>
<decoderBuffer> .Ints </decoderBuffer> <decoderBuffer> .Ints </decoderBuffer>
rule <k> ScanForEVEX => . ... </k> rule <k> ScanForEVEX => . ... </k>
<VEXVALID> 0 </VEXVALID>
<decoderBuffer> I:Int Is:Ints </decoderBuffer> <decoderBuffer> I:Int Is:Ints </decoderBuffer>
requires I:Int =/=Int 98 requires I:Int =/=Int 98
syntax K ::= "ParseEVEX" | "VerifyNotBound" syntax K ::= "ParseEVEX" | "VerifyNotBound"
rule <k> ScanForEVEX => VerifyNotBound ... </k> rule <k> ScanForEVEX => VerifyNotBound ... </k>
<VEXVALID> 0 </VEXVALID>
<decoderBuffer> 98 Is </decoderBuffer> <decoderBuffer> 98 Is </decoderBuffer>
rule <k> VerifyNotBound => ParseEVEX ... </k> rule <k> VerifyNotBound => ParseEVEX ... </k>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment