Verification Condition Generation

In the previous section, we added contracts, loop invariants, and inline assertions to the program. We now examine how the symbolic execution engine uses these assertions. The engine mechanically reduces the claim that the program satisfies its specification to a finite set of separation-logic entailments of the form p |-- qp |-- q, called verification conditions (VCs). Once every VC is proved, the function satisfies its contract. This section reviews the classic weakest-precondition calculus and three aspects that make it less intuitive for C* users, then introduces C*‘s forward symbolic execution through three worked examples. Later sections explain how to prove these VCs.

Recall the Hoare triple from Specifying with Separation Logic. Once contracts and invariants are written, we need a mechanical way to compute the logical proposition to be proved from the annotated program. A classic method is Dijkstra’s weakest-precondition (WP) calculus: is the weakest precondition needed to ensure that holds after executing statement . It is defined recursively over the program structure:

For a loop, use its annotated invariant : take , and generate two additional obligations: preservation and exit . Checking the whole function then reduces to a single entailment:

This is the classic verification-condition generator (VCGen) used by many deductive-verification tools.

For example, the following program computes (with ), with the target postcondition :

Annotate the loop with the invariant and expand wp using the rules above. The loop rule gives and the two obligations. Two applications of the assignment rule then replace and in by and , respectively, reducing verification of the whole function to one formula:

The entry and preservation obligations both hold, but the exit obligation cannot be proved: says that the loop has stopped, but does not imply . If were negative, would not entail . During execution, never becomes negative (, and each iteration decrements it by one), but the invariant does not record this fact, so the WP calculus cannot use it. Strengthening the invariant to makes all three obligations hold. This illustrates why the previous section required boundary facts to be included in the invariant.

Applying the WP calculus directly in a tool like C* raises three difficulties for users writing and verifying programs.

First, its direction is opposite to the program. processes before : it starts from ensureensure and substitutes backward through the statements, whereas people write, read, and debug programs from top to bottom. In the example above, the unprovable exit obligation becomes apparent only after the entire formula has been computed. When verification fails, it is therefore generally hard to identify the relevant program line.

Second, one function yields one big VC. WP combines the whole function body into a single formula. Even the five-line program produces a sizable VC; a C function with pointers, structs, and branches must also encode each statement’s memory effects, so the formula can grow quickly. If this large VC cannot be proved, or the automated solver times out, the user has little information to help locate the problem.

Third, separation logic needs the magic wand. Defining WP in separation logic requires a new connective for statements that read and write the heap. For example, the write statement from Specifying with Separation Logic has the weakest precondition:

This says that the cell at can be separated from the current heap, making the write safe. After its contents are changed to and the cell is combined with the remaining heap, holds. Here, is the magic wand from the notation table two sections earlier: means that adding a heap satisfying yields a heap satisfying . The magic wand allows WP to be computed structurally in separation logic, but automatically solving entailments that contain it remains difficult.

These three difficulties motivate a change from computing backward from the postcondition to advancing assertions forward in execution order. With the forward approach, each line has a current state, and proof obligations are generated at the relevant source lines. This is the process shown when you view symbolic states line by line in VSCode.

The symbolic execution engine currently enabled by default in C* is provided by QCP (Qualified C Programming). QCP works in the opposite direction from WP: starting from requirerequire, it computes the strongest postcondition statement by statement in execution order, generating multiple small VCs along the way. QCP’s forward style originates from VST-Floyd, where each proof step advances a current assertion. The proof goal consists of the current assertion and the remaining program, so the proof outline develops from top to bottom. QCP adapts this method from interactive proof to automated verification, using code annotations to guide execution. One motivation for the forward approach is real-time feedback: each line can be symbolically executed as you write it, showing the resulting state and allowing incremental verification of an unfinished function.

The engine represents the symbolic state as a separation-logic assertion, which you can view line by line in VSCode. It consists of logical variables bound by existsexists, pure facts expressed with factfact, and a spatial part built from data_atdata_at and representation predicates. Execution starts from requirerequire, with parameters represented by names such as __pre__pre. Each kind of statement advances the state by a fixed rule:

