2021-03-01 05:50 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002302Frama-CPlug-in > slicingpublic2017-12-06 09:12
ReporterYangyibiao 
Assigned ToNikolai_Kosmatov 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64OSUbuntuOS VersionUbuntu 16.04.4
Product VersionFrama-C 14-Silicon 
Target VersionFixed in VersionFrama-C 16-Sulfur 
Summary0002302: the return statement of a called function was wrongly removed
DescriptionWhile slicing the last statement in the attached test.c file, the "return g_79;" statement in function func_2 (line 312 in the test.c file) was wrongly removed from the slice.

gcc version: gcc(Ubuntu-5.4.0-6ubuntu1~16.04.4) 5.4.0 20160609

frama-c version: Silicon-20161101
Steps To Reproduceframa-c -cpp-command "gcc -C -E " test.c -slice-pragma main -then-on 'Slicing export' -print -ocode slice.c

gcc test.c -o test && ./test
gcc slice.c -o slice && ./slice
Tagscsmith
Attached Files
  • c file icon test.c (8,061 bytes) 2017-05-23 10:16 -
    /* Generated by Frama-C */
    typedef int wchar_t;
    typedef unsigned char uint8_t;
    typedef int int32_t;
    typedef unsigned int uint32_t;
    typedef unsigned long long uint64_t;
    /*@
    axiomatic MemCmp {
      logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n) 
        reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
      
      axiom memcmp_zero{L1, L2}:
        ∀ char *s1, char *s2;
        ∀ ℤ n;
          memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
          (∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
      
      }
     */
    /*@
    axiomatic MemChr {
      logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n) 
        reads *(s + (0 .. n - 1));
      
      axiom memchr_def{L}:
        ∀ char *s;
        ∀ ℤ c;
        ∀ ℤ n;
          memchr(s, c, n) ≡ \true ⇔
          (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
      
      }
     */
    /*@
    axiomatic MemSet {
      logic 𝔹 memset{L}(char *s, ℤ c, ℤ n) 
        reads *(s + (0 .. n - 1));
      
      axiom memset_def{L}:
        ∀ char *s;
        ∀ ℤ c;
        ∀ ℤ n;
          memset(s, c, n) ≡ \true ⇔
          (∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
      
      }
     */
    /*@
    axiomatic StrLen {
      logic ℤ strlen{L}(char *s) 
        reads *(s + (0 ..));
      
      axiom strlen_pos_or_null{L}:
        ∀ char *s;
        ∀ ℤ i;
          0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
          *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
      
      axiom strlen_neg{L}:
        ∀ char *s;
          (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
      
      axiom strlen_before_null{L}:
        ∀ char *s;
        ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
      
      axiom strlen_at_null{L}:
        ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
      
      axiom strlen_not_zero{L}:
        ∀ char *s;
        ∀ ℤ i;
          0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
      
      axiom strlen_zero{L}:
        ∀ char *s;
        ∀ ℤ i;
          0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
      
      axiom strlen_sup{L}:
        ∀ char *s;
        ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
      
      axiom strlen_shift{L}:
        ∀ char *s;
        ∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
      
      axiom strlen_create{L}:
        ∀ char *s;
        ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
      
      axiom strlen_create_shift{L}:
        ∀ char *s;
        ∀ ℤ i;
        ∀ ℤ k;
          0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
      
      axiom memcmp_strlen_left{L}:
        ∀ char *s1, char *s2;
        ∀ ℤ n;
          memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
          strlen(s1) ≡ strlen(s2);
      
      axiom memcmp_strlen_right{L}:
        ∀ char *s1, char *s2;
        ∀ ℤ n;
          memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
          strlen(s1) ≡ strlen(s2);
      
      axiom memcmp_strlen_shift_left{L}:
        ∀ char *s1, char *s2;
        ∀ ℤ k, ℤ n;
          memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
          0 ≤ strlen(s2) ≤ k + strlen(s1);
      
      axiom memcmp_strlen_shift_right{L}:
        ∀ char *s1, char *s2;
        ∀ ℤ k, ℤ n;
          memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
          0 ≤ strlen(s1) ≤ k + strlen(s2);
      
      }
     */
    /*@
    axiomatic StrCmp {
      logic ℤ strcmp{L}(char *s1, char *s2) 
        reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
      
      axiom strcmp_zero{L}:
        ∀ char *s1, char *s2;
          strcmp(s1, s2) ≡ 0 ⇔
          strlen(s1) ≡ strlen(s2) ∧
          (∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
      
      }
     */
    /*@
    axiomatic StrNCmp {
      logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) 
        reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
      
      axiom strncmp_zero{L}:
        ∀ char *s1, char *s2;
        ∀ ℤ n;
          strncmp(s1, s2, n) ≡ 0 ⇔
          (strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
          (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
      
      }
     */
    /*@
    axiomatic StrChr {
      logic 𝔹 strchr{L}(char *s, ℤ c) 
        reads *(s + (0 .. strlen(s)));
      
      axiom strchr_def{L}:
        ∀ char *s;
        ∀ ℤ c;
          strchr(s, c) ≡ \true ⇔
          (∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ c);
      
      }
     */
    /*@
    axiomatic WcsLen {
      logic ℤ wcslen{L}(wchar_t *s) 
        reads *(s + (0 ..));
      
      axiom wcslen_pos_or_null{L}:
        ∀ wchar_t *s;
        ∀ ℤ i;
          0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
          *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
      
      axiom wcslen_neg{L}:
        ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
      
      axiom wcslen_before_null{L}:
        ∀ wchar_t *s;
        ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
      
      axiom wcslen_at_null{L}:
        ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
      
      axiom wcslen_not_zero{L}:
        ∀ wchar_t *s;
        ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
      
      axiom wcslen_zero{L}:
        ∀ wchar_t *s;
        ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
      
      axiom wcslen_sup{L}:
        ∀ wchar_t *s;
        ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
      
      axiom wcslen_shift{L}:
        ∀ wchar_t *s;
        ∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
      
      axiom wcslen_create{L}:
        ∀ wchar_t *s;
        ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
      
      axiom wcslen_create_shift{L}:
        ∀ wchar_t *s;
        ∀ int i;
        ∀ int k;
          0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
      
      }
     */
    /*@
    axiomatic WcsCmp {
      logic ℤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
        reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
      
      axiom wcscmp_zero{L}:
        ∀ wchar_t *s1, wchar_t *s2;
          wcscmp(s1, s2) ≡ 0 ⇔
          wcslen(s1) ≡ wcslen(s2) ∧
          (∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
      
      }
     */
    /*@
    axiomatic WcsNCmp {
      logic ℤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, ℤ n) 
        reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
      
      axiom wcsncmp_zero{L}:
        ∀ wchar_t *s1, wchar_t *s2;
        ∀ ℤ n;
          wcsncmp(s1, s2, n) ≡ 0 ⇔
          (wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
          (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
      
      }
     */
    /*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
     */
    /*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
     */
    /*@
    predicate valid_string{L}(char *s) =
      0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
     */
    /*@
    predicate valid_read_string{L}(char *s) =
      0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
     */
    /*@
    predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
     */
    /*@
    predicate valid_wstring{L}(wchar_t *s) =
      0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
     */
    /*@
    predicate valid_wstring_or_null{L}(wchar_t *s) =
      s ≡ \null ∨ valid_wstring(s);
     */
    extern int printf(char const *format , ...);
    
    static uint32_t crc32_tab[256];
    static uint32_t crc32_context = (unsigned int)0xFFFFFFFFUL;
    static void crc32_gentab(void)
    {
      uint32_t crc;
      uint32_t poly;
      int i;
      int j;
      poly = (unsigned int)0xEDB88320UL;
      i = 0;
      while (i < 256) {
        crc = (unsigned int)i;
        j = 8;
        while (j > 0) {
          if (crc & (unsigned int)1) crc = (crc >> 1) ^ poly; else crc >>= 1;
          j --;
        }
        crc32_tab[i] = crc;
        i ++;
      }
      return;
    }
    
    static void transparent_crc(uint64_t val)
    {
      uint8_t b = (unsigned char)((val >> 0) & (unsigned long long)0xff);
      crc32_context = ((crc32_context >> 8) & (unsigned int)0x00FFFFFF) ^ crc32_tab[
                      (crc32_context ^ (unsigned int)b) & (unsigned int)0xFF];
      return;
    }
    
    static int32_t g_58 = (int)0x232038BEL;
    static int32_t const g_79 = (int)0x92FD4AE7L;
    static void func_1(void);
    
    static int32_t func_2(void);
    
    static void func_1(void)
    {
      int32_t *l_85;
      l_85 = & g_58;
      *l_85 = func_2();
      return;
    }
    
    static int32_t func_2(void)
    {
      return g_79;
    }
    
    void main(void)
    {
      crc32_gentab();
      func_1();
      transparent_crc((unsigned long long)g_58);
      transparent_crc((unsigned long long)g_79);
      /*@ slice pragma stmt; */
      printf("%X\n",crc32_context);
      return;
    }
    
    
    
    c file icon test.c (8,061 bytes) 2017-05-23 10:16 +

-Relationships
+Relationships

-Notes

~0006476

Yangyibiao (reporter)

Note that this bug has been fixed in frama-c Sulfur-20171101.
+Notes

-Issue History
Date Modified Username Field Change
2017-05-23 10:16 Yangyibiao New Issue
2017-05-23 10:16 Yangyibiao Status new => assigned
2017-05-23 10:16 Yangyibiao Assigned To => Nikolai_Kosmatov
2017-05-23 10:16 Yangyibiao File Added: test.c
2017-12-05 07:09 Yangyibiao Tag Attached: csmith
2017-12-05 07:10 Yangyibiao Note Added: 0006476
2017-12-06 09:12 signoles Status assigned => closed
2017-12-06 09:12 signoles Resolution open => fixed
2017-12-06 09:12 signoles Fixed in Version => Frama-C 16-Sulfur
+Issue History