Source code checker, source code checking method, program for causing execution of the method, and storage medium for storing the program

A non-transitory computer readable medium including a program causing a computer to execute a method of checking source code for a computer program comprising:

• a path extracting step for extracting an instruction series from the source code along an execution path representing an order for executing the instruction series, the execution path determined by simulating execution of the source code;
• and
• a checking information determining step for generating checking information of the source code according to the instruction series extracted in the path extracting step, the checking information corresponding to memory usage of the source code or indicating that the source code has been executed correctly, wherein the checking information determining step includes:
• a model graph composing step for composing a model graph from the instruction series extracted in the path extracting step;
• and
• a model description generating step for generating a model description from the model graph composed in the model graph composing step, wherein
• both the model graph composing step and the model description generating step are placed before a model checking executing step for performing model checking of the source code according to the model description and specifications expressing a property of checking the source code;
• and wherein
• checking of the source code is performed in the model checking executing step according to the model description generated by the model description generating step and preliminarily input specifications.

A source code checker executed by a processor, for checking source code for a computer program, the source code checker comprising:

• a path extractor programmed to extract an instruction series from the source code along an execution path representing an order for executing the instruction series, the execution path determined by simulating execution of the source code;
• and
• a checking information determining unit generating checking information of the source code according to the instruction series extracted by the path extractor, the checking information corresponding to memory usage of the source code or indicating that the source code has been executed correctly, wherein the checking information determining unit is placed before a model checker executing unit for performing model checking of the source code according to a model description and specifications expressing a property of checking the source code, and includes:
• a model graph composing unit for composing a model graph from the instruction series extracted by the path extractor;
• and
• a model description generator for generating the model description from the model graph composed by the model graph composing unit, and wherein the model checker executing unit checks the source code according to the model description generated by the model description generator and preliminarily input specifications.