int max_seq(int* p, int n) {
int res = *p;
for(int i = 0; i < n; i++) {
if (res < *p) { res = *p; }
p++;
}
return res;
}
Frama-C
ACSL
Frama-C
Przeglądanie kodu
Główne
zestaw narzędzi do analizy statycznej
Zastosowania:
- przeglądanie skomplikowanego kodu
- dowodzenie własności
ANSI/ISO C Specification Language
Wtyczki
- Impact analysis
- Scope & Data-flow browsing
- Variable occurrence browsing
requires \valid(p) && \valid(q);
ensures *p <= *q;
Proving
Value
analysis
Frama-C
Inne
Zmienianie kodu
Framework
- integracja wielu narzędzi
- dobry start dla nowych rzeczy
- Semantic constant folding
- Slicing
- Spare code
void max_ptr(int *p, int* q) {
if (*p > *q) {
int tmp = *p;
*p = *q;
*q = tmp;
}
}
- manuale
- tutoriale
- blog
- wiki
- przykłady
- grupy dyskusyjne
void max_ptr(int* p, int*q) {
*p = *q = 0;
}
requires \valid(p) && \valid(q);
ensures *p <= *q;
ensures (*p == \old(*p) && *q == \old(*q)) ||
(*p == \old(*q) && *q == \old(*p));
int max_seq(int* p, int n);
Weryfikacja bezpieczeństwa
bezpieczeństwo pamięci
Jessie
void max_ptr(int *p, int* q) {
if (*p > *q) {
int tmp = *p;
*p = *q;
*q = tmp;
}
}
- dereferencja wskaźników
- dostęp do tablicy
bezpieczeństwo arytmetyki
- przepełnienie
- dzielenie przez zero
- dowodzenie własności
- specyfikacja w języku ACSL
terminacja
- pętle
- funkcje rekurencyjne
int max_seq(int* p, int n);
requires n > 0;
requires \valid(p+ (0..n−1));
ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];
ensures \exists int e; 0 <= e <= n−1 && \result == p[e];
requires n > 0;
requires \valid(p+ (0..n−1));
ensures \forall int i; 0 <= i <= n−1 ==>
\result >= p[i];
ensures \exists int e; 0 <= e <= n−1 &&
\result == p[e];
C + ACSL
ensures \forall int i; 0 <= i <= n−1 ==> p[i] == \old(p[i]);
Frama - C Core
/*
terminates c>0;
assigns \nothing;
*/
JAVA + JML
CIL + annot
Weryfikacja
funkcjonalności
Jessie Plugin
Krakatoa
void f (int c) { while(!c); return;}
requires n > 0;
requires \valid(p+ (0..n−1));
ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];
ensures \exists int e; 0 <= e <= n−1 && \result == p[e];
JESSIE
requires n > 0 &&\valid(p + (0..n−1));
ensures \result == \max(0,n−1,
\lambda integer i; p[i]);
Jessie2Why
- funkcja robi to co trzeba
- weryfikacja kontraktów
assigns \nothing;
WHY
VC Generator
/*
requires c!=0;
assigns \nothing;
*/
VC
void f (int c) { while(!c); return;}
Automatic Provers:
- Alt - Ergo
- CVC3
- Simplify
- Yices
- Z3
Demo