Completion Of Coccinelle Control Flow,Design And Testing

With the increase in system complexity and codebase scale,software developers realized that it has become more and more difficult to rely on manual methods to maintain systems and eliminate system errors.The formal method is widely used in verification of the system because of its high accuracy and automation.As a technology of the formal method,model checking is a based on the abstraction of the system model and the verification of the property specification.Model checking is not only suitable for correctness and safety verification before system development,but also useful for maintenance of system.Coccinelle is a program matching and transformation tool based on the model checking.It was proposed to solve the collateral evolution problem in Linux drivers caused by system API library changes.As its description language,SmPL can expressively describe the code pattern which also includes the patterns that is prone to serious system errors.SmPL can precisely search for code blocks matching against the given code pattern.Currently SmPL supports different control flows but lacks support for the do-while loop,which would restrict its accuracy and coverage ratio of problematic code.We propose the do-while loop extension to Coccinelle including the modeling and formula design of the do-while loop in Coccinelle.We abstract a generic form of do-while loop in C language code and present it in control flow graph and translate do-while loop into CTL formulas.Finally,within Coccinelle,by adding the grammatical definition for do-while,and completing the transformation from code to AST to CTL formula,expanded the ideographic ability of SmPL contributes to the completion the functionality of control flow of Coccinelle.The results of this paper mainly include: 1.We have tested the improved Coccinelle.The test results show that the improved Coccinelle can correctly parse the do-while loop containing the composite control structure and the nested structure.2.We also investigate the code patterns in the Linux kernel with the improved Coccinelle and survey about the number and code distribution of the do-while loop.It also successfully verified a specific kernel problem,and the results show that the achievements of this paper are both of correctness and practicability.