Free Trial

Safari Books Online is a digital library providing on-demand subscription access to thousands of learning resources.

Share this Page URL

13.6 Static Analysis Techniques and Tool... > 13.6.1 Static Type Checking - Pg. 345

CHAPTER 13 alleviate the problem, but the run-time improve- ments may be necessary. There are many pro- posals on how to fix this issue. One approach is to certify that the compiler does exactly what it claims, which can be a complicated process. A set of compilers could be used to compile the same code and the compiled output could be compared, an approach proposed by Eide and Regehr [24] for detecting compiler bugs in general, but finding independent implementa- tions of compilers for PCC may be prohibitive. Another approach is to prove the correctness of the algorithms used in the compiler, but there could still be bugs in the implementations. Addi- tionally, any proof of the implementation must be redone any time there is a change to the compiler. Languages and Security 345 support for PCA systems [27]. PCAL is an exten- sion of the Bash scripting language, where the PCA annotations are converted to regular Bash scripts. These scripts can then be used in an existing PCA system. Contribution of this work is the language annotations and their compiler. The annotations allow the programmer to specify what proofs they think hold at certain points of the program. The compiler then uses a theorem prover to produce the proofs statically, so they can be passed to the PCA system. 13.6. STATIC ANALYSIS TECHNIQUES AND TOOLS Static checking techniques can have their roots traced back to statically typed languages such as Fortran, C, and Java. For these program- ming languages, the compiler would check to make sure that there were not any type violations 13.5.1. Current Research