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

Expand help text for llvm_compositional_extract to cover arguments #1840

Merged
merged 3 commits into from
Mar 15, 2023
Merged

Expand help text for llvm_compositional_extract to cover arguments #1840

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6331e55
Expand help text for `llvm_compositional_extract` to cover arguments
Mar 12, 2023
cda0117
Name arguments and clarify that 7th argument is a proof *strategy*
Mar 14, 2023
15a297d
Merge branch 'master' into bb/ce-help
bboston7 Mar 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion src/SAWScript/Interpreter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2744,7 +2744,20 @@ primitives = Map.fromList
, "`llvm_points_to`). The Term is the tuple consisting of the"
, "output parameters of the LLVM function: the return parameter, then"
, "the parameters passed by reference (in the order given by"
, "`llvm_points_to`). For more flexibility, see `llvm_verify`."
, "`llvm_points_to`)."
, ""
, "In order, the arguments to `llvm_compositional_extract` are:"
bboston7 marked this conversation as resolved.
Show resolved Hide resolved
, " 1. The LLVM module containing the function to extract."
, " 2. The name of the function to extract."
, " 3. The name of the `Term` to generate."
, " 4. A list of overrides to use in the memory safety proof in the 7th"
, " argument."
bboston7 marked this conversation as resolved.
Show resolved Hide resolved
, " 5. Whether to perform path satisfiability checks."
, " 6. Memory layout specification for the extracted function."
bboston7 marked this conversation as resolved.
Show resolved Hide resolved
, " 7. Proof that the extracted function satisfies the memory"
, " specification in the 6th argument."
bboston7 marked this conversation as resolved.
Show resolved Hide resolved
, ""
, "For more flexibility, see `llvm_verify`."
]
, prim "crucible_llvm_compositional_extract"
"LLVMModule -> String -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec"
Expand Down