Support for inline assembler & goto instructions in inline assembler
#1326
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| @@ -724,7 +724,7 @@ struct | |||
| Array (CArrays.set ask n (array_idx_top) v) | |||
| | t , Blob n -> Blob (Blobs.invalidate_value ask t n) | |||
| | _ , Thread tid -> Thread (Threads.join (Threads.top ()) tid) | |||
| | _ , JmpBuf _ -> state (* TODO: no top jmpbuf *) | |||
| | _ , JmpBuf (b, c, _) -> JmpBuf(b, c, true) | |||
There was a problem hiding this comment.
The comment should probably still remain, as we normally would have to do more here but just haven't gotten around to it yet.
jerhard
reviewed
Feb 8, 2024
| @@ -73,6 +75,17 @@ struct | |||
| ctx.local | |||
| end | |||
|
|
|||
| let asm ctx outs ins = | |||
| if not !ignore_asm then begin | |||
There was a problem hiding this comment.
Should the asm_is_top flag impact all analyses? If this check be moved into the mCP, so that it only needs to be done once?
There was a problem hiding this comment.
I think it probably should be at the FromSpec level even. And the top-level asm_is_nop option should probably be replaced with something more organized like sem.asm.nop.
3 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Depends on goblint/cil#161.
The tests with annotations will come in very few days.
We are sorry for this (right now still) unpolished state.
Changes in goblint-cil:
Changes in analyzer: all changes are switched off by default and can be turned on by --disable asm_is_nop