• Declaration and assignment: update the contents of the target variable’s data_atdata_at, looking up the current value of each variable in the expression from the state;
• Memory read (*p*p, v->tailv->tail): find the data_atdata_at for the required cell in the spatial part and read its value. If no such cell is found, the engine reports an error and halts: it does not unfold representation predicates on its own, as Examples 2 and 3 will show;
• Memory write: find the required cell, then replace its contents;
• Branch: split the state into two, conjoin one with the condition and the other with its negation, then advance each separately;
• Loop: use the invariant as a cut point. At the loop head, generate a VC (current state |--|-- invariant), then enter the loop body with only the invariant, conjoined with the loop condition. When execution returns from the end of the body to the loop head, generate another VC to check preservation of the invariant. After the loop, continue with the invariant **** the negation of the condition;
• Inline assertion: generate a VC (current state |--|-- assertion), then use the assertion as the new state, as described in the previous section;
• Function call: match and remove the resources specified by the callee’s requirerequire from the current state, item by item, and replace them with the resources specified by ensureensure. The rest of the state remains unchanged, following the frame rule; pure facts left unresolved by matching become VCs;
• Function exit: generate a VC of the form current state |--|-- ensureensure, removing local resources from the state and substituting the return value for __return__return.

Each of these VCs has the form p |-- qp |-- q: the left side is the symbolic state computed by the engine, and the right side is the assertion you wrote (an invariant, an inline assertion, a callee’s requirerequire, or this function’s ensureensure). Each VC records the source line that generated it. The engine also generates safety VCs at operations that could cause C undefined behavior, such as arithmetic overflow, division by zero, and out-of-range shifts. These are pure-fact obligations, as Example 1 will illustrate.

Forward symbolic execution addresses the three difficulties described above:

• Forward: the state advances in execution order, with a viewable symbolic state at each line. This supports the VSCode panel’s real-time feedback as you write code;
• Small and numerous: VCs are generated at annotations and record their source lines, so an unproved VC directs you to the relevant line;
• No magic wand needed: memory reads and writes use the data_atdata_at already in the state, and calls use item-by-item frame matching. Neither requires the magic wand.

Not every entailment appears in the VC list. QCP’s built-in entailment solver combines rule-based matching with lightweight arithmetic reasoning. It matches heap resources item by item and discharges trivial pure facts immediately; entailments solved this way do not appear in the list. The VCs you see are the obligations left unresolved by automation. Often the spatial parts already match, leaving pure facts that need a manual proof or a predicate that needs to be unfolded by its definition.

Consider the Gauss summation program from the previous section:

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

Verifying this file yields two VCs (the output is wrapped to page width, and line numbers refer to the listing above):

These VCs show which obligations the engine resolves and which remain to be proved:

• Loop-entry establishment is absent: the obligation to establish the invariant does not appear in the list. Before the loop, the state records ss and ii as two cells whose contents are 0i0i. Matching the invariant item by item leaves only trivial arithmetic such as , which the engine discharges automatically.
• The overflow checks are absent too: the results of i = i + 1i = i + 1 and s = s + is = s + i must both lie within the intint range. The engine checks a safety condition at each line and discharges both using the invariant: iv < n__pre <= 1000iv < n__pre <= 1000 bounds iv + 1iiv + 1i, while 2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i) and the bounds on iviv bound sv + iv + 1isv + iv + 1i. As the previous section explained, omitting fact(n__pre <= 1000i)fact(n__pre <= 1000i) from the invariant would leave both checks without the required bound, so both would appear as VCs.
• VC 1 checks preservation: the antecedent is the state after the loop body, with the contents of ss and ii updated; the consequent is the full invariant, including its existsexists quantifiers. The proof must choose new instances for iviv and svsv and verify each factfact.
• VC 2 checks the function exit: the left side of |--|-- is the invariant **** the negation of the loop condition. All data_atdata_at assertions have been removed, leaving only empemp in the spatial part: on return, the engine reclaims local-variable cells and retains the pure facts. The right side is ensureensure, with __return__return replaced by svsv. The remaining arithmetic step is to use , , and to derive .

This example illustrates a common form of VC: the engine has already matched and discharged the spatial part, leaving mostly pure arithmetic facts for a manual proof.

In the array and linked-list examples from the previous section, the invariant’s resources are folded into wrapper predicates. Symbolic execution fails if it tries to access those resources directly. We now examine the error. Remove the inline assertion from the clearclear loop body in the previous section and verify again. The engine halts at *p = 0*p = 0:

This is an error, not a VC: writing to *p*p requires the cell undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar to be directly available in the state, but it is folded into undef_suffixundef_suffix. The engine does not decide when to unfold a predicate, so symbolic execution cannot continue. The symbolic state reported with the error helps locate the problem: it shows which predicate contains the missing resource.

