[ioccc] add 2020 IOCCC winners

ioccc/.frama-c/2020_kurdyukov3_prog_orig.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "signal.h"
+#include "stdarg.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "time.h"
+int main(void)
+{
+  int __retres;
+  unsigned int i;
+  unsigned int j;
+  unsigned int t[64];
+  time_t tmp;
+  unsigned int a = (unsigned int)0;
+  tmp = time((time_t *)0);
+  srand((unsigned int)tmp);
+  while (~ a >> 8) {
+    j = (unsigned int)0;
+    i = j;
+    while (1) {
+      int tmp_1;
+      int tmp_2;
+      unsigned int tmp_0;
+      tmp_1 = getchar();
+      a = (unsigned int)tmp_1;
+      if (~ i >> 6) 
+        if (a >> 7 == (unsigned int)1) tmp_2 = 1;
+        else 
+          if ((a | (unsigned int)32) - (unsigned int)97 < (unsigned int)26) 
+            tmp_2 = 1;
+          else tmp_2 = 0;
+      else tmp_2 = 0;
+      if (! tmp_2) break;
+      tmp_0 = i;
+      i ++;
+      t[tmp_0] = a;
+    }
+    i --;
+    while (i + (unsigned int)1) {
+      unsigned int tmp_4;
+      putchar((int)t[j]);
+      tmp_4 = i;
+      i --;
+      t[j] = t[tmp_4];
+      if (i) {
+        int tmp_3;
+        tmp_3 = rand();
+        j = (unsigned int)tmp_3 % i + (unsigned int)1;
+      }
+      else j = (unsigned int)0;
+    }
+    if (! (a >> 8)) putchar((int)a);
+  }
+  __retres = 0;
+  return __retres;
+}
+
+

ioccc/.frama-c/2020_kurdyukov3_prog_orig.parse/metrics.log

+[metrics] Defined functions (1)
+=====================
+ main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 45
+Decision point = 8
+Global variables = 0
+If = 8
+Loop = 3
+Goto = 0
+Assignment = 21
+Exit point = 1
+Function = 1
+Function call = 6
+Pointer dereferencing = 0
+Cyclomatic complexity = 9

ioccc/.frama-c/2020_kurdyukov4_prog.eva/alarms.csv

+directory	file	line	function	property kind	status	property
+2020/kurdyukov4	prog.c	9	main	signed_overflow	Unknown	c + 1 ≤ 2147483647
+2020/kurdyukov4	prog.c	9	main	mem_access	Invalid or unreachable	\valid_read(V + 2)
+FRAMAC_SHARE/libc	stdlib.h	78	atoi	precondition	Unknown	valid_nptr: \valid_read(nptr)

ioccc/.frama-c/2020_kurdyukov4_prog.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+190 stmts in analyzed functions, 12 stmts analyzed (6.3%)
+main: 12 stmts out of 190 (6.3%)

ioccc/.frama-c/2020_kurdyukov4_prog.eva/nonterm.log

+2020/kurdyukov4/prog.c:9:[nonterm] warning: non-terminating function call
+stack: main

