← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/misc/strings.c

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
tests/misc/strings.c
 
1
/* run.config
 
2
  GCC:
 
3
  OPT: -memory-footprint 1 -val -deps -out -input  -main main1 -journal-disable
 
4
  OPT: -memory-footprint 1 -val -deps -out -input  -main main2 -journal-disable
 
5
  OPT: -memory-footprint 1 -val -deps -out -input  -main main3 -journal-disable
 
6
  OPT: -memory-footprint 1 -val -deps -out -input  -main main4 -journal-disable
 
7
  OPT: -memory-footprint 1 -val -deps -out -input  -main main5 -journal-disable
 
8
  OPT: -memory-footprint 1 -val -deps -out -input  -main main6 -journal-disable
 
9
  OPT: -memory-footprint 1 -val -deps -out -input  -main main7 -journal-disable
 
10
*/
 
11
 
 
12
char s1[]="hello, world";
 
13
char s2[]="hello";
 
14
 
 
15
void main1(void)
 
16
{
 
17
  char x;
 
18
  char *p;
 
19
  p = &s1[3];
 
20
  x=*(p-4);
 
21
}
 
22
/* tests/misc/strings.c:10: Warning: out of bounds access.
 
23
 */
 
24
 
 
25
void main2(void)
 
26
{
 
27
  char x;
 
28
  char *p;
 
29
  p = &s1[3];
 
30
  x=*(p+12);
 
31
}
 
32
/* tests/misc/strings.c:20: Warning: out of bounds access.
 
33
 */
 
34
 
 
35
void main3(int c)
 
36
{
 
37
  char x;
 
38
  char *p;
 
39
  if (c)
 
40
    p = &s1[5];
 
41
  else
 
42
    p = &s2[3];
 
43
  x=*(p-4);
 
44
}
 
45
/* tests/misc/strings.c:33: Warning: out of bounds access.
 
46
Values for function main3:
 
47
  p -> {{ &s2 + {3; } ; &s1 + {5; } ;}}
 
48
  x -> {101; }
 
49
 
 
50
Les valeurs invalides dans le d�r�f�rencement ligne 33
 
51
sont oubli�es en m�me temps que l'avertissement est affich�.
 
52
L'analyse continue avec celles des valeurs qui sont valides
 
53
(d'o� x=101 � la fin de la fonction).
 
54
Il serait possible de r�duire aussi les valeurs de p
 
55
sachant que p-4 doit �tre valide.
 
56
*/
 
57
 
 
58
char *strcpy(char*dst, char*src)
 
59
{
 
60
  char* ldst=dst;
 
61
  /*@ loop pragma UNROLL_LOOP 50; */
 
62
  while (*ldst++ = *src++)
 
63
    ;
 
64
  return dst;
 
65
}
 
66
 
 
67
void main4(void)
 
68
{
 
69
  char a[10] = "Not ok";
 
70
  char b[5];
 
71
 
 
72
  strcpy(b,a);
 
73
}
 
74
 
 
75
/*
 
76
tests/misc/strings.c:52: Warning: out of bounds access.
 
77
 
 
78
*/
 
79
 
 
80
unsigned int strlen(char *s)
 
81
{
 
82
  unsigned int l=0;
 
83
 /*@ loop pragma UNROLL_LOOP 50; */
 
84
  while(*s++ != 0)
 
85
    l++;
 
86
  return l;
 
87
}
 
88
 
 
89
int main5(char c)
 
90
{
 
91
  char a[15] = "A long string";
 
92
  a[3]=c;
 
93
  a[6]=c;
 
94
  return strlen(a);
 
95
}
 
96
/*
 
97
Values for function main5:
 
98
  __retres -> {3; 6; 13; }
 
99
*/
 
100
 
 
101
int main6(void)
 
102
{
 
103
  char *s;
 
104
  char c;
 
105
  s = "toto";
 
106
  c = *s;
 
107
  return c;
 
108
}
 
109
 
 
110
char *s3="tutu";
 
111
char *s4="tutu";
 
112
 
 
113
int main7(void)
 
114
{
 
115
  char c;
 
116
  *s3=' ';
 
117
  c=*s4;
 
118
  return c;
 
119
}