Difference between revisions of "Cascade User Manual"

From CVC4
Jump to: navigation, search
(Basic Structure)
(Basic Structure)
Line 9: Line 9:
 
== Basic Structure ==
 
== Basic Structure ==
  
Every control file starts with \texttt{sourceFile} sections that specify the files to be analyzed. Each source file has two attributes: \texttt{name} contains the path to the file, and \texttt{fileId} attaches a unique id to it. After \texttt{sourceFile}, one or more \texttt{run} sections are specified, which describe the runs to be checked. Each run starts with a single \texttt{startPosition} and \texttt{endPosition} to give the start point and the end point respectively, and in between, one or more \texttt{wayPoint} may be inserted optionally to indicate the positions should be passed through.
+
Every control file starts with "sourceFile" sections that specify the files to be analyzed. Each source file has two attributes: "name" contains the path to the file, and "fileId" attaches a unique id to it. After "sourceFile", one or more "run" sections are specified, which describe the runs to be checked. Each run starts with a single "startPosition" and "endPosition" to give the start point and the end point respectively, and in between, one or more "wayPoint"s may be inserted optionally to indicate the positions should be passed through.

Revision as of 11:18, 12 December 2012

Getting Cascade

Using Cascade

Control File

Instead of inserting annotations in the source code, Cascade keeps them in a control file in order to leaves the source code clean. The control file is in the simple XML format, which serves as the guidance of verification. In this section, we will introduce the elements included control files by showing how to verify some sample codes in Cascade.

Basic Structure

Every control file starts with "sourceFile" sections that specify the files to be analyzed. Each source file has two attributes: "name" contains the path to the file, and "fileId" attaches a unique id to it. After "sourceFile", one or more "run" sections are specified, which describe the runs to be checked. Each run starts with a single "startPosition" and "endPosition" to give the start point and the end point respectively, and in between, one or more "wayPoint"s may be inserted optionally to indicate the positions should be passed through.