A sequence point in C is any point in the execution point of a program at which all side effects of previous evaluations performed and no side effects from subsequent evaluations have yet been performed. The end of a full expression, between of the left and right operands of the && (logical AND), || (logical OR), and comma operators are the typical sequence points of C expressions. The evaluation of C expressions missing sequence point like may produce different result from that of other compilers due to the missing sequence point. That is, C expressions missing sequence point have a potential to cause unexpected portability problems. C standard has defined those kind of expressions as undefined and proposed a method for detecting expressions missing sequence points. Also several tools such as GCC compiler and Splint provide a feature which detects errornous expression due to missing sequence points. But those are all based on C programming language specification described informally. That is, the results depend on the interpretation of C specification.
We avoid the possibility of interpretation of C standard variously by choosing formal specification of C language which is mechanized by Michael Norrish. From the formal specification, we have derived reduction relations for detecting undefined expressions which is caused by missing sequence points. Base on the derived rules, we have implemented context-sensitive term rewriting system. It has revealed that existing tools providing a feature detecting missing sequence points show different results. Some of them detects less or more than expected result.
C 언어에서 시퀀스 포인트는 이전 평가에서 발생한 모든 사이드 이펙트가 완료되고 다음 평가의 사이드 이펙트는 수행되지 않은 프로그램 지점이다. 수식의 끝과 논리연산자(&&, ||)와 콤마(,) 연산자의 왼쪽과 오른쪽 인자 사이가 전형적인 시퀀스 포인트가 된다. 시퀀스 포인트가 누락된 C 수식의 평가는 컴파일러마다 다른 결과를 낼 수도 있다. 즉, 시퀀스 포인트가 누락된 C 수식은 예상치 못한 이식성 문제를 일으킬 수 있는 잠재성을 가지고 있다. C 표준은 이러한 수식을 undefined 라고 정의 하였고 시퀀스 포인트가 누락되었는지 여부를 판별하는 방법들을 제안하였다. 뿐만 아니라 GCC 컴파일러나 Splint 같은 정적분석도구에서도 이러한 기능을 제공하고 있다. 그러나 이들은 모두 자연언어인 영어로 쓰여진 C 언어 명세서에 기반을 하고 있다. 즉, 시퀀스 포인트의 누락여부를 판별하는 결과는 C 언어 명세서를 어떻게 해석하느냐에 따라 그 결과가 달라 질 수 있다.
우리는 C 표준을 여러 가능성으로 해석할 여지를 피하기 위해 Michael Norrish 에 의해 만들어진 C 언어 형식 명세서를 그 기준으로 채택하였다. 이 형식명세서로부터 우리는 시퀀스 포인트가 누락되었는지 여부를 확인하기 위한 reductino 규칙을 도출하였다. 이 규칙들을 가지고 우리는 항 개서 시스템을 구현하였다. 이것은 기존의 툴들이 서로 다른 결과를 보여주고 있다는 것을 확인시켜주었다. 그들 중 일부는 예상보다 적거나 혹은 더 많이 시퀀스 포인트의 누락을 탐지하였다.