1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/macro_escape_chars.c (with preprocessing)
/* Generated by Frama-C */
struct file;
typedef struct file FILE;
extern FILE *fopen(char const *, char const *);
extern int fclose(FILE *);
extern int putc(int, FILE *);
extern int fputs(char const *, FILE *);
/*@ predicate foo(char *s) = \true;
*/
/*@ lemma test1: foo("\\");
*/
/*@ lemma test2: '\\' ≡ '\\';
*/
int main(int argc, char **argv)
{
int __retres;
FILE *f;
f = fopen("/tmp/testfile.out","w");
putc('\\',f);
fputs("\\",f);
fclose(f);
__retres = 0;
return __retres;
}
|
