← Back to branch summary

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

« back to all changes in this revision

Viewing changes to share/jessie/jessie_machine_prolog.h

  • 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:
share/jessie/jessie_machine_prolog.h
 
1
/**************************************************************************/
 
2
/*                                                                        */
 
3
/*  This file is part of Frama-C.                                         */
 
4
/*                                                                        */
 
5
/*  Copyright (C) 2007-2008                                               */
 
6
/*    INRIA (Institut National de Recherche en Informatique et en         */
 
7
/*           Automatique)                                                 */
 
8
/*                                                                        */
 
9
/*  you can redistribute it and/or modify it under the terms of the GNU   */
 
10
/*  Lesser General Public License as published by the Free Software       */
 
11
/*  Foundation, version 2.1.                                              */
 
12
/*                                                                        */
 
13
/*  It is distributed in the hope that it will be useful,                 */
 
14
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
 
15
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
 
16
/*  GNU Lesser General Public License for more details.                   */
 
17
/*                                                                        */
 
18
/*  See the GNU Lesser General Public License version 2.1                 */
 
19
/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
 
20
/**************************************************************************/
 
21
 
 
22
/* $Id: jessie_machine_prolog.h,v 1.8 2008/12/09 10:17:25 uid525 Exp $ */
 
23
 
 
24
#ifndef _JESSIE_MACHINE_PROLOG_H_
 
25
#define _JESSIE_MACHINE_PROLOG_H_
 
26
 
 
27
#include "stddef.h"
 
28
#include "limits.h"
 
29
 
 
30
/*@ axiomatic MemCmp {
 
31
  @
 
32
  @ logic integer memcmp{L}(char *s1, char *s2, integer n);
 
33
  @ // reads s1[0..n - 1], s2[0..n - 1];
 
34
  @
 
35
  @ axiom memcmp_range{L}:
 
36
  @   \forall char *s1, *s2; \forall integer n;
 
37
  @      INT_MIN <= memcmp(s1,s2,n) <= INT_MAX;
 
38
  @
 
39
  @ axiom memcmp_zero{L}:
 
40
  @   \forall char *s1, *s2; \forall integer n;
 
41
  @      memcmp(s1,s2,n) == 0
 
42
  @      <==> \forall integer i; 0 <= i < n ==> s1[i] == s2[i];
 
43
  @
 
44
  @ }
 
45
  @*/
 
46
 
 
47
/*@ axiomatic MemChr {
 
48
  @ logic boolean memchr{L}(char *s, integer c, integer n);
 
49
  @ // reads s[0..n - 1];
 
50
  @ // Returns [true] iff array [s] contains character [c]
 
51
  @
 
52
  @ axiom memchr_def{L}:
 
53
  @   \forall char *s; \forall integer c; \forall integer n;
 
54
  @      memchr(s,c,n) <==> \exists int i; 0 <= i < n && s[i] == c;
 
55
  @ }
 
56
  @*/
 
57
 
 
58
/*@ axiomatic MemSet {
 
59
  @ logic boolean memset{L}(char *s, integer c, integer n);
 
60
  @ // reads s[0..n - 1];
 
61
  @ // Returns [true] iff array [s] contains only character [c]
 
62
  @
 
63
  @ axiom memset_def{L}:
 
64
  @   \forall char *s; \forall integer c; \forall integer n;
 
65
  @      memset(s,c,n) <==> \forall integer i; 0 <= i < n ==> s[i] == c;
 
66
  @ }
 
67
  @*/
 