Restoring the inline assertion that unfolds one step lets symbolic execution complete for the whole function and produces four VCs:

Unlike Example 1, the loop-entry establishment obligation also remains as a VC. Rewriting undef_bytes arr__pre n__preundef_bytes arr__pre n__pre as an empty prefix **** a suffix covering the whole segment (zero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__prezero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__pre) requires unfolding all three predicates, which the automated strategy cannot do. Consider the assertion obligation, VC 2. As the previous section explained, assertassert allows symbolic execution to continue while leaving its proof obligation to be discharged later. Here is that obligation:

The two sides are almost identical. The right side contains the assertion’s own pure facts: iv <= n__preiv <= n__pre is absent because it is implied by iv < n__preiv < n__pre. The spatial difference is in the last line and a half: undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre on the left must be split into the first cell and the remaining suffix. This step uses the definitions of undef_suffixundef_suffix and undef_array_atundef_array_at; its proof will be given later. The exit obligation, VC 4, is shorter:

The boundary facts imply iv == n__preiv == n__pre. The suffix then has length zero and reduces to the empty heap, while the prefix covers the whole segment. This entailment expresses the exit argument from the previous section.

The linked-list example behaves similarly. If you remove the inline assertion and verify reversereverse, the engine halts when reading v->tailv->tail:

The cell for the tailtail field is folded into sll vv l2sll vv l2. Restoring the previous section’s assertion lets symbolic execution finish, again producing four VCs: establishment, assertion, preservation, and exit. The assertion VC unfolds sllsll using its non-empty branch:

The proof uses two facts. Since vvvv is non-null, sll vv l2sll vv l2 must use the definition’s CONSCONS branch, so l2l2 has the form x :: xsx :: xs. Unfolding that branch exposes the head node’s two data_atdata_at cells and the remaining sll q xssll q xs. The list equality l == l1 ++ l2l == l1 ++ l2 must also be rewritten as l == l1 ++ x :: xsl == l1 ++ x :: xs.

The preservation VC’s antecedent records the state after the three pointer updates: ww contains vvvv, vv contains qq, and the head node’s FtailFtail cell contains wvwv. The proof must refold these resources into the invariant’s two sllsll segments. The exit VC is again short:

This entailment expresses the previous section’s three-line exit argument. From vv == 0ivv == 0i and sll vv l2sll vv l2, the definition’s empty-list branch gives l2 == []l2 == [], hence l1 == ll1 == l. The antecedent’s sll wv (REVERSE l1)sll wv (REVERSE l1) then matches the conclusion.

You can view all the output shown in this section in VSCode using the same command as for symbolic states (right-click and select Show Symbolic StateShow Symbolic State):

• With the cursor on a line inside a function body, the panel shows the symbolic state at that line: the strongest postcondition computed by forward symbolic execution up to that point;
• With the cursor on a file-level line, such as the end of the file, the panel lists the verification conditions accumulated up to that point. Each is labeled with its number and source line (VC n line lVC n line l); expanding it shows the two sides separated by |--|--.

A non-empty VC list means verification is incomplete. To discharge the remaining obligations, write proof code in [[cst::proof]][[cst::proof]] that constructs theorems and rewrites the symbolic state until the engine can discharge every VC. Later sections explain this process.

• A verification condition (VC) is a separation-logic entailment of the form p |-- qp |-- q: the left is the symbolic state computed by the engine, the right is the assertion you wrote; once symbolic execution completes successfully, proving all generated VCs establishes that the program satisfies its specification.
• The classic WP calculus has three counterintuitive aspects: it substitutes backward from ensureensure, combines the whole function into one large formula, and requires the magic wand when used in separation logic.
• C*‘s default symbolic execution engine is provided by QCP and draws on VST-Floyd. Starting from requirerequire, it computes the strongest postcondition in execution order and generates VCs at loop heads (establishment/preservation), inline assertions, function calls, and function exits. It also generates safety VCs for overflow, division by zero, and similar operations. Each VC records its source line.
• Resources needed for memory reads and writes must be directly available in the state. A missing resource causes an error, not a VC; you specify when to unfold a predicate through an assertion or proof.
• Entailments discharged automatically do not appear in the VC list. The remaining obligations commonly have matching spatial parts with unresolved pure facts, or require a predicate to be unfolded by one step.