SnoopStop Origin

C ya da Rust kodunuzu yapıştırın. Her dizi erişimi, bölme ve tamsayı işlemi için iki sonuçtan birini verir: ya tüm girdilerde güvenli olduğunu matematiksel olarak kanıtlar ya da açığı tetikleyen gerçek girdiyi bulur, onu çalıştırıp gösterir ve kapattığı yeniden kanıtlanmış bir yama önerir.

Deneme sürümü. Şimdilik C'nin bir bölümünü anlar: tüm tamsayı türleri (char, short, int, long, unsigned, size_t), bunların dizileri, metinler, döngüler, koşullar, kendi fonksiyonlarınız ve strcpy, strcat, strncpy, strlen, memcpy, memset gibi kütüphane fonksiyonları, işaretçiler (*p, p + i, &a[i], NULL) ve malloc / calloc / free. ve struct (s.x, p->x, a[i].x, p->ad[i], typedef). İşaretçinin işaretçisi ve işaretçi tutan alanlar henüz yok. Eşzamanlılık ve yetki (yeni): genel değişkenler, pthread_mutex_t kilitleri, //@ guarded_by m (veri yarışı), çift kilitleme ve kilidi açık bırakarak dönme; //@ grants X if ... / //@ requires \granted(X) ile bildirilen yetki modeli. Kural sizin bildirdiğinizdir; araç onun her yolda tuttuğunu kanıtlar. İş parçacıklarının araya girme sıraları tek tek denenmez: kilit disiplinine uyan kodda yarış olmaz, uymayan yol gösterilir. Rust (yeni): tamsayı türleri, dilimler (&[T], &mut [T]), diziler ([v; N]), alt dilimler (&a[i..j]), .len(), for / while, if ifadeleri, as, wrapping_*, assert! / panic!. Taşma denetimi açık derleme varsayılır (taşma panik sayılır). Yapılar, Vec, yineleyiciler henüz yok; otomatik yama ve "Hepsini düzelt" şimdilik yalnız C için. "Kanıtlandı" yalnız aşağıda listelenen özellikler için geçerlidir ve bu aracın doğru çalıştığı varsayımına dayanır; bağımsız bir denetimden geçmedi. Güvenlik incelemesinin yerini tutmaz.

//@ requires 0 <= i && i < n;      // çağıran bunu sağlamalı
//@ ensures \result >= 0;            // fonksiyon bunu garanti eder
int al(int a[], int n, int i) { ... }

//@ invariant 0 <= i && i <= n;      // döngünün her turunda doğru
for (int i = 0; i < n; i++) { ... }