슬라이스시 C 파일에 여러 인수 전달

Question

내 소스 코드에서 내 주요 메소드 인 a.c는 두 개의 인수를 허용합니다. 하나는 파일 이름이고 다른 하나는 정수입니다.

 ./a.out filename1.txt 3 

을하지만 FRAMA-C와 슬라이스를 사용하려고하면

 frama-c a.c filename1.txt 3 -slice-...... 

Framac이 파일 3을 찾을 수 없다는 오류가 발생합니다 ??? : 나는 그것을 좋아 실행

filename1.txt_3을 입력하고 코드 내에서 별도로 추출 할 때도 다른 옵션을 시도했지만 frama-c도 이와 유사하지 않았습니다. 그것은 그것이 파일 filename1.txt_3을 찾을 수 없습니다 불평. FRAMA C를 실행할 때

분석 된 프로그램이 명령 행 인수를 필요로하는 경우

Answer 1

, 당신은 일반적으로 인수를 구축 argc 및 argv하고이를 전달합니다 void의 함수를 작성해야 나 소스에 여러 인수를 보내는 방법을 알려주세요 분석 프로그램의 main() 기능 :

int analysis_main(void) { 
    char *argv[] = { "myprogram", "filename1.txt", "3", 0 }; 
    return main(3, argv); 
} 

주 그 목표는 파일의 이름으로 사용 "filename1.txt"이 경우 fopen()로 열고 fread()과에서 읽고해야하는 경우 파일의 내용이 프로그램의 동작과 관련이 있기 때문에 호출 할 때 원하는 결과를 반환하는 두 함수의 구현을 제공하는 것이 좋습니다. 분석 프로그램이하는 첫번째 것은 strtol()에 argv[2]을 통과하는 경우

반대로, 당신이 실용적으로 strtol()에 대한 구현을 제공하는 대신 프로그램의 비트를 단순화 할 수 있습니다,의 분석은 어디 없음 복잡성을 소개하는 것 필요했다.