68
 
 
69
/*@ axiomatic StrLen {
 
70
  @ logic integer strlen{L}(char *s);
 
71
  @ // reads s[0..];
 
72
  @
 
73
  @ axiom strlen_pos_or_null{L}:
 
74
  @   \forall char* s; \forall integer i;
 
75
  @      (0 <= i <= INT_MAX
 
76
  @       && (\forall integer j; 0 <= j < i ==> s[j] != '\0')
 
77
  @       && s[i] == 0) ==> strlen(s) == i;
 
78
  @
 
79
  @ axiom strlen_neg{L}:
 
80
  @   \forall char* s;
 
81
  @      (\forall integer i; 0 <= i <= INT_MAX ==> s[i] != '\0')
 
82
  @      ==> strlen(s) < 0;
 
83
  @
 
84
  @ axiom strlen_range{L}:
 
85
  @   \forall char* s; strlen(s) <= INT_MAX;
 
86
  @
 
87
  @ axiom strlen_before_null{L}:
 
88
  @   \forall char* s; \forall integer i; 0 <= i < strlen(s) ==> s[i] != '\0';
 
89
  @
 
90
  @ axiom strlen_at_null{L}:
 
91
  @   \forall char* s; 0 <= strlen(s) ==> s[strlen(s)] == '\0';
 
92
  @
 
93
  @ axiom strlen_not_zero{L}:
 
94
  @   \forall char* s; \forall integer i;
 
95
  @      0 <= i <= strlen(s) && s[i] != '\0' ==> i < strlen(s);
 
96
  @
 
97
  @ axiom strlen_zero{L}:
 
98
  @   \forall char* s; \forall integer i;
 
99
  @      0 <= i <= strlen(s) && s[i] == '\0' ==> i == strlen(s);
 
100
  @
 
101
  @ axiom strlen_sup{L}:
 
102
  @   \forall char* s; \forall integer i;
 
103
  @      0 <= i && s[i] == '\0' ==> 0 <= strlen(s) <= i;
 
104
  @
 
105
  @ axiom strlen_shift{L}:
 
106
  @   \forall char* s; \forall integer i;
 
107
  @      0 <= i <= strlen(s) ==> strlen(s + i) == strlen(s) - i;
 
108
  @
 
109
  @ axiom strlen_create{L}:
 
110
  @   \forall char* s; \forall integer i;
 
111
  @      0 <= i <= INT_MAX && s[i] == '\0' ==> 0 <= strlen(s) <= i;
 
112
  @
 
113
  @ axiom strlen_create_shift{L}:
 
114
  @   \forall char* s; \forall integer i; \forall integer k;
 
115
  @      0 <= k <= i <= INT_MAX && s[i] == '\0' ==> 0 <= strlen(s+k) <= i - k;
 
116
  @
 
117
  @ axiom memcmp_strlen_left{L}:
 
118
  @   \forall char *s1, *s2; \forall integer n;
 
119
  @      memcmp(s1,s2,n) == 0 && strlen(s1) < n ==> strlen(s1) == strlen(s2);
 
120
  @      
 
121
  @ axiom memcmp_strlen_right{L}:
 
122
  @   \forall char *s1, *s2; \forall integer n;
 
123
  @      memcmp(s1,s2,n) == 0 && strlen(s2) < n ==> strlen(s1) == strlen(s2);
 
124
  @      
 
125
  @ axiom memcmp_strlen_shift_left{L}:
 
126
  @   \forall char *s1, *s2; \forall integer k, n;
 
127
  @      memcmp(s1,s2 + k,n) == 0 && 0 <= k && strlen(s1) < n ==> 
 
128
  @        0 <= strlen(s2) <= k + strlen(s1);
 
129
  @      
 
130
  @ axiom memcmp_strlen_shift_right{L}:
 
131
  @   \forall char *s1, *s2; \forall integer k, n;
 
132
  @      memcmp(s1 + k,s2,n) == 0 && 0 <= k && strlen(s2) < n ==> 
 
133
  @        0 <= strlen(s1) <= k + strlen(s2);
 
134
  @
 
135
  @ }
 
136
  @*/
 
137
 
 
138
/*@ axiomatic StrCmp {
 
139
  @ logic integer strcmp{L}(char *s1, char *s2);
 
140
  @ // reads s1[0..strlen(s1)], s2[0..strlen(s2)];
 
141
  @
 
142
  @ axiom strcmp_range{L}:
 
143
  @   \forall char *s1, *s2; INT_MIN <= strcmp(s1,s2) <= INT_MAX;
 
144
  @
 
145
  @ axiom strcmp_zero{L}:
 
146
  @   \forall char *s1, *s2;
 
147
  @      strcmp(s1,s2) == 0 <==>
 
148
  @        (strlen(s1) == strlen(s2)
 
149
  @         && \forall integer i; 0 <= i <= strlen(s1) ==> s1[i] == s2[i]);
 
150
  @ }
 
151
  @*/
 
152
 
 
153
/*@ axiomatic StrNCmp {
 
154
  @ logic integer strncmp{L}(char *s1, char *s2, integer n);
 
155
  @ // reads s1[0..n-1], s2[0..n-1];
 
156
  @
 
157
  @ axiom strncmp_zero{L}:
 
158
  @   \forall char *s1, *s2; \forall integer n;
 
159
  @      strncmp(s1,s2,n) == 0 <==>
 
160
  @        (strlen(s1) < n && strcmp(s1,s2) == 0
 
161
  @         || \forall integer i; 0 <= i < n ==> s1[i] == s2[i]);
 
162
  @ }
 
163
  @*/
 
