कोड के लिए सबूत जो हस्ताक्षरित पूर्णांक ओवरफ़्लो पर निर्भर करता है?

Question

मुझे कुछ अक्षमता से बचने के लिए निम्नलिखित की तरह कोड की शुद्धता को साबित करने के लिए कैसे दृष्टिकोण करना चाहिए, मॉड्यूलर अंकगणित पर निर्भर करता है?

#include <stdint.h> 

uint32_t my_add(uint32_t a, uint32_t b) { 
    uint32_t r = a + b; 
    if (r < a) 
     return UINT32_MAX; 
    return r; 
} 

मैं WP के "पूर्णांक" मॉडल के साथ प्रयोग किया गया है, लेकिन, अगर मैं सही ढंग से समझ, कि मॉडल पीओ में तार्किक पूर्णांकों का अर्थ विज्ञान, नहीं सी कोड की औपचारिक मॉडल कॉन्फ़िगर करता है। उदाहरण के लिए, "int" मॉडल का उपयोग करते समय ऊपर दिए गए हस्ताक्षर किए गए अतिरिक्त के लिए WP और RTE प्लगइन्स को अभी भी ओवरफ़्लो दावा पीओ की आवश्यकता होती है और इंजेक्ट करता है।

इस तरह के मामलों में, क्या मैं एक कथन या मूल ब्लॉक के लिए लॉजिकल मॉडल को निर्धारित करने वाली टिप्पणियां जोड़ सकता हूं, इसलिए मैं फ्रैमा-सी को बता सकता हूं कि एक विशेष कंपाइलर वास्तव में एक कथन का अर्थ कैसे देता है? यदि ऐसा है, तो मैं परिभाषित-लेकिन-अक्सर-दोष-प्रेरक व्यवहार जैसी चीजों के लिए अन्य सत्यापन तकनीकों का उपयोग कर सकता हूं जैसे हस्ताक्षरित रैप-आस-पास, कंपाइलर-परिभाषित व्यवहार, गैर-मानक व्यवहार (इनलाइन assy?), आदि, और उसके बाद शुद्धता साबित करें आसपास के कोड। मैं कुछ स्थिर विश्लेषकों को सूचित करने के लिए उपयोग किए जाने वाले "जोरदार फिक्स" से कुछ (लेकिन अधिक शक्तिशाली) के समान चित्रण कर रहा हूं कि कुछ गुण तब होते हैं जब वे अपने लिए गुण प्राप्त नहीं कर सकते हैं।

मैं संदर्भ के लिए, Frama-C Fluorine-20130601 के साथ काम कर रहा हूं, alt-ergo 95.1 के साथ।

Answer 1

मैं Frama-सी फ्लोरीन-20130601

आप नवीनतम संस्करण का उपयोग करने के लिए एक रास्ता मिल गया है कि देखने के लिए खुशी है कि के साथ काम कर रहा हूँ।

जेसी है:

#pragma JessieIntegerModel(modulo) 

ऊपर pragma यह विचार करना बनाता

यहाँ जानकारी के कुछ यादृच्छिक बिट्स है कि, हालांकि वे पूरी तरह से आपके प्रश्न का उत्तर नहीं है, में एक StackOverflow टिप्पणी फिट नहीं है कर रहे हैं कि सभी ओवरफ्लो (अपरिभाषित हस्ताक्षरित दोनों और परिभाषित हस्ताक्षरित वाले दोनों) चारों ओर लपेटते हैं (हस्ताक्षर किए गए ओवरफ्लो के समान में, 2 के पूरक अंकगणित में)। उत्पन्न प्रमाण दायित्व बहुत कठिन हैं, क्योंकि उनमें हर जगह अतिरिक्त मॉड्यूलो ऑपरेशन होते हैं। स्वचालित प्रमेय समर्थकों में से, आमतौर पर केवल सरलता उनके साथ कुछ करने में सक्षम है।

फ्लोरीन में, आरटीई डिफ़ॉल्ट रूप से ए + बी के बारे में चेतावनी नहीं करता है:

$ frama-c -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    r = a + b; 
    if (r < a) { 
    __retres = 4294967295U; 
    goto return_label; 
    } 
    __retres = r; 
    return_label: return __retres; 
} 

आरटीई विकल्प -warn-unsigned-overflow साथ अहस्ताक्षरित इसके बारे में चेतावनी देने के लिए बनाया जा सकता है:

$ frama-c -warn-unsigned-overflow -rte t.c -then -print 
[kernel] preprocessing with "gcc -C -E -I. t.c" 
[rte] annotating function my_add 
/* Generated by Frama-C */ 
typedef unsigned int uint32_t; 
uint32_t my_add(uint32_t a, uint32_t b) 
{ 
    uint32_t __retres; 
    uint32_t r; 
    /*@ assert rte: unsigned_overflow: 0 ≤ a+b; */ 
    /*@ assert rte: unsigned_overflow: a+b ≤ 4294967295; */ 
    r = a + b; 
    … 

लेकिन वह ठीक है आप जो चाहते हैं उसके विपरीत मैं नहीं देखता कि आप ऐसा क्यों करेंगे।

Answer 2

आपने सटीक कमांड लाइन प्रदान नहीं की है जिसका आप उपयोग कर रहे हैं। मुझे लगता है कि यह frama-c -wp -wp-rte file.c -pp-annot है। उस स्थिति में, वास्तव में, आरटीई संभवतः उत्सर्जित कर सकते हैं कि सभी दावे उत्पन्न होते हैं। हालांकि, आप उस पर एक बेहतर नियंत्रण कर सकते हैं, फ्रैमा-सी को पहली बार आरटीई की श्रेणियों को उत्पन्न करने के लिए जो आप रुचि रखते हैं (सावधान रहें कि उन्हें दो प्रकार के विकल्पों द्वारा नियंत्रित किया जाता है: frama-c -rte-help और -warn-{signed,unsigned}-{overflow,downcast} परिभाषित किए गए हैं कर्नेल में), और फिर परिणाम पर wp लॉन्च करें।

/*@ 
    behavior no_overflow: 
    assumes a + b <= UINT32_MAX; 
    ensures \result == a+b; 
    behavior saturate: 
    assumes a+b > UINT32_MAX; 
    ensures \result == UINT32_MAX; 
*/ 
uint32_t my_add(uint32_t a,uint32_t b);