-
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
first.c 212 B
/* run.config
OPT: -print tests/spec/third.c tests/spec/second.c -journal-disable
*/
/*@ behavior b:
requires \valid(first);
ensures \result == 0;*/
int bar(int *first);
void main (int * c) {
bar(c);
}