Examples: PHP String Analyzer

Examples

The followings are the examples in the distribution.

example1

% phpsa -ispec example1.ispec -simplify example1.php

Result:

({$316$,$320$,$325$,$334$},                                        // set of nonterminals
 {$316$ -> $320$1|$334$,$320$ -> $325$|0$316$1,$325$ -> 0abc|0xyz, // productions
  $334$ -> abc|xyz},
 $316$)                                                            // start nonterminal

example2
We can check the context-free grammar obtained by the analyzer against a regular expression. There are two modes of checking. The first mode is to check whether or not L(Prog) is disjoint with L(Spec).
```
% phpsa -ispec example2.ispec -spec example2.spec example2.php    
```
Result:
In this case, the output is not disjoint with L(Spec). Then, the following counter example is shown by the analyzer.
```
<html><body>
<script></body></html>
```
example3
This example is about the second mode of checking. It checks whether or not L(Prog) <= L(Spec). For this mode, we supply the option '-inclusion'.
```
% phpsa -ispec example3.ispec -inclusion -spec example3.spec example3e.php    
```
Result:
```
L(Prog) is a subset of L(Spec).
```
validation1 : XHTML validation
```
% phpsa -ispec validation1.ispec -validate validation1.php
```
Result:
```
Valid
```
'xhtml1-transitional.dtd' is used for validation by default. You can specify an alternate DTD file by -dtdfile option.

validation2 : XHTML validation

% phpsa -ispec validation2.ispec -validate validation2.php

The generated document is invalid because the <p> element cannot occur directly under the <ul> element. result:

Invalid for <ul>
<p>                               // This says <p> occurs under <ul>
...
Counter example:
<html>
<head><title>test</title></head>
<body>
<ul><p>
</p></ul>
</body>
</html>

htmlvalidation1 : HTML validation
```
% phpsa -htmlvalidate htmlvalidation1.php    
```
Result:
```
Valid
```
- In this example generates a HTML page where </pgt; is omitted.
- The validation is based on the HTML 4.01 Transitional DTD.
htmlvalidation2 : HTML validation
```
% phpsa -htmlvalidate htmlvalidation1.php    
```
Result:
```
Valid
```
In this example generates a HTML page where a table where many optional tags are used.
smplbbs : more realistic XHTML validation, SQL query string validation
```
% phpsa -ispec smplbbs.ispec -validate smplbbs.php    
```
smplbbs is a simple Web-based bulletin board program where a string [b]...[/b] in a comment field is translated into <b>...</b>.
- A newline in a comment is translated into a combination of
  and the newline.
- the file 'samplbbs.html' is an output obtained by running smplbbs.php.
```
% phpsa -ispec smplbbs.ispec -mysql -spec smplbbs_sql.spec smplbbs.php    
```
With -mysql option, query strings in mysql_query is analyzed instead of the output of a program.