ioccc/.frama-c/2020_kurdyukov4_prog.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+int main(int c, char **V)
+{
+  int __retres;
+  int k;
+  int l;
+  int p;
+  int i;
+  int x;
+  int y;
+  int n;
+  int q;
+  uint64_t s;
+  uint64_t z;
+  uint32_t *h;
+  uint32_t a;
+  uint32_t t[512];
+  uint64_t S = (unsigned long)5;
+  while (1) {
+    int tmp_14;
+    tmp_14 = c;
+    c ++;
+    ;
+    if (! (tmp_14 == 5)) break;
+    {
+      uint8_t *m;
+      void *F;
+      int tmp;
+      x = atoi((char const *)*(V + 2));
+      y = atoi((char const *)*(V + 3));
+      tmp = atoi((char const *)*(V + 4));
+      s = (unsigned long)tmp;
+      if (x >> 20) break;
+      else 
+        if ((y - 1) >> 7) break;
+        else {
+          q = 1;
+          ;
+          F = (void *)fopen((char const *)*(V + q),"rb");
+          if (F) {
+            int tmp_0;
+            tmp_0 = fseek((FILE *)F,(long)0,2);
+            if (tmp_0) break;
+            else {
+              long tmp_1;
+              tmp_1 = ftell((FILE *)F);
+              n = (int)tmp_1;
+              ;
+              if (y > n) break;
+              else {
+                int tmp_2;
+                tmp_2 = fseek((FILE *)F,(long)0,0);
+                if (tmp_2) break;
+                else {
+                  m = (uint8_t *)malloc((unsigned long)(n + y));
+                  if (m) {
+                    size_t tmp_3;
+                    tmp_3 = fread((void *)m,(unsigned long)1,
+                                  (unsigned long)n,(FILE *)F);
+                    ;
+                    if (tmp_3 - (size_t)n) break;
+                    else 
+                      if (n >> 29) break;
+                  }
+                  else break;
+                }
+              }
+            }
+          }
+          else break;
+        }
+      fclose((FILE *)F);
+      while (S * (uint64_t)5 > S) S *= (uint64_t)5;
+      l = 0;
+      k = l;
+      i = k;
+      while (i < n) {
+        int tmp_6;
+        tmp_6 = i;
+        i ++;
+        a = (unsigned int)*(m + tmp_6);
+        if ((uint32_t)'_' - a) {
+          if (a == (uint32_t)'<') {
+            a = (unsigned int)' ';
+            while (1) 
+              if (i < n) {
+                int tmp_4;
+                tmp_4 = i;
+                i ++;
+                ;
+                if (! ((int)*(m + tmp_4) - '>')) break;
+              }
+              else break;
+          }
+          if (a - (uint32_t)' ') {
+            if (a - (uint32_t)'\n') {
+              if (a - (uint32_t)'\r') {
+                if (a - (uint32_t)'\t') goto _LOR; else goto _LAND_1;
+              }
+              else goto _LAND_1;
+            }
+            else goto _LAND_1;
+          }
+          else {
+            _LAND_1: { /* sequence */
+                       a = (unsigned int)' ';
+                       ;
+                     }
+            if ((uint32_t)k - a) {
+              int tmp_5;
+              _LOR:
+              { /* sequence */
+                tmp_5 = l;
+                l ++;
+                k = (int)a;
+                *(m + tmp_5) = (unsigned char)k;
+              }
+            }
+          }
+        }
+      }
+      n = l;
+      memcpy((void *)(m + l),(void const *)m,(unsigned long)y);
+      while (l * 3 > q) q += q;
+      h = (uint32_t *)malloc((unsigned long)(4 * q));
+      if (h) {
+        int tmp_7;
+        tmp_7 = q;
+        q --;
+        ;
+        ;
+        memset((void *)h,-1,(unsigned long)(4 * tmp_7));
+        k = 0;
+        while (k < l) {
+          int tmp_8;
+          i = 0;
+          a = (unsigned int)i;
+          while (i < y) {
+            int tmp_9;
+            tmp_9 = i;
+            i ++;
+            a = (a ^ (unsigned int)*(m + (k + tmp_9))) * (unsigned int)79764919;
+          }
+          while (1) {
+            i = (int)*(h + (a & (unsigned int)q));
+            if (! (i ^ -1)) break;
+            a += (uint32_t)1;
+          }
+          tmp_8 = k;
+          k ++;
+          *(h + (a & (unsigned int)q)) = (unsigned int)tmp_8;
+        }
+        s *= S;
+        a = (unsigned int)(s >> 31);
+        z = (unsigned long)a;
+        p = (int)(z * (uint64_t)n >> 32);
+        while (1) {
+          int tmp_13;
+          tmp_13 = x;
+          x --;
+          ;
+          if (! tmp_13) break;
+          n = 0;
+          memset((void *)(t),n,(unsigned long)(8 << 8));
+          i = 0;
+          a = (unsigned int)i;
+          while (i < y) {
+            int tmp_10;
+            tmp_10 = i;
+            i ++;
+            a = (a ^ (unsigned int)*(m + (p + tmp_10))) * (unsigned int)79764919;
+          }
+          while (1) {
+            int tmp_12;
+            i = (int)*(h + (a & (unsigned int)q));
+            if (! (i ^ -1)) break;
+            tmp_12 = memcmp((void const *)(m + p),(void const *)(m + i),
+                            (unsigned long)y);
+            if (! tmp_12) {
+              int tmp_11;
+              k = (int)*(m + (i + y)) * 2;
+              tmp_11 = k;
+              k ++;
+              t[tmp_11] += (uint32_t)1;
+              n ++;
+              t[k] = (unsigned int)i;
+            }
+            a += (uint32_t)1;
+          }
+          s *= S;
+          a = (unsigned int)(s >> 31);
+          z = (unsigned long)a;
+          n = (int)(z * (uint64_t)n >> 32);
+          k = -1;
+          while (n >= 0) {
+            k ++;
+            n = (int)((uint32_t)n - t[k * 2]);
+          }
+          putchar(k);
+          p = (int)(t[(k + k) + 1] + (uint32_t)1);
+          if (p - l) p = p; else p = 0;
+        }
+        putchar('\n');
+        c = 0;
+      }
+    }
+  }
+  __retres = ! (! c);
+  return __retres;
+}
+
+

ioccc/.frama-c/2020_kurdyukov4_prog.parse/metrics.log

+[metrics] Defined functions (1)
+=====================
+ main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 190
+Decision point = 32
+Global variables = 0
+If = 32
+Loop = 12
+Goto = 4
+Assignment = 79
+Exit point = 1
+Function = 1
+Function call = 17
+Pointer dereferencing = 13
+Cyclomatic complexity = 33

ioccc/.frama-c/2020_kurdyukov4_prog.parse/warnings.log

