{"abstract":"Return alias summary chooses one of multiple parameter origins.","category":"Borrow checking","checks":21,"contract":"Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.","evaluation_group":"s3-borrow-checking-borrow-call-summaries","failed_approach":"The partial repair uses if not d['return_origins'] and bool(d['body_return_origins']): errors.append('return-origin-summary'), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-borrow-call-summaries-return-origin-summary","id":"FA-43466","implementations":{"attempt":{"sha256":"f258ee8df26a33301d7331bf7b2c06284028ce95e485dde605fd61c789dd0f96","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')\n    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')\n    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')\n    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')\n    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')\n    if not d['return_origins'] and bool(d['body_return_origins']): errors.append('return-origin-summary')\n    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')\n    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')\n    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')\n    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}\ncheck('well formed empty obligations',solve(base),[])\ncheck('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])\ncheck('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])\ncheck('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])\ncheck('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])\ncheck('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])\ncheck('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])\ncheck('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])\ncheck('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])\ncheck('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])\ncheck('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])\ncheck('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])\ncheck('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])\ncheck('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])\ncheck('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])\ncheck('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])\ncheck('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])\ncheck('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])\ncheck('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])\ncheck('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])\ncheck('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-release'])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"a61ac9291a6b4a2836791aa7cb0d3cdab003aa97a6bc69a05a61f8d0f8f9aa6e","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')\n    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')\n    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')\n    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')\n    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')\n    if False: errors.append('return-origin-summary')\n    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')\n    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')\n    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')\n    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}\ncheck('well formed empty obligations',solve(base),[])\ncheck('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])\ncheck('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])\ncheck('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])\ncheck('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])\ncheck('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])\ncheck('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])\ncheck('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])\ncheck('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])\ncheck('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])\ncheck('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])\ncheck('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])\ncheck('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])\ncheck('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])\ncheck('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])\ncheck('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])\ncheck('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])\ncheck('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])\ncheck('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])\ncheck('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])\ncheck('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-release'])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"da0cc2f158e5b10bef05994fa32e96fbab0e8ac8bd5fcc5a8a1db0dda9816a87","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')\n    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')\n    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')\n    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')\n    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')\n    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')\n    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')\n    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')\n    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')\n    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}\ncheck('well formed empty obligations',solve(base),[])\ncheck('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])\ncheck('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])\ncheck('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])\ncheck('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])\ncheck('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])\ncheck('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])\ncheck('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])\ncheck('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])\ncheck('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])\ncheck('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])\ncheck('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])\ncheck('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])\ncheck('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])\ncheck('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])\ncheck('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])\ncheck('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])\ncheck('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])\ncheck('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])\ncheck('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])\ncheck('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-release'])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"s3-borrow-checking-borrow-call-summaries-return-origin-summary","generated_at":"2026-09-29T14:44:02.268544+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.","repair":"Apply the specified transfer or inference rule at this site: if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary').","root_cause":"The static analyzer mishandles return origin summary: return alias summary chooses one of multiple parameter origins.","sha256":"e992298df69d1bb482cd9d19949203c8fe5c60454377748e2743db17f9b6724a","title":"Return alias summary chooses one of multiple parameter origins · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":51.485,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["read-summary"],"check":"read-summary regression 0","expected":["read-summary"],"passed":true},{"actual":["read-summary"],"check":"read-summary regression 1","expected":["read-summary"],"passed":true},{"actual":["write-summary"],"check":"write-summary regression 0","expected":["write-summary"],"passed":true},{"actual":["write-summary"],"check":"write-summary regression 1","expected":["write-summary"],"passed":true},{"actual":["move-summary"],"check":"move-summary regression 0","expected":["move-summary"],"passed":true},{"actual":["move-summary"],"check":"move-summary regression 1","expected":["move-summary"],"passed":true},{"actual":["escape-summary"],"check":"escape-summary regression 0","expected":["escape-summary"],"passed":true},{"actual":["escape-summary"],"check":"escape-summary regression 1","expected":["escape-summary"],"passed":true},{"actual":["unique-actual"],"check":"unique-actual regression 0","expected":["unique-actual"],"passed":true},{"actual":["unique-actual"],"check":"unique-actual regression 1","expected":["unique-actual"],"passed":true},{"actual":[],"check":"return-origin-summary regression 0","expected":["return-origin-summary"],"passed":false},{"actual":[],"check":"return-origin-summary regression 1","expected":["return-origin-summary"],"passed":false},{"actual":["unknown-retention"],"check":"unknown-retention regression 0","expected":["unknown-retention"],"passed":true},{"actual":["unknown-retention"],"check":"unknown-retention regression 1","expected":["unknown-retention"],"passed":true},{"actual":["noescape-proof"],"check":"noescape-proof regression 0","expected":["noescape-proof"],"passed":true},{"actual":["noescape-proof"],"check":"noescape-proof regression 1","expected":["noescape-proof"],"passed":true},{"actual":["formal-map-bijection"],"check":"formal-map-bijection regression 0","expected":["formal-map-bijection"],"passed":true},{"actual":["formal-map-bijection"],"check":"formal-map-bijection regression 1","expected":["formal-map-bijection"],"passed":true},{"actual":["unwind-release"],"check":"unwind-release regression 0","expected":["unwind-release"],"passed":true},{"actual":["unwind-release"],"check":"unwind-release regression 1","expected":["unwind-release"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"read-summary regression 0\", \"actual\": [\"read-summary\"], \"expected\": [\"read-summary\"], \"passed\": true}, {\"check\": \"read-summary regression 1\", \"actual\": [\"read-summary\"], \"expected\": [\"read-summary\"], \"passed\": true}, {\"check\": \"write-summary regression 0\", \"actual\": [\"write-summary\"], \"expected\": [\"write-summary\"], \"passed\": true}, {\"check\": \"write-summary regression 1\", \"actual\": [\"write-summary\"], \"expected\": [\"write-summary\"], \"passed\": true}, {\"check\": \"move-summary regression 0\", \"actual\": [\"move-summary\"], \"expected\": [\"move-summary\"], \"passed\": true}, {\"check\": \"move-summary regression 1\", \"actual\": [\"move-summary\"], \"expected\": [\"move-summary\"], \"passed\": true}, {\"check\": \"escape-summary regression 0\", \"actual\": [\"escape-summary\"], \"expected\": [\"escape-summary\"], \"passed\": true}, {\"check\": \"escape-summary regression 1\", \"actual\": [\"escape-summary\"], \"expected\": [\"escape-summary\"], \"passed\": true}, {\"check\": \"unique-actual regression 0\", \"actual\": [\"unique-actual\"], \"expected\": [\"unique-actual\"], \"passed\": true}, {\"check\": \"unique-actual regression 1\", \"actual\": [\"unique-actual\"], \"expected\": [\"unique-actual\"], \"passed\": true}, {\"check\": \"return-origin-summary regression 0\", \"actual\": [], \"expected\": [\"return-origin-summary\"], \"passed\": false}, {\"check\": \"return-origin-summary regression 1\", \"actual\": [], \"expected\": [\"return-origin-summary\"], \"passed\": false}, {\"check\": \"unknown-retention regression 0\", \"actual\": [\"unknown-retention\"], \"expected\": [\"unknown-retention\"], \"passed\": true}, {\"check\": \"unknown-retention regression 1\", \"actual\": [\"unknown-retention\"], \"expected\": [\"unknown-retention\"], \"passed\": true}, {\"check\": \"noescape-proof regression 0\", \"actual\": [\"noescape-proof\"], \"expected\": [\"noescape-proof\"], \"passed\": true}, {\"check\": \"noescape-proof regression 1\", \"actual\": [\"noescape-proof\"], \"expected\": [\"noescape-proof\"], \"passed\": true}, {\"check\": \"formal-map-bijection regression 0\", \"actual\": [\"formal-map-bijection\"], \"expected\": [\"formal-map-bijection\"], \"passed\": true}, {\"check\": \"formal-map-bijection regression 1\", \"actual\": [\"formal-map-bijection\"], \"expected\": [\"formal-map-bijection\"], \"passed\": true}, {\"check\": \"unwind-release regression 0\", \"actual\": [\"unwind-release\"], \"expected\": [\"unwind-release\"], \"passed\": true}, {\"check\": \"unwind-release regression 1\", \"actual\": [\"unwind-release\"], \"expected\": [\"unwind-release\"], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":50.527,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["read-summary"],"check":"read-summary regression 0","expected":["read-summary"],"passed":true},{"actual":["read-summary"],"check":"read-summary regression 1","expected":["read-summary"],"passed":true},{"actual":["write-summary"],"check":"write-summary regression 0","expected":["write-summary"],"passed":true},{"actual":["write-summary"],"check":"write-summary regression 1","expected":["write-summary"],"passed":true},{"actual":["move-summary"],"check":"move-summary regression 0","expected":["move-summary"],"passed":true},{"actual":["move-summary"],"check":"move-summary regression 1","expected":["move-summary"],"passed":true},{"actual":["escape-summary"],"check":"escape-summary regression 0","expected":["escape-summary"],"passed":true},{"actual":["escape-summary"],"check":"escape-summary regression 1","expected":["escape-summary"],"passed":true},{"actual":["unique-actual"],"check":"unique-actual regression 0","expected":["unique-actual"],"passed":true},{"actual":["unique-actual"],"check":"unique-actual regression 1","expected":["unique-actual"],"passed":true},{"actual":[],"check":"return-origin-summary regression 0","expected":["return-origin-summary"],"passed":false},{"actual":[],"check":"return-origin-summary regression 1","expected":["return-origin-summary"],"passed":false},{"actual":["unknown-retention"],"check":"unknown-retention regression 0","expected":["unknown-retention"],"passed":true},{"actual":["unknown-retention"],"check":"unknown-retention regression 1","expected":["unknown-retention"],"passed":true},{"actual":["noescape-proof"],"check":"noescape-proof regression 0","expected":["noescape-proof"],"passed":true},{"actual":["noescape-proof"],"check":"noescape-proof regression 1","expected":["noescape-proof"],"passed":true},{"actual":["formal-map-bijection"],"check":"formal-map-bijection regression 0","expected":["formal-map-bijection"],"passed":true},{"actual":["formal-map-bijection"],"check":"formal-map-bijection regression 1","expected":["formal-map-bijection"],"passed":true},{"actual":["unwind-release"],"check":"unwind-release regression 0","expected":["unwind-release"],"passed":true},{"actual":["unwind-release"],"check":"unwind-release regression 1","expected":["unwind-release"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"read-summary regression 0\", \"actual\": [\"read-summary\"], \"expected\": [\"read-summary\"], \"passed\": true}, {\"check\": \"read-summary regression 1\", \"actual\": [\"read-summary\"], \"expected\": [\"read-summary\"], \"passed\": true}, {\"check\": \"write-summary regression 0\", \"actual\": [\"write-summary\"], \"expected\": [\"write-summary\"], \"passed\": true}, {\"check\": \"write-summary regression 1\", \"actual\": [\"write-summary\"], \"expected\": [\"write-summary\"], \"passed\": true}, {\"check\": \"move-summary regression 0\", \"actual\": [\"move-summary\"], \"expected\": [\"move-summary\"], \"passed\": true}, {\"check\": \"move-summary regression 1\", \"actual\": [\"move-summary\"], \"expected\": [\"move-summary\"], \"passed\": true}, {\"check\": \"escape-summary regression 0\", \"actual\": [\"escape-summary\"], \"expected\": [\"escape-summary\"], \"passed\": true}, {\"check\": \"escape-summary regression 1\", \"actual\": [\"escape-summary\"], \"expected\": [\"escape-summary\"], \"passed\": true}, {\"check\": \"unique-actual regression 0\", \"actual\": [\"unique-actual\"], \"expected\": [\"unique-actual\"], \"passed\": true}, {\"check\": \"unique-actual regression 1\", \"actual\": [\"unique-actual\"], \"expected\": [\"unique-actual\"], \"passed\": true}, {\"check\": \"return-origin-summary regression 0\", \"actual\": [], \"expected\": [\"return-origin-summary\"], \"passed\": false}, {\"check\": \"return-origin-summary regression 1\", \"actual\": [], \"expected\": [\"return-origin-summary\"], \"passed\": false}, {\"check\": \"unknown-retention regression 0\", \"actual\": [\"unknown-retention\"], \"expected\": [\"unknown-retention\"], \"passed\": true}, {\"check\": \"unknown-retention regression 1\", \"actual\": [\"unknown-retention\"], \"expected\": [\"unknown-retention\"], \"passed\": true}, {\"check\": \"noescape-proof regression 0\", \"actual\": [\"noescape-proof\"], \"expected\": [\"noescape-proof\"], \"passed\": true}, {\"check\": \"noescape-proof regression 1\", \"actual\": [\"noescape-proof\"], \"expected\": [\"noescape-proof\"], \"passed\": true}, {\"check\": \"formal-map-bijection regression 0\", \"actual\": [\"formal-map-bijection\"], \"expected\": [\"formal-map-bijection\"], \"passed\": true}, {\"check\": \"formal-map-bijection regression 1\", \"actual\": [\"formal-map-bijection\"], \"expected\": [\"formal-map-bijection\"], \"passed\": true}, {\"check\": \"unwind-release regression 0\", \"actual\": [\"unwind-release\"], \"expected\": [\"unwind-release\"], \"passed\": true}, {\"check\": \"unwind-release regression 1\", \"actual\": [\"unwind-release\"], \"expected\": [\"unwind-release\"], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":50.363,"exit_code":0,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["read-summary"],"check":"read-summary regression 0","expected":["read-summary"],"passed":true},{"actual":["read-summary"],"check":"read-summary regression 1","expected":["read-summary"],"passed":true},{"actual":["write-summary"],"check":"write-summary regression 0","expected":["write-summary"],"passed":true},{"actual":["write-summary"],"check":"write-summary regression 1","expected":["write-summary"],"passed":true},{"actual":["move-summary"],"check":"move-summary regression 0","expected":["move-summary"],"passed":true},{"actual":["move-summary"],"check":"move-summary regression 1","expected":["move-summary"],"passed":true},{"actual":["escape-summary"],"check":"escape-summary regression 0","expected":["escape-summary"],"passed":true},{"actual":["escape-summary"],"check":"escape-summary regression 1","expected":["escape-summary"],"passed":true},{"actual":["unique-actual"],"check":"unique-actual regression 0","expected":["unique-actual"],"passed":true},{"actual":["unique-actual"],"check":"unique-actual regression 1","expected":["unique-actual"],"passed":true},{"actual":["return-origin-summary"],"check":"return-origin-summary regression 0","expected":["return-origin-summary"],"passed":true},{"actual":["return-origin-summary"],"check":"return-origin-summary regression 1","expected":["return-origin-summary"],"passed":true},{"actual":["unknown-retention"],"check":"unknown-retention regression 0","expected":["unknown-retention"],"passed":true},{"actual":["unknown-retention"],"check":"unknown-retention regression 1","expected":["unknown-retention"],"passed":true},{"actual":["noescape-proof"],"check":"noescape-proof regression 0","expected":["noescape-proof"],"passed":true},{"actual":["noescape-proof"],"check":"noescape-proof regression 1","expected":["noescape-proof"],"passed":true},{"actual":["formal-map-bijection"],"check":"formal-map-bijection regression 0","expected":["formal-map-bijection"],"passed":true},{"actual":["formal-map-bijection"],"check":"formal-map-bijection regression 1","expected":["formal-map-bijection"],"passed":true},{"actual":["unwind-release"],"check":"unwind-release regression 0","expected":["unwind-release"],"passed":true},{"actual":["unwind-release"],"check":"unwind-release regression 1","expected":["unwind-release"],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"read-summary regression 0\", \"actual\": [\"read-summary\"], \"expected\": [\"read-summary\"], \"passed\": true}, {\"check\": \"read-summary regression 1\", \"actual\": [\"read-summary\"], \"expected\": [\"read-summary\"], \"passed\": true}, {\"check\": \"write-summary regression 0\", \"actual\": [\"write-summary\"], \"expected\": [\"write-summary\"], \"passed\": true}, {\"check\": \"write-summary regression 1\", \"actual\": [\"write-summary\"], \"expected\": [\"write-summary\"], \"passed\": true}, {\"check\": \"move-summary regression 0\", \"actual\": [\"move-summary\"], \"expected\": [\"move-summary\"], \"passed\": true}, {\"check\": \"move-summary regression 1\", \"actual\": [\"move-summary\"], \"expected\": [\"move-summary\"], \"passed\": true}, {\"check\": \"escape-summary regression 0\", \"actual\": [\"escape-summary\"], \"expected\": [\"escape-summary\"], \"passed\": true}, {\"check\": \"escape-summary regression 1\", \"actual\": [\"escape-summary\"], \"expected\": [\"escape-summary\"], \"passed\": true}, {\"check\": \"unique-actual regression 0\", \"actual\": [\"unique-actual\"], \"expected\": [\"unique-actual\"], \"passed\": true}, {\"check\": \"unique-actual regression 1\", \"actual\": [\"unique-actual\"], \"expected\": [\"unique-actual\"], \"passed\": true}, {\"check\": \"return-origin-summary regression 0\", \"actual\": [\"return-origin-summary\"], \"expected\": [\"return-origin-summary\"], \"passed\": true}, {\"check\": \"return-origin-summary regression 1\", \"actual\": [\"return-origin-summary\"], \"expected\": [\"return-origin-summary\"], \"passed\": true}, {\"check\": \"unknown-retention regression 0\", \"actual\": [\"unknown-retention\"], \"expected\": [\"unknown-retention\"], \"passed\": true}, {\"check\": \"unknown-retention regression 1\", \"actual\": [\"unknown-retention\"], \"expected\": [\"unknown-retention\"], \"passed\": true}, {\"check\": \"noescape-proof regression 0\", \"actual\": [\"noescape-proof\"], \"expected\": [\"noescape-proof\"], \"passed\": true}, {\"check\": \"noescape-proof regression 1\", \"actual\": [\"noescape-proof\"], \"expected\": [\"noescape-proof\"], \"passed\": true}, {\"check\": \"formal-map-bijection regression 0\", \"actual\": [\"formal-map-bijection\"], \"expected\": [\"formal-map-bijection\"], \"passed\": true}, {\"check\": \"formal-map-bijection regression 1\", \"actual\": [\"formal-map-bijection\"], \"expected\": [\"formal-map-bijection\"], \"passed\": true}, {\"check\": \"unwind-release regression 0\", \"actual\": [\"unwind-release\"], \"expected\": [\"unwind-release\"], \"passed\": true}, {\"check\": \"unwind-release regression 1\", \"actual\": [\"unwind-release\"], \"expected\": [\"unwind-release\"], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}