parsing.res.oracle

[kernel] Parsing parsing.c (with preprocessing)
[kernel:annot-error] parsing.c:27: Warning: 
  Attribute annotation 'private' are not supported anymore, use regular C attributes instead.
[kernel:annot-error] parsing.c:15: Warning: 
  comparison of incompatible types: 𝔹 and ℤ. Ignoring global annotation
[kernel:annot-error] parsing.c:19: Warning: 
  comparison of incompatible types: 𝔹 and ℤ. Ignoring global annotation
/* Generated by Frama-C */
/*@ lemma bidon{Here}: ∀ int *t; ¬(*(t + 0) > 0);
 */
/*@ lemma bidon1{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
 */
/*@ lemma bidon2{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
 */
/*@
predicate foo{L}(int *a, int *b, int length) =
  ¬(∀ ℤ k; 0 ≤ k < length ⇒ *(a + k) ≡ *(b + k));
 */