+2020/kurdyukov4/prog.c:13:[kernel:typing:implicit-conv-void-ptr] warning: implicit conversion from void * to FILE *
+2020/kurdyukov4/prog.c:13:[kernel:typing:implicit-conv-void-ptr] warning: implicit conversion from void * to FILE *
+2020/kurdyukov4/prog.c:14:[kernel:typing:implicit-conv-void-ptr] warning: implicit conversion from void * to FILE *
+2020/kurdyukov4/prog.c:14:[kernel:typing:implicit-conv-void-ptr] warning: implicit conversion from void * to FILE *
+2020/kurdyukov4/prog.c:15:[kernel:typing:implicit-conv-void-ptr] warning: implicit conversion from void * to FILE *

ioccc/.frama-c/2020_otterness_prog.eva/alarms.csv

+directory	file	line	function	property kind	status	property
+2020/otterness	prog.c	12	A	initialization	Unknown	\initialized(c + (int)(!(c ≢ \null)? 0: 1))
+2020/otterness	prog.c	12	A	initialization	Unknown	\initialized(c)
+2020/otterness	prog.c	12	A	mem_access	Unknown	\valid_read(c + (int)(!(c ≢ \null)? 0: 1))
+2020/otterness	prog.c	12	A	mem_access	Unknown	\valid_read(c)
+2020/otterness	prog.c	12	A	ptr_comparison	Unknown	\pointer_comparable((void *)0, (void *)c)
+2020/otterness	prog.c	12	A	signed_overflow	Unknown	(int)((unsigned short)*c) << l ≤ 2147483647
+2020/otterness	prog.c	15	B	mem_access	Unknown	\valid(tmp)
+2020/otterness	prog.c	15	B	shift	Unknown	0 ≤ l < 32
+2020/otterness	prog.c	16	B	mem_access	Unknown	\valid(c)
+2020/otterness	prog.c	24	C	initialization	Unknown	\initialized(c + d)
+2020/otterness	prog.c	24	C	mem_access	Unknown	\valid_read(c + d)
+2020/otterness	prog.c	26	C	shift	Unknown	0 ≤ l < 32
+2020/otterness	prog.c	45	D	division_by_zero	Unknown	(int)c ≢ 0
+2020/otterness	prog.c	50	F	mem_access	Unknown	\valid(c)
+2020/otterness	prog.c	51	F	division_by_zero	Unknown	n ≢ 0
+2020/otterness	prog.c	57	F	mem_access	Unknown	\valid(c)
+2020/otterness	prog.c	58	F	shift	Unknown	0 ≤ l < 32
+2020/otterness	prog.c	68	G	signed_overflow	Unknown	(int)p << (int)q ≤ 2147483647
+2020/otterness	prog.c	68	G	shift	Unknown	0 ≤ (int)q < 32
+2020/otterness	prog.c	70	G	initialization	Unknown	\initialized(c)
+2020/otterness	prog.c	70	G	mem_access	Unknown	\valid_read(c)
+2020/otterness	prog.c	84	G	division_by_zero	Unknown	(unsigned int)o ≢ 0
+2020/otterness	prog.c	85	G	shift	Unknown	0 ≤ (int)q < 32
+2020/otterness	prog.c	104	H	division_by_zero	Unknown	n ≢ 0
+2020/otterness	prog.c	105	H	division_by_zero	Unknown	(int)m ≢ 0
+2020/otterness	prog.c	106	H	initialization	Unknown	\initialized(c + n)
+2020/otterness	prog.c	106	H	mem_access	Unknown	\valid_read(c + n)
+2020/otterness	prog.c	107	H	shift	Unknown	0 ≤ (int)((int)q * (int)q) < 32
+2020/otterness	prog.c	107	H	shift	Unknown	0 ≤ (int)q < 32
+2020/otterness	prog.c	110	H	ptr_comparison	Unknown	\pointer_comparable((void *)c, (void *)d)
+2020/otterness	prog.c	132	J	signed_overflow	Unknown	(int)((int)s - (int)o) << (int)r ≤ 2147483647
+2020/otterness	prog.c	132	J	shift	Unknown	0 ≤ (int)((int)s - (int)o)
+2020/otterness	prog.c	132	J	shift	Unknown	0 ≤ (int)r < 32
+2020/otterness	prog.c	133	J	division_by_zero	Unknown	(int)((int)s + (int)o) ≢ 0
+2020/otterness	prog.c	134	J	division_by_zero	Unknown	l ≢ 0
+2020/otterness	prog.c	135	J	division_by_zero	Unknown	(unsigned int)r ≢ 0
+2020/otterness	prog.c	136	J	division_by_zero	Unknown	n ≢ 0
+2020/otterness	prog.c	140	J	division_by_zero	Unknown	(unsigned int)m ≢ 0
+2020/otterness	prog.c	147	J	mem_access	Unknown	\valid(t + k)
+2020/otterness	prog.c	148	J	mem_access	Unknown	\valid(t + r)
+2020/otterness	prog.c	149	J	mem_access	Unknown	\valid(u)
+2020/otterness	prog.c	150	J	precondition of memcpy	Unknown	valid_dest: valid_or_empty(dest, n)
+2020/otterness	prog.c	150	J	precondition of memcpy	Unknown	valid_src: valid_read_or_empty(src, n)
+2020/otterness	prog.c	166	K	shift	Unknown	0 ≤ (int)tmp_3 < 32
+2020/otterness	prog.c	167	K	division_by_zero	Unknown	(unsigned int)e ≢ 0
+2020/otterness	prog.c	175	K	mem_access	Unknown	\valid(b)
+2020/otterness	prog.c	176	K	mem_access	Unknown	\valid(b + (int)(k ≢ 0? 0: 1))
+2020/otterness	prog.c	176	K	mem_access	Unknown	\valid_read(b)
+2020/otterness	prog.c	177	K	mem_access	Unknown	\valid(b + n)
+2020/otterness	prog.c	178	K	initialization	Unknown	\initialized(b + n)
+2020/otterness	prog.c	178	K	mem_access	Unknown	\valid(b + o)
+2020/otterness	prog.c	178	K	mem_access	Unknown	\valid_read(b + n)
+2020/otterness	prog.c	180	K	shift	Unknown	0 ≤ (unsigned int)((unsigned int)o * l) < 32
+2020/otterness	prog.c	182	K	mem_access	Unknown	\valid(tmp_8)
+2020/otterness	prog.c	183	K	mem_access	Unknown	\valid(tmp_9)
+2020/otterness	prog.c	184	K	division_by_zero	Unknown	(unsigned int)(n + (unsigned int)o) ≢ 0
+2020/otterness	prog.c	185	K	mem_access	Unknown	\valid(tmp_10)
+2020/otterness	prog.c	188	K	mem_access	Unknown	\valid(tmp_12)
+2020/otterness	prog.c	189	K	mem_access	Unknown	\valid(d)
+2020/otterness	prog.c	191	K	mem_access	Unknown	\valid(tmp_13)
+2020/otterness	prog.c	192	K	mem_access	Unknown	\valid(tmp_15)
+2020/otterness	prog.c	193	K	precondition of memcpy	Unknown	valid_dest: valid_or_empty(dest, n)
+2020/otterness	prog.c	193	K	precondition of memcpy	Unknown	valid_src: valid_read_or_empty(src, n)
+2020/otterness	prog.c	196	K	division_by_zero	Unknown	(int)s ≢ 0
+2020/otterness	prog.c	198	K	mem_access	Unknown	\valid(tmp_16)
+2020/otterness	prog.c	199	K	mem_access	Unknown	\valid(tmp_17)
+2020/otterness	prog.c	200	K	mem_access	Unknown	\valid(tmp_18)
+2020/otterness	prog.c	201	K	mem_access	Unknown	\valid(d)
+2020/otterness	prog.c	202	K	mem_access	Unknown	\valid(c + (unsigned int)(l + (unsigned int)p))
+2020/otterness	prog.c	204	K	precondition of fwrite	Unknown	valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1))
+2020/otterness	prog.c	204	K	precondition of fwrite	Unknown	valid_stream: \valid(stream)
+2020/otterness	prog.c	205	K	precondition of fwrite	Unknown	valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1))
+2020/otterness	prog.c	205	K	precondition of fwrite	Unknown	valid_stream: \valid(stream)
+2020/otterness	prog.c	219	main	precondition of fread	Unknown	valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
+2020/otterness	prog.c	219	main	precondition of fread	Unknown	valid_stream: \valid(stream)
+2020/otterness	prog.c	221	main	division_by_zero	Unknown	n ≢ 0
+2020/otterness	prog.c	222	main	initialization	Unknown	\initialized(c + n)
+2020/otterness	prog.c	222	main	mem_access	Unknown	\valid_read(c + n)
+2020/otterness	prog.c	222	main	initialization	Unknown	\initialized(c + (unsigned int)((unsigned int)m - k))
+2020/otterness	prog.c	222	main	mem_access	Unknown	\valid_read(c + (unsigned int)((unsigned int)m - k))
+FRAMAC_SHARE/libc	stdio.h	351	fread	precondition	Unknown	valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
+FRAMAC_SHARE/libc	stdio.h	352	fread	precondition	Unknown	valid_stream: \valid(stream)
+FRAMAC_SHARE/libc	stdio.h	364	fwrite	precondition	Unknown	valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1))
+FRAMAC_SHARE/libc	stdio.h	365	fwrite	precondition	Unknown	valid_stream: \valid(stream)
+FRAMAC_SHARE/libc	string.h	92	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	93	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)

