Frama-c로 C 코드 조각 내기

Question

frama-c로 표시된 사용되지 않는 변수를 잘라야합니다. 하지만 라인을 명령 아무 생각이 나는 https://frama-c.com/slicing.html에 언급 한 바와 같이 하나의 명령 줄

Last login: Thu Nov 9 20:48:42 on ttys000 
Recep-MacBook-Pro:~ recepinanir$ cd desktop 
Recep-MacBook-Pro:desktop recepinanir$ cat hw.c 
#include <stdio.h> 

int main() 
{ 
    int x= 10; 
    int y= 24; 
    int z; 

    printf("Hello World\n"); 

    return 0; 
} 

Recep-MacBook-Pro:desktop recepinanir$ clang hw.c 
Recep-MacBook-Pro:desktop recepinanir$ ./a.out 
Hello World 
Recep-MacBook-Pro:desktop recepinanir$ clang -Wall hw.c -o result 
hw.c:5:9: warning: unused variable 'x' [-Wunused-variable] 
    int x= 10; 
     ^
hw.c:6:9: warning: unused variable 'y' [-Wunused-variable] 
    int y= 24; 
     ^
hw.c:7:9: warning: unused variable 'z' [-Wunused-variable] 
    int z; 
     ^
3 warnings generated. 
Recep-MacBook-Pro:desktop recepinanir$ 

Answer 1

에 사용되지 않는 모든 변수를 슬라이스 쓰기 안 가지고, 슬라이스는 항상 상대적 어떤 기준이며, 목표는 작은 프로그램을 생산하는 것입니다 원래 기준에 부합하는 동시에 기준과 관련하여 동일한 행동을 나타냅니다. Slicing 플러그인 자체는 이러한 기준을 수립하는 몇 가지 방법을 제공하지만 Sparecode 플러그인 (https://frama-c.com/sparecode.html)의 결과에 관심이있는 것으로 보입니다. 이것은 특수화 된 조각이며, 끝은 프로그램 상태입니다. 귀하의 분석 엔트리 포인트 (예 : main). 즉, Sparecode는 분석중인 코드의 최종 결과에 기여하지 않는 모든 것을 제거합니다. 귀하의 경우 frama-c -sparecode-analysis hw.c은 다음 결과를 제공합니다 (printf에 대한 호출이 Variadic 플러그인에 의해 수정되었으며 해당 인수가 main의 최종 상태에 유용하지 않은 것으로 나타남). 이것이 문제인 경우, 그들이 어떤 전역 변수에 영향을 미칠 것으로

/* Generated by Frama-C */ 
#include "stdio.h" 
/*@ assigns \result, __fc_stdout->__fc_FILE_data; 
    assigns \result 
     \from (indirect: __fc_stdout->__fc_FILE_id), 
      __fc_stdout->__fc_FILE_data; 
    assigns __fc_stdout->__fc_FILE_data 
     \from (indirect: __fc_stdout->__fc_FILE_id), 
      __fc_stdout->__fc_FILE_data; 
*/ 
int printf_va_1(void); 

int main(void) 
{ 
    int __retres; 
    printf_va_1(); 
__retres = 0; 
return __retres; 
} 

마지막)을 ACSL 사양 나타내는 함께 전문화 출력 기능을 제공 할 필요가 D, 일반적인 경우 것을 유의 슬라이싱 (따라서 Sparecode)는 overapproximation을 준다 : 그것은 기준에 아무런 영향을 미치지 않는 진술 만 삭제합니다.