pollution: buf
int setjmp(jmp_buf buf); 

pollution: buf
pollution: value
void longjmp(jmp_buf buf, int value);