-
Notifications
You must be signed in to change notification settings - Fork 161
Open
runtimeverification/pyk
#770Labels
Description
Related: runtimeverification/pyk#693 (comment)
Here, in order to group calls to multiple clients that correspond to the same proof, along with bug_report, an additional optional argument bug_report_id is passed. If the argument is missing, a default value is calculated from the object id.
This means the class that produces bug report content is responsible for defining where to write data within the tar file. A more flexible design would be to let the caller define bug report structure by abstracting the target directory for the producer using a handle:
# BugReport defines which file to write
bug_report = BugReport('bug-report')
# BugReporter is a handle for writing in a certain directory within the file
bug_reporter = bug_report.reporter('AssertTest.test_assert_true')
# The handle is passed to the class that produces bug report content
client = JsonRpcClient(..., bug_reporter=bug_reporter)Then the producer is no longer concerned about where to write things:
class JsonRpcClient(...):
def request(self, ...):
# The producer can use the handle to create artifacts
self.bug_reporter.add_command(...)The private interface between BugReport and BugReporter should implement locking to prevent race conditions.