Frama-C 포함 파일의 경로를 지정하는 방법은 무엇입니까?

Question

사용할 파일이 포함 된 Frama-C 을 어떻게 말 할 지 결정하는 데 몇 가지 문제가 있습니다. 보통 Frama-C의 표준 사양을 사용하기 위해

-cpp-extra-args="-I $(frama-c -print-path)/libc" 

옵션을 추가합니다. 하지만 종종 Frama-C 라이브러리에없는 것들이 필요합니다. 예를 들어

, 내가 분석 할 소스 파일 중 하나 <sys/wait.h>, 에 정의되어 있지만 FRAMA-C가 자신의 frama-c/libc/sys/wait.h을 가지고 있기 때문에, GCC의 파일이 포함되지 않은 매크로를 사용합니다. 아쉽게도 Frama-C는 매크로를 정의하지 않으므로 결국 정의가 누락됩니다. 물론 소스 파일을 변경하고 싶지 않습니다!

나는 FRAMA-C 파일과있는 내가 GCC 파일에서 누락 된 것을 복사 할 수 있습니다 포함 것 my_libc/sys/wait.h 파일을 로컬 디렉토리 을 건물의 생각했다.

당신은 어떻게 생각 ...

-cpp-extra-args="-I my_libc -I $(frama-c -print-path)/libc" 

하지만 약간은 파일을 포함 GCC에서 정의를 추출하는 것은 매우 까다로운 일이 될 수 있기 때문에 내 솔루션이 걱정입니다 :

그때 사용해야합니까? 좋은 생각 인 것 같습니까? 더 나은 조직에 대한 조언이 있으십니까?

Answer 1

이 솔루션은 괜찮은 것처럼 보입니다. gcc의 헤더에서 정의를 추출하는 것은 실제로 복잡 할 수 있지만 거기에는 선택의 여지가 없습니다. 어떤 시점에서 매크로를 제공해야하며 전체 헤더를 갖고 싶지 않을 것입니다. Frama-C로 끝남).

나는 아무 사전 처리 전문가는 아니지만, 난 당신이 제안한다 -cpp-extra-args 옵션을 모두 my_libc/sys/wait.h 및 $FRAMAC_SHARE/libc/sys/wait.h을 포함 할 수 있습니다 모르겠어요 : 두 sys/wait.h 헤더와 cpp 항상 선택됩니다와 끝까지 첫번째. 단지 그들

당신이 #include <libc/sys/wait.h>와 헤더를 정의

• 당신이 (잠재적 FRAMA-C의 libc의에서 copy'n 페이스트) 자신의 표준 헤더를 정의하고 사용하고 -cpp-extra-args=... -I$(frama-c -print-path)이 : 나는이 개 솔루션을 참조 헤더의 상대 경로에 대한 혼동을 피할 수 있습니다.

대부분의 경우 해당 Frama-C 파일로 리디렉션하거나 복사하는 경우에도 응용 프로그램에서 사용하는 모든 헤더 파일을 제공해야합니다. 하지만 당신이 몇 가지 쉘 명령으로 끝내야한다고 생각합니다.