ioccc/.frama-c/2020_otterness_prog.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 11 (out of 11)
+Semantically reached functions = 11
+Coverage estimation = 100.0%
+[metrics] Statements analyzed by Eva
+--------------------------
+328 stmts in analyzed functions, 324 stmts analyzed (98.8%)
+A: 2 stmts out of 2 (100.0%)
+B: 6 stmts out of 6 (100.0%)
+D: 17 stmts out of 17 (100.0%)
+G: 47 stmts out of 47 (100.0%)
+H: 26 stmts out of 26 (100.0%)
+I: 11 stmts out of 11 (100.0%)
+J: 22 stmts out of 22 (100.0%)
+K: 122 stmts out of 122 (100.0%)
+main: 22 stmts out of 22 (100.0%)
+C: 28 stmts out of 29 (96.6%)
+F: 21 stmts out of 24 (87.5%)

ioccc/.frama-c/2020_otterness_prog.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+typedef uint8_t u1;
+typedef uint16_t u2;
+typedef uint32_t u4;
+u4 k;
+u4 l;
+u4 n;
+u1 m;
+u1 o;
+u1 p;
+u1 q;
+u1 r;
+u1 s;
+u1 *t;
+u1 *u;
+u2 A(u1 *c)
+{
+  u2 __retres;
+  __retres = (unsigned short)((int)*(c + ! (! c)) | ((int)((unsigned short)*c) << l));
+  return __retres;
+}
+
+void B(u1 *c, u2 a)
+{
+  u1 *tmp;
+  tmp = c;
+  c ++;
+  *tmp = (unsigned char)((int)a >> l);
+  *c = (unsigned char)a;
+  return;
+}
+
+int C(u1 *c, u4 *a)
+{
+  int __retres;
+  u1 b;
+  u4 tmp;
+  u4 tmp_0;
+  u1 d = (unsigned char)k;
+  tmp = l;
+  l -= (u4)1;
+  s = (unsigned char)tmp;
+  tmp_0 = k;
+  k += (u4)1;
+  *a = tmp_0;
+  while ((int)d < (int)s >> k) {
+    b = *(c + d);
+    *a |= (unsigned int)((int)b & (int)p);
+    if (! ((int)b >> l)) {
+      u4 tmp_1;
+      tmp_1 = k;
+      k -= (u4)1;
+      d = (unsigned char)((u4)d + tmp_1);
+      l = (unsigned int)s;
+      __retres = (int)d;
+      goto return_label;
+    }
+    *a <<= l;
+    d = (unsigned char)((int)d + 1);
+  }
+  exit(! k);
+  __retres = (int)p;
+  return_label: return __retres;
+}
+
+u1 D(u4 a)
+{
+  u1 __retres;
+  u4 tmp;
+  tmp = k;
+  k += (u4)1;
+  u1 b = (unsigned char)tmp;
+  u1 c = (unsigned char)(l - k);
+  if (a) {
+    b = (unsigned char)k;
+    while (1) {
+      a >>= k;
+      if (! a) break;
+      b = (unsigned char)((int)b + 1);
+    }
+  }
+  if (k) k = (unsigned int)(! k); else k = k;
+  __retres = (unsigned char)((int)b / (int)c + ! (! ((int)b % (int)c)));
+  return __retres;
+}
+
+int F(u4 a, u1 *c)
+{
+  int __retres;
+  u4 tmp_0;
+  u1 b = D(a);
+  tmp_0 = l;
+  l -= (u4)1;
+  *c = (unsigned char)((u4)s - tmp_0);
+  r = (unsigned char)((u4)q / n);
+  if (! a) {
+    __retres = (int)b;
+    goto return_label;
+  }
+  if ((int)b > (int)r) exit((int)o);
+  c += (int)b;
+  c --;
+  while (a) {
+    *c = (unsigned char)(a & (unsigned int)p);
+    a >>= l;
+    c --;
+  }
+  l = (unsigned int)s;
+  __retres = (int)b;
+  return_label: return __retres;
+}
+
+u1 *G(u1 *c, u1 *a)
+{
+  u1 *__retres;
+  u4 d;
+  u1 b;
+  u1 e;
+  if ((int)m < (int)p) m = (unsigned char)((int)p << (int)q); else m = m;
+  if ((u4)q < n + (u4)o) q = (unsigned char)((int)p >> (int)q); else 
+                                                                  q = q;
+  e = *c;
+  if ((int)e == (int)m) goto _LOR;
+  else 
+    if ((int)e == (int)m + (int)q) {
+      _LOR:
+      {
+        int tmp;
+        *a = (unsigned char)k;
+        c ++;
+        tmp = C(c,& d);
+        c += tmp;
+        __retres = c + d;
+        goto return_label;
+      }
+    }
+  if ((int)e == ((int)m | (int)p)) {
+    int tmp_0;
+    *a = (unsigned char)k;
+    c ++;
+    c ++;
+    tmp_0 = C(c,& d);
+    c += tmp_0;
+    __retres = c + d;
+    goto return_label;
+  }
+  l /= (u4)o;
+  if ((int)e >> (int)q) {
+    b = *c;
+    c ++;
+    *a = b;
+  }
+  else b = *a;
+  e = (unsigned char)((int)b >> l);
+  if ((int)e < (int)s) exit((int)n);
+  else 
+    if ((u4)e > l + (u4)s) exit((int)n);
+  if ((u4)e != l + (u4)s) 
+    if ((u4)e != l + (u4)o) c ++;
+  c ++;
+  l = (unsigned int)s;
+  __retres = c;
+  return_label: return __retres;
+}
+
+u1 *H(u1 *c, u4 *a)
+{
+  u4 b;
+  u4 e;
+  u1 *d;
+  u2 tmp;
+  u2 tmp_0;
+  u4 h = (unsigned int)q;
+  u4 i = (unsigned int)m;
+  u1 f = (unsigned char)k;
+  *a = k;
+  q = (unsigned char)((u4)q / n);
+  m = (unsigned char)(((int)p - (int)m) + (int)p / (int)m);
+  if ((int)*(c + n) != (int)m) exit((int)q);
+  tmp = A(c + (int)q);
+  tmp_0 = A(c + ((int)m >> (int)q));
+  b = ((unsigned int)tmp << (int)q * (int)q) | (unsigned int)tmp_0;
+  c += l;
+  d = c + b;
+  while (c < d) {
+    int tmp_1;
+    tmp_1 = C(c,& e);
+    c += tmp_1;
+    *a += e;
+    c = G(c,& f);
+  }
+  q = (unsigned char)h;
+  m = (unsigned char)i;
+  return c;
+}
+
+u4 I(u1 *c, u4 a)
+{
+  u4 e;
+  u4 b;
+  u4 d = k;
+  e = k;
+  while (e < a) {
+    c = H(c,& b);
+    if (b > d) d = b;
+    e += (u4)1;
+  }
+  return d;
+}
+
+u1 *J(u1 *c, u4 a, u4 b)
+{
+  u1 *__retres;
+  u1 d;
+  u1 e;
+  if (l > (u4)o) {
+    s = (unsigned char)((int)s - 1);
+    o = (unsigned char)(((int)s - (int)o) << (int)r);
+    l = (unsigned int)((int)p % ((int)s + (int)o));
+    r = (unsigned char)((u4)o / l);
+    n = l / (u4)r;
+    m = (unsigned char)((u4)o / n);
+  }
+  d = (unsigned char)(l + (u4)r);
+  e = o;
+  if (! (a % (unsigned int)m)) {
+    d = (unsigned char)(l - (u4)m);
+    e = (unsigned char)((u4)o + l);
+  }
+  else 
+    if (a % (unsigned int)m == (unsigned int)r) {
+      d = (unsigned char)l;
+      e = (unsigned char)(n + (u4)o);
+    }
+  *(t + k) = d;
+  *(t + r) = e;
+  *u = d;
+  memcpy((void *)c,(void const *)t,(unsigned long)b);
+  __retres = c + b;
+  return __retres;
+}
+
+void K(u1 *c, u4 a)
+{
+  u1 *b;
+  u1 *d;
+  u2 e;
+  u2 f;
+  u4 g;
+  u4 h;
+  u4 i;
+  u4 j;
+  u2 tmp;
+  u4 tmp_0;
+  u4 tmp_1;
+  u4 tmp_2;
+  u1 tmp_3;
+  u4 tmp_5;
+  u1 tmp_4;
+  u1 tmp_6;
+  u1 tmp_7;
+  u1 *tmp_8;
+  u1 *tmp_9;
+  u1 *tmp_10;
+  int tmp_11;
+  u1 *tmp_12;
+  u1 *tmp_13;
+  u4 tmp_14;
+  u1 *tmp_15;
+  u1 *tmp_16;
+  u1 *tmp_17;
+  u1 *tmp_18;
+  u4 tmp_19;
+  o = (unsigned char)(n ^ k);
+  m = (unsigned char)l;
+  l = (unsigned int)((int)o << (int)o);
+  f = A((c + l) + (int)o);
+  tmp = A(((c + l) + (int)o) + (int)o);
+  tmp_0 = k;
+  k -= (u4)1;
+  e = (unsigned short)((int)tmp >> tmp_0);
+  tmp_1 = k;
+  k += (u4)1;
+  p = (unsigned char)(~ tmp_1);
+  tmp_2 = k;
+  k -= (u4)1;
+  p = (unsigned char)((int)p >> tmp_2);
+  q = (unsigned char)((int)p >> n);
+  tmp_3 = q;
+  q = (unsigned char)((int)q - 1);
+  ;
+  if ((int)e >> (int)tmp_3) exit((int)(n + (u4)o));
+  ;
+  tmp_4 = q;
+  q = (unsigned char)((int)q - 1);
+  ;
+  tmp_5 = I(c + (int)tmp_4,(unsigned int)f);
+  g = tmp_5 / (u4)e;
+  tmp_6 = D((unsigned int)e);
+  i = (n + (u4)o) + (u4)tmp_6;
+  t = (u1 *)malloc((unsigned long)i);
+  if (! t) exit((int)(n * (u4)o));
+  j = g * i + (u4)q;
+  b = (u1 *)malloc((unsigned long)j);
+  l -= (u4)1;
+  r = (unsigned char)l;
+  l += (u4)1;
+  if (! b) exit((int)r);
+  *b = (unsigned char)((l << n) | (unsigned int)q);
+  *(b + ! k) = (unsigned char)((int)*b + (int)r);
+  *(b + n) = (unsigned char)((u4)((int)*b << n) + n);
+  tmp_7 = r;
+  r = (unsigned char)((int)r - 1);
+  *(b + o) = (unsigned char)((int)*(b + n) + (int)tmp_7);
+  B(b + n * (u4)o,(unsigned short)(j - l));
+  B(b + (int)o * (int)o,(unsigned short)((j - l) >> (u4)o * l));
+  d = t;
+  tmp_8 = d;
+  d ++;
+  *tmp_8 = (unsigned char)k;
+  tmp_9 = d;
+  d ++;
+  *tmp_9 = (unsigned char)((int)r * (int)r);
+  m = (unsigned char)((u4)p / (n + (u4)o));
+  tmp_10 = d;
+  d ++;
+  *tmp_10 = (unsigned char)(((int)p - (int)m) - (int)o);
+  tmp_11 = F((unsigned int)e,d);
+  d += tmp_11;
+  u = d;
+  tmp_12 = d;
+  d ++;
+  *tmp_12 = (unsigned char)((int)r * (int)r);
+  *d = (unsigned char)k;
+  d = b + l;
+  tmp_13 = d;
+  d ++;
+  tmp_14 = k;
+  k += (u4)1;
+  *tmp_13 = (unsigned char)tmp_14;
+  tmp_15 = d;
+  d ++;
+  *tmp_15 = (unsigned char)(((int)p + (int)q) + (int)q);
+  memcpy((void *)d,(void const *)(t + k),(unsigned long)(i - k));
+  d += i - k;
+  h = k;
+  while (h < g) {
+    d = J(d,h,i);
+    h += (u4)1;
+  }
+  l = (unsigned int)(((int)o + (int)m) / (int)s - (int)m);
+  o = r;
+  tmp_16 = d;
+  d ++;
+  k -= (u4)1;
+  *tmp_16 = (unsigned char)k;
+  tmp_17 = d;
+  d ++;
+  *tmp_17 = (unsigned char)(~ k);
+  tmp_18 = d;
+  d ++;
+  *tmp_18 = (unsigned char)((u4)((int)p / (int)o) - (u4)o * l);
+  tmp_19 = k;
+  k += (u4)1;
+  *d = (unsigned char)tmp_19;
+  *(c + (l + (u4)p)) = (unsigned char)k;
+  B((c + l) + (int)o,(unsigned short)((u4)f + k));
+  fwrite((void const *)c,(unsigned long)a,(unsigned long)(! (! c)),
+         __fc_stdout);
+  fwrite((void const *)b,(unsigned long)j,(unsigned long)(! (! b)),
+         __fc_stdout);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  u4 a;
+  u4 b;
+  u1 *c;
+  size_t tmp;
+  k = (unsigned int)(! (! __fc_stdin));
+  n = (k + k) + k;
+  l = k << n;
+  m = (unsigned char)l;
+  l = (l | (l >> (k + k))) << k;
+  b = k << l;
+  c = (u1 *)malloc((unsigned long)b);
+  if (! c) exit((int)m);
+  tmp = fread((void *)c,(unsigned long)k,(unsigned long)b,__fc_stdin);
+  a = (unsigned int)tmp;
+  l = (u4)(((int)m << k) + (int)m) + k;
+  if (a >= b) exit((int)(l / n + k));
+  if ((u4)*(c + n) != l << (k + k)) exit((int)((u4)((int)m << k) - (n << k)));
+  else 
+    if ((u4)*(c + ((u4)m - k)) != n + n) exit((int)((u4)((int)m << k) - (
+                                                    n << k)));
+  K(c,a);
+  __retres = ! b;
+  return __retres;
+}
+
+

