-
Virgile Prevosto authored
[Ptests] preserve LOG after STDOPT directive See merge request frama-c/frama-c!2073
Virgile Prevosto authored[Ptests] preserve LOG after STDOPT directive See merge request frama-c/frama-c!2073
pointer_cast.res.oracle 329 B
[kernel] Parsing tests/spec/pointer_cast.c (with preprocessing)
[kernel:annot-error] tests/spec/pointer_cast.c:3: Warning:
incompatible types int * and int **
. Ignoring code annotation
/* Generated by Frama-C */
void f(int **a)
{
int *b;
/*@ assert (int *)a ≡ b; */ ;
/*@ assert a ≡ (int **)b; */ ;
return;
}