이 예를 들어 나는 다음과 같은 기능을 사용하여 값.FRAMA-C는 비 결정적 플로트
원하는 변수 x는 -inf, + inf 및 NaN을 포함하여 가능한 모든 부동 소수점 값으로 간주됩니다.
x가 NaN 인 경우 some_error()에 도달 할 수있는 결과를 얻고 싶습니다.
그래서 제 질문은 :
어떻게 비 결정적 수레를 시뮬레이션 할? 특정 함수 호출의 연결 가능성을 테스트하려면 어떻게합니까?
Frama-C는 무한/NaN 부동 소수점 값에 대해 서로 다른 수준의 지원을 제공하는 플러그인 모음입니다. 나는 WP가 NaN과 무한대를 지원한다고 믿는다; 하지만 이것은 아마도 당신이 선택한 숫자 모델 (옵션 -wp-model)에 달려 있습니다.
추상 해석 플러그인 (EVA, 이전 값)의 경우 NaN 및 무한은 지원되지 않습니다. 분석기는 모든 부동 소수점 값이 유한하다고 가정하고 증명합니다. Frama-C Sulfur에는 비 한정의 지원이 추가됩니다.
또한 nondet_float 함수는 유효하지 않습니다. 초기화되지 않은 값을 반환하는 것은 C 표준에 의해 금지되며,이 함수는 예를 들어 C로 표기됩니다. EVA. 대신 본문이없는 함수를 사용하고 절은 assigns \result \from \nothing을 지정해야합니다.
예를들 수 있습니까? 나는 당신이 그것을 어떻게 의미하는지 이해하지 못합니다. – Derping
답변의 일부분. 또한 어떤 플러그인을 사용 하시겠습니까? – byako
예를 들면 : "대신 본문이없는 함수를 사용해야합니다. 절에 \ result \ from \ nothing이 지정되어 있습니다." 최적의 방법으로 특정 코드의 도달 가능성을 증명할 수있는 플러그인이 필요합니다. 내 예제에서는 some_error() 호출에 연결할 수 있는지 확인하고 싶습니다. WP와 추상 해석 모두 가능합니다. 아오 라이 (Asorai). 내 이해 후에 추적 추상화 (Trace Abstraction)를 수행합니다. NAN/INF에 대한 지원이 필요하므로 추상 해석을 사용할 수 없으므로 WP/Aorai 플러그인을 사용해야합니다. – Derping
함수 :'nondet_float()'는 초기화되지 않은 지역 변수의 내용을 반환합니다. 결과는 정의되지 않은 동작입니다. 아마도'srand()'와'rand()'를 사용하여 float 값을 얻는 등 재 설계를 제안하십시오. – user3629249