Frama-C: Eklentide Ek Açıklama Ekle

Bir Frama-C-plugin yazıyorum. Bu eklentide, işlevlere ek açıklamalar eklemek istiyorum (ör., Işlev adı = "test", bir şart cümlesi ekleyin, parametre == 1).Frama-C: Eklentide Ek Açıklama Ekle

Annotations.add_requires işlevini buldum, ancak bazı parametreleri (Emitter.t, Identified_predicates) bilmiyorum. String parametresi, işlev adı veya yüklemi için kendi adıdır.

Bu işlevi nasıl kullanırım? Birisi örnek gösterebilir mi?

kaynak

2016-03-29 Thomas Böhm

Bir şey denediniz mi? "Parametre" nin "test" fonksiyonunu ('kernel_function') ve değişkenini (' varinfo') bulmayı başardınız mı? Şimdi, 'add_requires' kullanmadan önce 'parametre == 1' yüklemesini oluşturmalısınız, değil mi? Bunu nasıl yapacağını buldun mu? – Anne

Çekirdek_fonksiyonu ve varinfo aldım. Üçüncü parametreyi (isminin bu olduğunu düşünüyorum) "test et" olarak ayarladım. Artık, onları nasıl oluşturacağımı bilmediğim 2 tane daha parametre (ilk ve son) var. Emitter bir oluşturma işlevine sahiptir, ancak ne yaptıklarını bilmediğim birkaç liste alır (şimdi "Emitter.create" adını denedim "name" [Code_annot] [] [] 'Ayrıca, nasıl yapılacağını bilmiyorum Diğer birçok garip şeyler içerdiğinden, yüklem listesi, bu yüzden ad ve vericiyle diğer iki denemeyi de test edemiyorum. –

Şimdi şunu denedim: 'pred = Cil_types.Ptrue in id_pred = {ip_name = []; ip_loc = location; ip_id = 1; ip_content = pred} ', ama hangi konumun kullanıldığını bilmiyorum? –

Yayıcı, eklentinizi tanımlar ve değiştirmeyi düşündüklerini beyan etmek zorundadır. Bir kernel_function için bu ilk parametre eşit olduğunu söyleyen bir ön şartı nasıl oluşturulacağını örneğidir,

let emitter = Emitter.create "My plugin" [ Emitter.Funspec ] 
    ~correctness:[] ~tuning:[]

Şimdi: Eğer şartnamelere özelliklerini eklemek istediğiniz gibi durumda, sen bunu inşa edebilirsiniz one:

let add_pre kf = match Kernel_function.get_formals kf with 
    | [] ->() 
    | c_var::_ -> 
    let l_var = Cil.cvar_to_lvar c_var in 
    let var_term = Logic_const.tvar l_var in 
    let cnst_term = Logic_const.tinteger 1 in 
    let eq_pred = Logic_const.prel (Cil_types.Req, var_term, cnst_term) in 
    let pred = Logic_const.new_predicate eq_pred in 
    let bname = Cil.default_behavior_name in 
    Annotations.add_requires emitter kf ~behavior:bname [pred]

kaynak

2016-03-31 07:22:10 Anne

Kod snippet'ini kullanıyorum (ki bu mantıklı geliyor). // @ config gerektirir == 1; C kodunda ve bir yorumun add_pre çağrısını yaparsanız, değer analizi 'config_0 -> \t {{NULL -> {1}}}' gösterir, ancak elle yazılmış, işlevinizi gerektirir ve çağırırsa, 'config_0 -> \t {{NULL -> [- ...--]}} 'gibi biter (bir şey yapmadığı gibi) Her iki durumda da, işlevinize yapılan çağrıdan (başarılı durumda yorumlanmıştır) sonra,! Db.Value.compute() işlevini çağırıyorum. Aynı şekilde tepki vermemeli mi? –

Özelliğin doğru eklenip eklenmediğini görmek için '-print 'seçeneğini kullanmayı deneyebilirsiniz. – Anne

Ve ayrıca frama-c file.c -your-plugin-option -then -val işlevini de deneyin (buradaki gibi görünüyor). – Anne

Frama-C: Eklentide Ek Açıklama Ekle

cevap

İlgili konular