Difference between revisions of "Cascade User Manual"
(→Assertion) |
(→Basic Structure) |
||
| Line 12: | Line 12: | ||
Let's discuss it more with a simple example [[abs.c]]. This program returns the absolute value of parameter x. | Let's discuss it more with a simple example [[abs.c]]. This program returns the absolute value of parameter x. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
[[abs1.ctrl]] is the control file for it, in which the ''sourceFile'' indicates the path to abs.c and assigns an id 1 for it. For the execution path to check, we simply use the start and end line number of [[abs.c]] as ''startPosition'' and ''endPosition''. Since there's an if-else branchs, we use a ''wayPoint'' to select one to check. Normally, a ''wayPoint'' is often the first line of the chosen code. Note that the ''fileId'' is all assigned to 1 in the ''startPosition'', ''endPosition'' and ''wayPoint'', which means these positions are all in [[abs.c]] (whose id is 1). | [[abs1.ctrl]] is the control file for it, in which the ''sourceFile'' indicates the path to abs.c and assigns an id 1 for it. For the execution path to check, we simply use the start and end line number of [[abs.c]] as ''startPosition'' and ''endPosition''. Since there's an if-else branchs, we use a ''wayPoint'' to select one to check. Normally, a ''wayPoint'' is often the first line of the chosen code. Note that the ''fileId'' is all assigned to 1 in the ''startPosition'', ''endPosition'' and ''wayPoint'', which means these positions are all in [[abs.c]] (whose id is 1). | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
As mentioned above, multiple paths can be specified in one control file. In [[abs2.ctrl]], two possible alternative runs of [[abs.c]] are considered together. | As mentioned above, multiple paths can be specified in one control file. In [[abs2.ctrl]], two possible alternative runs of [[abs.c]] are considered together. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
== Cascade Command == | == Cascade Command == | ||
Revision as of 12:08, 12 December 2012
Contents
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 wayPoints may be inserted optionally to indicate the positions should be passed through.
Let's discuss it more with a simple example abs.c. This program returns the absolute value of parameter x.
abs1.ctrl is the control file for it, in which the sourceFile indicates the path to abs.c and assigns an id 1 for it. For the execution path to check, we simply use the start and end line number of abs.c as startPosition and endPosition. Since there's an if-else branchs, we use a wayPoint to select one to check. Normally, a wayPoint is often the first line of the chosen code. Note that the fileId is all assigned to 1 in the startPosition, endPosition and wayPoint, which means these positions are all in abs.c (whose id is 1).
As mentioned above, multiple paths can be specified in one control file. In abs2.ctrl, two possible alternative runs of abs.c are considered together.
Cascade Command
Each position (start point, end point and way point) can further include a command, which include: (1) 'cascade_assume, which takes a source code expression and adds it as an assumption; (2) cascade_check, which takes a source code expression and checks whether it is valid at the given position.
Assertion
Let's go futher of the example of abs.c. One property should be hold in it is result 
0. In abs3.ctrl, such expression is an argument of command cascade_check. Cascade can prove its validity in both runs, which means it is indeed guaranteed to hold in both branches.
<controlFile>
<sourceFile name="abs.c" id="1" />
<run>
<startPosition fileId="1" line="1" />
<wayPoint fileId="1" line="4" />
<endPosition fileId="1" line="8" >
<command>
<cascadeFunction> cascade_check </cascadeFunction>
<argument><![CDATA[
result >= 0
]]>
</argument>
</command>
</endPosition>
</run>
<run>
<startPosition fileId="1" line="1" />
<wayPoint fileId="1" line="6" />
<endPosition fileId="1" line="8" >
<command>
<cascadeFunction> cascade_check </cascadeFunction>
<argument><![CDATA[
result >= 0
]]>
</argument>
</command>
</endPosition>
</run>
</controlFile>
