일종의 별칭 분석을 수행하는 frama-c 플러그인을 개발하기 시작했습니다. Dataflow.Backwards 분석을 사용하고 있습니다. 이제는 다른 할당 문을 거치고 lvalues에 대한 정보를 수집해야합니다. frama-c는 3 주소 코드를 제공합니까? lvalue (또는 메모리 액세스)의 모양에 대해 몇 가지 보장이 있습니까? 내 말은, 그을음이나 말
에서 \와 루프 불변을 입증 할 수 없습니다 WP. ACSL by Example (68 페이지, swap_ranges)에도 이와 유사한 기능이 있지만이 기능은 WP 플러그인에서이 특정 기능을 증명할 수 없었습니다. 나는 내 컴퓨터에서 그것을 시도했지만 참으로 똑같은 불변성을 증명할 수는 없다. 전체 코드 /*
* memswap()
*
* Swaps t
OCaml에서 C 헤더 파일을 처리하는 방법으로 frama-c를보고있었습니다 (예 : 언어 바인딩 생성 용). 매우 잘 문서화되고 유지 보수 된 프로젝트처럼 보이기 때문에 매력적입니다. 그러나 문서를 통해 검색 및 검색을 많이 한 후에는 용도에 맞는 것을 찾을 수 없습니다. 이 작업을 수행하는 올바른 방법이 누락 되었습니까, 아니면 frama-c 범위를 벗
frama-c의 WP 플러그인을 사용하여 간단한 어설 션을 증명하려고합니다. C 코드는 Targetlink 검색 테이블에서 생성되었습니다. 필자는 함수에 충분한 주석을 제공하여 호출하는 프로그램의 속성을 증명하기 위해 결과 계약을 사용할 수 있습니다. 첫 번째 단계로서 상수를 참조 해제 된 포인터에서 얻은 값과 비교하는 함수의 시작 부분 근처에 어설 션을
C 매크로에 ACSL을 사용하여 주석을 추가 할 수 있습니까? 는 예 : /*@
assigns \nothing;
behavior xmin:
assumes x < y;
ensures \result == x;
behavior ymin:
assumes y <= x;
ensures \resu
배열에 대한 수량화 된 어설 션을 증명하려고 시도 중이며 몇 가지 문제가 있습니다. 다음과 같은 작은 프로그램을 고려 나는 '형식화'메모리 모델을 사용하고 int a[4] = {1,2,3,4};
/*@ requires p == a;
assigns \nothing;
*/
void test(int *p)
{
p++;
//@
내가 FRAMA-C에 새로 온 사람과 나는이 간단한 예제와 문제가 무엇인지 이해하고 싶습니다 :이 예에서 /*@ requires \valid(array+(0..length-1))
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0;
@ assigns array[0..length-1];
*/
외부 함수의 동작,보다 정확하게는 종료를 지정하려고합니다. ACSL 문서에 따르면 \terminates p; 속성은 술어 p이 보유하는 경우 함수가 종료되도록 보장하지만 p이 보유하지 않을 경우 아무 것도 지정하지 않도록 지정합니다. //@ ensures \false ; terminates \false ;
는 또한 ACSL이 갑자기 종료의 경우 사후 조
포인터를 입력으로 사용하는 함수의 종속성에 대해 ACSL 사양을 작성하고 포인터가 NULL이 아닌 경우 내용을 사용합니다. /*@ behavior p_null:
assumes p == \null;
assigns \result from \nothing;
behavior p_not_null:
assumes p != \n