Python bindings: Add proclaim_f, a cry_f version of proclaim

Addresses the request in
#1676 (comment)

saw-remote-api/python/CHANGELOG.md

@@ -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
 

saw-remote-api/python/saw_client/crucible.py

@@ -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.

saw-remote-api/python/tests/saw/test_llvm_proclaim.py

@@ -18,15 +18,32 @@ def specification(self):
         self.returns(r)
 
 
+# Like FContract1, but using `proclaim_f` instead of `proclaim`.
+class FContract2(Contract):
+    def specification(self):
+        x = self.fresh_var(i32, 'x')
+        self.proclaim_f('{x} < 0x7fffffff')
+
+        self.execute_func(x)
+
+        r = self.fresh_var(i32, 'r')
+        self.proclaim_f('{r} == {x} + 1')
+        self.proclaim_f('{r} <= 0x7fffffff')
+        self.returns(r)
+
+
 class LLVMProclaimTest(unittest.TestCase):
     def test_llvm_proclaim(self):
         connect(reset_server=True)
         if __name__ == "__main__": view(LogResults())
         bcname = str(Path('tests','saw','test-files', 'llvm_proclaim.bc'))
         mod = llvm_load_module(bcname)
 
-        result = llvm_verify(mod, 'f', FContract1())
-        self.assertIs(result.is_success(), True)
+        result1 = llvm_verify(mod, 'f', FContract1())
+        self.assertIs(result1.is_success(), True)
+
+        result2 = llvm_verify(mod, 'f', FContract2())
+        self.assertIs(result2.is_success(), True)
 
 
 if __name__ == "__main__":