Frama-C WP eklentisi kaç tane geçici değişken kullanabilir?

Question

Toplam 44 geçici değişkenin bulunduğu belirli bir programın en zayıf önkoşulunu oluşturmaya çalışıyordum. 2 geçici değişkenin değerleri varsayılmaktadır. Diğer tüm değişkenler bu iki değişkenden türetilmiştir. Ayrıca, 2 giriş değişkeni vardır. İşte kodumun bir segmenti.

void main(int err1_10, int err2_10){ 
    int x_mkfirm1,x_mkfirm2; 
    int dist_00=0, dist_10=5, a00=0, a01=0, a10=-1, a11=0, b00=1,b10=0, u=2; 
    int K_00=-1, K_01=1, x0_00=0,x0_10=3; 
    int x1_00,x2_00,x3_00,....,x20_00; 
    int x1_10,x2_10,x3_10,....,x20_10; 
    x0_00=x0_00+dist_00; 
    x0_10=x0_10+dist_10; 
    u=-K_00*x0_00-K_01*x0_10; 
    x1_00=a00*x0_00+a01*x0_10+u*b00; 
    x1_10=a10*x0_00+a11*x0_10+u*b10; 
    u=-K_00*x1_00-K_01*x1_10; 
    ........................... 
    ........................... 
} 

oluşturulan zayıf önkoşul böylece x4_10 ve açısından gelir. x1_00, x1_00'dan 'e kadar hiç bir bahsedilmemiştir. Ayrıca üretilen en zayıf önkoşul içinde girdiler mevcut değildir. Frama-c wp'nin çıktı mesajı Alt-Ergo:0 (interruped: 1)'u gösterir. Değişken sayısında herhangi bir kısıtlama var mı?

Answer 1

WP, değişkenleri yeniden adlandırmaya eğilimlidir, bu nedenle, orijinal C kaynağından daha çok ispat zorunluluklarında aynı adları görmediğiniz normaldir. Üstelik, kodunuzdan gördüğüm kadarıyla, ara değişkenlerin çoğu aslında sabittir. Bu, normal olarak teori geliştiricilerine ispat yükümlülüğünü göndermeden önce WP tarafından basitleştirilecektir. Sadece ortaya çıkan değeri görmelisiniz.

İspat yükümlülüğünüzün Alt-Ergo tarafından boşaltılamaması ile ilgili olarak, tam dosyaya sahip olmaksızın cevap vermek temelde imkansızdır. Spesifikasyondaki bir hatadan ya da koddan otomatik teoremi geliştirenler için genellikle erişilemeyen doğrusal olmayan hesaplamalara sahip olmaktan çok fazla olasılık vardır. Bununla birlikte, birçok ara değişkene sahip olmanın, çok önemli bir rol oynaması muhtemel değildir.