goal

The goal statement specifies a section that describes a goal for Cyclone to solve.

Syntax

The syntax of a goal statement is as follows:

goal { [<expression>] <check/enumerate> [<condition>] [<reach>] }

The goal section contains three parts: expressions that describe a list of path conditions, a check statement that issues a command to Cyclone (along with path condition) and a reach statement that specifies the set of reachable nodes. The goal section must have exactly either one check or enumeration statement.

Here is an example:

 goal {

          let pc = S1->S2 ^ S1->S3;

          check for  5 condition(pc) reach (S0,S2)

Scope

The goal section is a part of Cyclone specification. Every valid Cyclone specification can have at most one goal section . A specification without a goal section is still a valid specification.

Semantics

The goal section is the most fundamental building block for a Cyclone specification. All different kinds of path conditions are generated from this block by the compiler

< Back