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;
}