Skip to content

Commit

Permalink
Python bindings: Add proclaim_f, a cry_f version of proclaim
Browse files Browse the repository at this point in the history
Addresses the request in
#1676 (comment)
  • Loading branch information
RyanGlScott committed Sep 14, 2023
1 parent da7ad0d commit a6b7892
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 0 deletions.
3 changes: 3 additions & 0 deletions saw-remote-api/python/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,9 @@
function with LLVM or JVM verification will raise an error.
* The `proclaim` function (which is the Python counterpart to to
`{llvm,jvm,mir}_assert` in SAWScript) is no longer deprecated.
* Add a `proclaim_f` function. This behaves like the `proclaim` function, except
that it takes a `cry_f`-style format string as an argument. That is,
`proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`.

## 1.0.1 -- YYYY-MM-DD

Expand Down
6 changes: 6 additions & 0 deletions saw-remote-api/python/saw_client/crucible.py
Original file line number Diff line number Diff line change
Expand Up @@ -536,6 +536,12 @@ def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSO
else:
raise Exception("wrong state")

def proclaim_f(self, s : str) -> None:
"""Proclaims an assertion using a ``cry_f``-style format string, i.e.
``proclaim_f(...)`` is equivalent to ``proclaim(cry_f(...))``"""
expression = to_cryptol_str_customf(s, frames=1, filename="<proclaim_f>")
return self.proclaim(expression)

def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None:
"""Establishes ``proposition`` as a precondition for the function ```Contract```
being specified.
Expand Down

0 comments on commit a6b7892

Please sign in to comment.