[WIP] Initial commit to dump_c #27
Draft
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
Using the command dump_c, uclid will spit out a C file that can be either compiled or fed to another verification tool. At the moment supported veification commands are: unroll and induction The syntax is currently CBMC specific, but will be adapted in future to work for any SV comp tool
| @@ -261,45 +263,54 @@ case class IntUnaryMinusOp() extends IntArgOperator { | |||
| // These operators take bitvector operands and return bitvector results. | |||
| sealed abstract class BVArgOperator(val w : Int) extends Operator { | |||
| override def fixity = Operator.INFIX | |||
| def signed_operands = false | |||
There was a problem hiding this comment.
When is this actually used? And why is it plural?
There was a problem hiding this comment.
ah yeah, I put that there because eventually I'm going to have to deal with bitvector comparisons being either signed or unsigned. So, if the comparison is signed, the operands need to be made signed, and if the comparison is unsigned, the operands need to be made unsigned. But currently it doesn't do that and I was hoping to come up with a better way of dealing with the signed/unsigned-ness of operators but haven't yet.
There was a problem hiding this comment.
If you want to avoid clutter in the Operator class, you can have a helper function that just does a match on the operators to say if they are signed
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.
Work in progress but please provide feedback!
Using the command dump_c, uclid will spit out a C file that can
be either compiled or fed to another verification tool.
At the moment supported verification commands are: unroll and induction
The syntax is currently CBMC specific, but will be adapted in future to work
for any SV comp tool.
The aim is that we can: