Skip to content

Commit

Permalink
Add the jvm_setup_with_tag primitive, similar to the LLVM one
Browse files Browse the repository at this point in the history
with a similar name.
  • Loading branch information
robdockins committed Jun 2, 2022
1 parent 67fe177 commit 84b00b7
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 0 deletions.
8 changes: 8 additions & 0 deletions src/SAWScript/Crucible/JVM/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ module SAWScript.Crucible.JVM.Builtins
, jvm_fresh_var
, jvm_alloc_object
, jvm_alloc_array
, jvm_setup_with_tag
) where

import Control.Lens
Expand Down Expand Up @@ -1413,6 +1414,13 @@ jvm_return retVal =
X.throwM (JVMReturnTypeMismatch retTy valTy)
Setup.crucible_return retVal

jvm_setup_with_tag ::
String ->
JVMSetupM () ->
JVMSetupM ()
jvm_setup_with_tag tag m =
JVMSetupM (Setup.setupWithTag tag (runJVMSetupM m))

--------------------------------------------------------------------------------

-- | Sort a list of things and group them into equivalence classes.
Expand Down
8 changes: 8 additions & 0 deletions src/SAWScript/Interpreter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3279,6 +3279,14 @@ primitives = Map.fromList
, "jvm_return statement is required if and only if the method"
, "has a non-void return type." ]

, prim "jvm_setup_with_tag" "String -> JVMSetup () -> JVMSetup ()"
(pureVal jvm_setup_with_tag)
Experimental
[ "All conditions (e.g., from points-to or assert statements) executed"
, "in the scope of the given setup block will have the provieded string"
, "attached as a tag that can later be filtered by proof tactics."
]

, prim "jvm_verify"
"JavaClass -> String -> [JVMSpec] -> Bool -> JVMSetup () -> ProofScript () -> TopLevel JVMSpec"
(pureVal jvm_verify)
Expand Down

0 comments on commit 84b00b7

Please sign in to comment.