From 86f1f2ee4dd7de05886609b82f9daf41e4cbcc58 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 11 Sep 2024 14:38:07 -0700 Subject: [PATCH] Revise Haddocks for Crucible backends (#1249) The fact that these backends use an `AssumptionStack` is an implementation detail that is not exposed via their interface, instead clients interact with `getProofObligations`. Also, point to a module that helps with dispatching such obligations. --- crucible/src/Lang/Crucible/Backend.hs | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 75b346284..83c9f3411 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -16,13 +16,11 @@ offline solver connection, while the 'Lang.Crucible.Backend.Online.OnlineBackend' is designed to be used with an online solver. -The 'AS.AssumptionStack' tracks the assumptions that are in scope for each -assertion, accounting for the branching and merging structure of programs. The -symbolic simulator manages the 'AS.AssumptionStack'. After symbolic simulation -completes, the caller should traverse the 'AS.AssumptionStack' (or use -combinators like 'AS.proofGoalsToList') to discharge the resulting proof -obligations with a solver backend. - +The backend tracks the assumptions that are in scope for each assertion, +accounting for the branching and merging structure of programs. After +symbolic simulation completes, the caller should traverse the collected +'ProofObligations' (via 'getProofObligations') to discharge the resulting proof +obligations with a solver backend. See also "Lang.Crucible.Backend.Prove". -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}