VeriFast Help > Glossary

Term

Path condition

Definition

A list of first-order formulas describing assumptions which hold on the path currently being verified.

Shown in the Assumptions pane in the bottom center of the VeriFast window.

Notes

• To show the path condition at a given symbolic execution step, select the step in the Steps pane.
• Producing a pure assertion adds a formula to the path condition.
• Consuming a pure assertion causes VeriFast to check that the assertion follows from the path condition.
• When verifying conditional statements, expressions and assertions, VeriFast adds the condition to the path condition when verifying the then branch and its negation when verifying the else branch.
• VeriFast stops investigating a path when the path condition becomes inconsistent.
• The path condition, the symbolic store, and the symbolic heap together constitute the symbolic state of the symbolic execution.