164
 
 
165
/*@ axiomatic StrChr {
 
166
  @ logic boolean strchr{L}(char *s, integer c);
 
167
  @ // reads s[0..strlen(s)];
 
168
  @ // Returns [true] iff string [s] contains character [c]
 
169
  @
 
170
  @ axiom strchr_def{L}:
 
171
  @   \forall char *s; \forall integer c;
 
172
  @      strchr(s,c) <==> \exists integer i; 0 <= i <= strlen(s) && s[i] == c;
 
173
  @ }
 
174
  @*/
 
175
 
 
176
/*@ axiomatic WcsLen {
 
177
  @ logic integer wcslen{L}(wchar_t *s);
 
178
  @ // reads s[0..];
 
179
  @
 
180
  @ axiom wcslen_pos_or_null{L}:
 
181
  @   \forall wchar_t* s; \forall integer i;
 
182
  @      (0 <= i
 
183
  @       && (\forall integer j; 0 <= j < i ==> s[j] != L'\0')
 
184
  @       && s[i] == L'\0') ==> wcslen(s) == i;
 
185
  @
 
186
  @ axiom wcslen_neg{L}:
 
187
  @   \forall wchar_t* s;
 
188
  @      (\forall integer i; 0 <= i ==> s[i] != L'\0')
 
189
  @      ==> wcslen(s) < 0;
 
190
  @
 
191
  @ axiom wcslen_before_null{L}:
 
192
  @   \forall wchar_t* s; \forall int i; 0 <= i < wcslen(s) ==> s[i] != L'\0';
 
193
  @
 
194
  @ axiom wcslen_at_null{L}:
 
195
  @   \forall wchar_t* s; 0 <= wcslen(s) ==> s[wcslen(s)] == L'\0';
 
196
  @
 
197
  @ axiom wcslen_not_zero{L}:
 
198
  @   \forall wchar_t* s; \forall int i;
 
199
  @      0 <= i <= wcslen(s) && s[i] != L'\0' ==> i < wcslen(s);
 
200
  @
 
201
  @ axiom wcslen_zero{L}:
 
202
  @   \forall wchar_t* s; \forall int i;
 
203
  @      0 <= i <= wcslen(s) && s[i] == L'\0' ==> i == wcslen(s);
 
204
  @
 
205
  @ axiom wcslen_sup{L}:
 
206
  @   \forall wchar_t* s; \forall int i;
 
207
  @      0 <= i && s[i] == L'\0' ==> 0 <= wcslen(s) <= i;
 
208
  @
 
209
  @ axiom wcslen_shift{L}:
 
210
  @   \forall wchar_t* s; \forall int i;
 
211
  @      0 <= i <= wcslen(s) ==> wcslen(s+i) == wcslen(s)-i;
 
212
  @
 
213
  @ axiom wcslen_create{L}:
 
214
  @   \forall wchar_t* s; \forall int i;
 
215
  @      0 <= i && s[i] == L'\0' ==> 0 <= wcslen(s) <= i;
 
216
  @
 
217
  @ axiom wcslen_create_shift{L}:
 
218
  @   \forall wchar_t* s; \forall int i; \forall int k;
 
219
  @      0 <= k <= i && s[i] == L'\0' ==> 0 <= wcslen(s+k) <= i - k;
 
220
  @ }
 
221
  @*/
 
222
 
 
223
/*@ axiomatic WcsCmp {
 
224
  @ logic integer wcscmp{L}(wchar_t *s1, wchar_t *s2);
 
225
  @ // reads s1[0..wcslen(s1)], s2[0..wcslen(s2)];
 
226
  @
 
227
  @ axiom wcscmp_zero{L}:
 
228
  @   \forall wchar_t *s1, *s2;
 
229
  @      wcscmp(s1,s2) == 0 <==>
 
230
  @        (wcslen(s1) == wcslen(s2)
 
231
  @         && \forall integer i; 0 <= i <= wcslen(s1) ==> s1[i] == s2[i]);
 
232
  @ }
 
233
  @*/
 
234
 
 
235
/*@ axiomatic WcsNCmp {
 
236
  @ logic integer wcsncmp{L}(wchar_t *s1, wchar_t *s2, integer n);
 
237
  @ // reads s1[0..n-1], s2[0..n-1];
 
238
  @
 
239
  @ axiom wcsncmp_zero{L}:
 
240
  @   \forall wchar_t *s1, *s2; \forall integer n;
 
241
  @      wcsncmp(s1,s2,n) == 0 <==>
 
242
  @        (wcslen(s1) < n && wcscmp(s1,s2) == 0
 
243
  @         || \forall integer i; 0 <= i < n ==> s1[i] == s2[i]);
 
244
  @ }
 
245
  @*/
 
246
 
 
247
#endif /* _JESSIE_MACHINE_PROLOG_H_ */