ioccc/.frama-c/2020_otterness_prog.parse/metrics.log

+[metrics] Defined functions (11)
+======================
+ A (4 calls); B (3 calls); C (3 calls); D (2 calls); F (1 call); G (1 call);
+ H (1 call); I (1 call); J (1 call); K (1 call); main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 328
+Decision point = 33
+Global variables = 11
+If = 33
+Loop = 6
+Goto = 5
+Assignment = 202
+Exit point = 11
+Function = 11
+Function call = 38
+Pointer dereferencing = 46
+Cyclomatic complexity = 44

ioccc/.frama-c/GNUmakefile

+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
+
+### Prologue. Do not modify this block. #######################################
+-include path.mk
+FRAMAC ?= frama-c
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
+###############################################################################
+
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+
+MACHDEP = x86_64
+
+## Preprocessing flags (for -cpp-extra-args)
+CPPFLAGS    += \
+
+## General flags
+FCFLAGS     += \
+  -add-symbolic-path=..:. \
+  -kernel-warn-key annot:missing-spec=abort \
+  -kernel-warn-key typing:implicit-function-declaration=abort \
+
+## Eva-specific flags
+EVAFLAGS    += \
+  -eva-warn-key builtins:missing-spec=abort \
+
+## GUI-only flags
+FCGUIFLAGS += \
+
+## Analysis targets (suffixed with .eva)
+TARGETS = \
+2020_burton_prog.eva \
+2020_giles_prog.eva \
+2020_kurdyukov1_prog.eva \
+2020_kurdyukov1_prog_extra.eva \
+2020_kurdyukov1_prog_orig.eva \
+2020_kurdyukov2_prog_ppm.eva \
+2020_kurdyukov3_prog.eva \
+2020_kurdyukov3_prog_extra.eva \
+2020_kurdyukov3_prog_orig.eva \
+2020_kurdyukov4_prog.eva \
+2020_otterness_prog.eva \
+
+#### The folowing cases are not currently handled by Frama-C;
+#### See comments in .parse lines
+
+NOT_HANDLED=\
+2020_carlini_prog.eva \
+2020_endoh1_prog.eva \
+2020_endoh1_prog_orig.eva \
+2020_endoh2_prog.eva \
+2020_endoh3_clock.eva \
+2020_endoh3_prog.eva \
+2020_endoh3_prog_alt.eva \
+2020_ferguson1_termcaps.eva \
+2020_ferguson1_prog_3.eva \
+2020_ferguson1_prog.eva \
+2020_ferguson1_prog_2.eva \
+2020_ferguson1_prog_alt.eva \
+2020_ferguson1_prog_3-j.eva \
+2020_ferguson2_prog.eva \
+2020_ferguson2_recode.eva \
+2020_kurdyukov2_prog.eva \
+2020_kurdyukov2_prog_png.eva \
+2020_kurdyukov4_rand.eva \
+2020_tsoj_prog.eva \
+2020_yang_prog.eva \
+
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+
+2020_burton_prog.parse: ../2020/burton/prog.c
+2020_burton_prog.parse: FCFLAGS += -json-compilation-database ../2020/burton \
+
+#2020_carlini_prog.parse: ../2020/carlini/prog.c #  missing spec for scanf with non-static format argument
+#2020_carlini_prog.parse: FCFLAGS += -json-compilation-database ../2020/carlini \
+
+#2020_endoh1_prog.parse: ../2020/endoh1/prog.c # requires <ncurses.h>
+
+#2020_endoh1_prog_orig.parse: ../2020/endoh1/prog_orig.c # requires <ncurses.h>
+
+#2020_endoh2_prog.parse: ../2020/endoh2/prog.c # requires <complex.h>
+
+#2020_endoh3_clock.parse: ../2020/endoh3/clock.c # parsing issue with comment/slash
+
+#2020_endoh3_prog.parse: ../2020/endoh3/prog.c # parsing issue with comment/slash
+
+#2020_endoh3_prog_alt.parse: ../2020/endoh3/prog_alt.c # parsing issue with comment/slash
+
+#2020_ferguson1_termcaps.parse: ../2020/ferguson1/termcaps.c # requires <curses.h>
+
+#2020_ferguson1_prog_3.parse: ../2020/ferguson1/prog.3.c # requires <curses.h>
+
+#2020_ferguson1_prog.parse: ../2020/ferguson1/prog.c # requires <curses.h>
+
+#2020_ferguson1_prog_2.parse: ../2020/ferguson1/prog.2.c # requires <curses.h>
+
+#2020_ferguson1_prog_alt.parse: ../2020/ferguson1/prog.alt.c # requires <curses.h>
+
+#2020_ferguson1_prog_3-j.parse: ../2020/ferguson1/prog.3-j.c # requires <curses.h>
+
+#2020_ferguson2_prog.parse: ../2020/ferguson2/prog.c # missing spec for stdio.h's getdelim
+
+#2020_ferguson2_recode.parse: ../2020/ferguson2/recode.c # missing spec for stdio.h's getdelim
+
+2020_giles_prog.parse: ../2020/giles/prog.c
+
+2020_kurdyukov1_prog.parse: ../2020/kurdyukov1/prog.c
+
+2020_kurdyukov1_prog_extra.parse: ../2020/kurdyukov1/prog.extra.c
+
+2020_kurdyukov1_prog_orig.parse: ../2020/kurdyukov1/prog.orig.c
+
+2020_kurdyukov2_prog_ppm.parse: ../2020/kurdyukov2/prog.ppm.c
+
+#2020_kurdyukov2_prog.parse: ../2020/kurdyukov2/prog.c # requires <jpeglib.h>
+
+#2020_kurdyukov2_prog_png.parse: ../2020/kurdyukov2/prog.png.c # requires <png.h>
+
+2020_kurdyukov3_prog.parse: ../2020/kurdyukov3/prog.c
+
+2020_kurdyukov3_prog_extra.parse: ../2020/kurdyukov3/prog.extra.c
+
+2020_kurdyukov3_prog_orig.parse: ../2020/kurdyukov3/prog.orig.c
+
+2020_kurdyukov4_prog.parse: ../2020/kurdyukov4/prog.c
+
+#2020_kurdyukov4_rand.parse: ../2020/kurdyukov4/rand.c # missing spec for stdlib.h's memmem
+
+2020_otterness_prog.parse: ../2020/otterness/prog.c
+
+#2020_tsoj_prog.parse: ../2020/tsoj/prog.c # missing macro TIOCGWINSZ (ioctl)
+
+#2020_yang_prog.parse: ../2020/yang/prog.c # missing spec for printf with non-static format argument
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
+###############################################################################
+
+# optional, for OSCS
+-include ../../Makefile.common