## lustrec / optim / wpdir / typed / toto_step_assert_4_Alt-Ergo.mlw @ 6a93d814

History | View | Annotate | Download (32.6 KB)

1 | 6a93d814 | xthirioux | (**************************************************************************) |
---|---|---|---|

2 | (* *) |
||

3 | (* The Why3 Verification Platform / The Why3 Development Team *) |
||

4 | (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) |
||

5 | (* *) |
||

6 | (* This software is distributed under the terms of the GNU Lesser *) |
||

7 | (* General Public License version 2.1, with the special exception *) |
||

8 | (* on linking described in file LICENSE. *) |
||

9 | (* *) |
||

10 | (* File modified by CEA (Commissariat à l'énergie atomique et aux *) |
||

11 | (* énergies alternatives). *) |
||

12 | (* *) |
||

13 | (**************************************************************************) |
||

14 | |||

15 | (* this is a prelude for Alt-Ergo*) |
||

16 | (* this is a prelude for Alt-Ergo integer arithmetic *) |
||

17 | (** The theory BuiltIn_ must be appended to this file*) |
||

18 | (** The theory Bool_ must be appended to this file*) |
||

19 | (**************************************************************************) |
||

20 | (* *) |
||

21 | (* The Why3 Verification Platform / The Why3 Development Team *) |
||

22 | (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) |
||

23 | (* *) |
||

24 | (* This software is distributed under the terms of the GNU Lesser *) |
||

25 | (* General Public License version 2.1, with the special exception *) |
||

26 | (* on linking described in file LICENSE. *) |
||

27 | (* *) |
||

28 | (* File modified by CEA (Commissariat à l'énergie atomique et aux *) |
||

29 | (* énergies alternatives). *) |
||

30 | (* *) |
||

31 | (**************************************************************************) |
||

32 | |||

33 | (* this is a prelude for Alt-Ergo*) |
||

34 | (** The theory BuiltIn_ must be appended to this file*) |
||

35 | (** The theory Bool_ must be appended to this file*) |
||

36 | (** The theory int_Int_ must be appended to this file*) |
||

37 | logic abs_int : int -> int |
||

38 | |||

39 | axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x))) |
||

40 | |||

41 | axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x)))) |
||

42 | |||

43 | axiom Abs_le : |
||

44 | (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x))) |
||

45 | |||

46 | axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y))) |
||

47 | |||

48 | axiom Abs_le2 : |
||

49 | (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) -> |
||

50 | (abs_int(x) <= y))) |
||

51 | |||

52 | axiom Abs_pos : (forall x:int. (0 <= abs_int(x))) |
||

53 | |||

54 | (**************************************************************************) |
||

55 | (* *) |
||

56 | (* The Why3 Verification Platform / The Why3 Development Team *) |
||

57 | (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) |
||

58 | (* *) |
||

59 | (* This software is distributed under the terms of the GNU Lesser *) |
||

60 | (* General Public License version 2.1, with the special exception *) |
||

61 | (* on linking described in file LICENSE. *) |
||

62 | (* *) |
||

63 | (* File modified by CEA (Commissariat à l'énergie atomique et aux *) |
||

64 | (* énergies alternatives). *) |
||

65 | (* *) |
||

66 | (**************************************************************************) |
||

67 | |||

68 | (* this is a prelude for Alt-Ergo*) |
||

69 | logic safe_comp_div: int, int -> int |
||

70 | axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y |
||

71 | logic safe_comp_mod: int, int -> int |
||

72 | axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y |
||

73 | (** The theory BuiltIn_ must be appended to this file*) |
||

74 | (** The theory Bool_ must be appended to this file*) |
||

75 | (** The theory int_Int_ must be appended to this file*) |
||

76 | (** The theory int_Abs_ must be appended to this file*) |
||

77 | axiom Div_bound : |
||

78 | (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> |
||

79 | (0 <= safe_comp_div(x,y)))) |
||

80 | |||

81 | axiom Div_bound1 : |
||

82 | (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> |
||

83 | (safe_comp_div(x,y) <= x))) |
||

84 | |||

85 | axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x)) |
||

86 | |||

87 | axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0)) |
||

88 | |||

89 | axiom Div_inf : |
||

90 | (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> |
||

91 | (safe_comp_div(x,y) = 0))) |
||

92 | |||

93 | axiom Mod_inf : |
||

94 | (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> |
||

95 | (safe_comp_mod(x,y) = x))) |
||

96 | |||

97 | axiom Div_mult : |
||

98 | (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)]. |
||

99 | (((0 < x) and ((0 <= y) and (0 <= z))) -> |
||

100 | (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x))))) |
||

101 | |||

102 | axiom Mod_mult : |
||

103 | (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)]. |
||

104 | (((0 < x) and ((0 <= y) and (0 <= z))) -> |
||

105 | (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x)))) |
||

106 | |||

107 | (**************************************************************************) |
||

108 | (* *) |
||

109 | (* The Why3 Verification Platform / The Why3 Development Team *) |
||

110 | (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) |
||

111 | (* *) |
||

112 | (* This software is distributed under the terms of the GNU Lesser *) |
||

113 | (* General Public License version 2.1, with the special exception *) |
||

114 | (* on linking described in file LICENSE. *) |
||

115 | (* *) |
||

116 | (* File modified by CEA (Commissariat à l'énergie atomique et aux *) |
||

117 | (* énergies alternatives). *) |
||

118 | (* *) |
||

119 | (**************************************************************************) |
||

120 | |||

121 | (* this is a prelude for Alt-Ergo*) |
||

122 | (* this is a prelude for Alt-Ergo real arithmetic *) |
||

123 | (** The theory BuiltIn_ must be appended to this file*) |
||

124 | (** The theory Bool_ must be appended to this file*) |
||

125 | axiom add_div : |
||

126 | (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) -> |
||

127 | (((x + y) / z) = ((x / z) + (y / z))))) |
||

128 | |||

129 | axiom sub_div : |
||

130 | (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) -> |
||

131 | (((x - y) / z) = ((x / z) - (y / z))))) |
||

132 | |||

133 | axiom neg_div : |
||

134 | (forall x:real. forall y:real. ((not (y = 0.0)) -> |
||

135 | (((-x) / y) = (-(x / y))))) |
||

136 | |||

137 | axiom assoc_mul_div : |
||

138 | (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) -> |
||

139 | (((x * y) / z) = (x * (y / z))))) |
||

140 | |||

141 | axiom assoc_div_mul : |
||

142 | (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and |
||

143 | (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z))))) |
||

144 | |||

145 | axiom assoc_div_div : |
||

146 | (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and |
||

147 | (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y)))) |
||

148 | |||

149 | (**************************************************************************) |
||

150 | (* *) |
||

151 | (* The Why3 Verification Platform / The Why3 Development Team *) |
||

152 | (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) |
||

153 | (* *) |
||

154 | (* This software is distributed under the terms of the GNU Lesser *) |
||

155 | (* General Public License version 2.1, with the special exception *) |
||

156 | (* on linking described in file LICENSE. *) |
||

157 | (* *) |
||

158 | (* File modified by CEA (Commissariat à l'énergie atomique et aux *) |
||

159 | (* énergies alternatives). *) |
||

160 | (* *) |
||

161 | (**************************************************************************) |
||

162 | |||

163 | (* this is a prelude for Alt-Ergo*) |
||

164 | (** The theory BuiltIn_ must be appended to this file*) |
||

165 | (** The theory Bool_ must be appended to this file*) |
||

166 | (** The theory real_Real_ must be appended to this file*) |
||

167 | (**************************************************************************) |
||

168 | (* *) |
||

169 | (* The Why3 Verification Platform / The Why3 Development Team *) |
||

170 | (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) |
||

171 | (* *) |
||

172 | (* This software is distributed under the terms of the GNU Lesser *) |
||

173 | (* General Public License version 2.1, with the special exception *) |
||

174 | (* on linking described in file LICENSE. *) |
||

175 | (* *) |
||

176 | (* File modified by CEA (Commissariat à l'énergie atomique et aux *) |
||

177 | (* énergies alternatives). *) |
||

178 | (* *) |
||

179 | (**************************************************************************) |
||

180 | |||

181 | (* this is a prelude for Alt-Ergo*) |
||

182 | (** The theory BuiltIn_ must be appended to this file*) |
||

183 | (** The theory Bool_ must be appended to this file*) |
||

184 | (** The theory int_Int_ must be appended to this file*) |
||

185 | (** The theory real_Real_ must be appended to this file*) |
||

186 | logic from_int : int -> real |
||

187 | |||

188 | axiom Zero : (from_int(0) = 0.0) |
||

189 | |||

190 | axiom One : (from_int(1) = 1.0) |
||

191 | |||

192 | axiom Add : |
||

193 | (forall x:int. forall y:int. |
||

194 | (from_int((x + y)) = (from_int(x) + from_int(y)))) |
||

195 | |||

196 | axiom Sub : |
||

197 | (forall x:int. forall y:int. |
||

198 | (from_int((x - y)) = (from_int(x) - from_int(y)))) |
||

199 | |||

200 | axiom Mul : |
||

201 | (forall x:int. forall y:int. |
||

202 | (from_int((x * y)) = (from_int(x) * from_int(y)))) |
||

203 | |||

204 | axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x)))) |
||

205 | |||

206 | (**************************************************************************) |
||

207 | (* *) |
||

208 | (* This file is part of WP plug-in of Frama-C. *) |
||

209 | (* *) |
||

210 | (* Copyright (C) 2007-2014 *) |
||

211 | (* CEA (Commissariat a l'energie atomique et aux energies *) |
||

212 | (* alternatives) *) |
||

213 | (* *) |
||

214 | (* you can redistribute it and/or modify it under the terms of the GNU *) |
||

215 | (* Lesser General Public License as published by the Free Software *) |
||

216 | (* Foundation, version 2.1. *) |
||

217 | (* *) |
||

218 | (* It is distributed in the hope that it will be useful, *) |
||

219 | (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) |
||

220 | (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) |
||

221 | (* GNU Lesser General Public License for more details. *) |
||

222 | (* *) |
||

223 | (* See the GNU Lesser General Public License version 2.1 *) |
||

224 | (* for more details (enclosed in the file licenses/LGPLv2.1). *) |
||

225 | (* *) |
||

226 | (**************************************************************************) |
||

227 | |||

228 | (* this is a prelude for Alt-Ergo*) |
||

229 | (** The theory BuiltIn_ must be appended to this file*) |
||

230 | (** The theory Bool_ must be appended to this file*) |
||

231 | (** The theory bool_Bool_ must be appended to this file*) |
||

232 | (** The theory int_Int_ must be appended to this file*) |
||

233 | (** The theory int_Abs_ must be appended to this file*) |
||

234 | (** The theory int_ComputerDivision_ must be appended to this file*) |
||

235 | (** The theory real_Real_ must be appended to this file*) |
||

236 | (** The theory real_RealInfix_ must be appended to this file*) |
||

237 | (** The theory real_FromInt_ must be appended to this file*) |
||

238 | logic ite : bool, 'a, 'a -> 'a |
||

239 | |||

240 | axiom ite1 : |
||

241 | (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and |
||

242 | (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y)))) |
||

243 | |||

244 | logic eqb : 'a, 'a -> bool |
||

245 | |||

246 | axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y))) |
||

247 | |||

248 | axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true))) |
||

249 | |||

250 | logic neqb : 'a, 'a -> bool |
||

251 | |||

252 | axiom neqb1 : |
||

253 | (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y)))) |
||

254 | |||

255 | axiom neqb2 : |
||

256 | (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true))) |
||

257 | |||

258 | logic zlt : int, int -> bool |
||

259 | |||

260 | logic zleq : int, int -> bool |
||

261 | |||

262 | axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x < y))) |
||

263 | |||

264 | axiom zlt2 : (forall x:int. forall y:int. ((x < y) -> (zlt(x, y) = true))) |
||

265 | |||

266 | axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y))) |
||

267 | |||

268 | axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true))) |
||

269 | |||

270 | logic rlt : real, real -> bool |
||

271 | |||

272 | logic rleq : real, real -> bool |
||

273 | |||

274 | axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x < y))) |
||

275 | |||

276 | axiom rlt2 : (forall x:real. forall y:real. ((x < y) -> (rlt(x, y) = true))) |
||

277 | |||

278 | axiom rleq1 : |
||

279 | (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y))) |
||

280 | |||

281 | axiom rleq2 : |
||

282 | (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true))) |
||

283 | |||

284 | logic truncate : real -> int |
||

285 | |||

286 | function real_of_int(x: int) : real = from_int(x) |
||

287 | |||

288 | axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x)) |
||

289 | |||

290 | axiom c_euclidian : |
||

291 | (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)]. |
||

292 | ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d))))) |
||

293 | |||

294 | axiom cdiv_cases : |
||

295 | (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 < d) -> |
||

296 | (safe_comp_div(n,d) = (n / d))))) |
||

297 | |||

298 | axiom cdiv_cases1 : |
||

299 | (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 < d) -> |
||

300 | (safe_comp_div(n,d) = (-((-n) / d)))))) |
||

301 | |||

302 | axiom cdiv_cases2 : |
||

303 | (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d < 0) -> |
||

304 | (safe_comp_div(n,d) = (-(n / (-d))))))) |
||

305 | |||

306 | axiom cdiv_cases3 : |
||

307 | (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d < 0) -> |
||

308 | (safe_comp_div(n,d) = ((-n) / (-d)))))) |
||

309 | |||

310 | axiom cmod_cases : |
||

311 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) -> |
||

312 | (safe_comp_mod(n,d) = (n % d))))) |
||

313 | |||

314 | axiom cmod_cases1 : |
||

315 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) -> |
||

316 | (safe_comp_mod(n,d) = (-((-n) % d)))))) |
||

317 | |||

318 | axiom cmod_cases2 : |
||

319 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) -> |
||

320 | (safe_comp_mod(n,d) = (n % (-d)))))) |
||

321 | |||

322 | axiom cmod_cases3 : |
||

323 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) -> |
||

324 | (safe_comp_mod(n,d) = (-((-n) % (-d))))))) |
||

325 | |||

326 | axiom cmod_remainder : |
||

327 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) -> |
||

328 | (0 <= safe_comp_mod(n,d))))) |
||

329 | |||

330 | axiom cmod_remainder1 : |
||

331 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) -> |
||

332 | (safe_comp_mod(n,d) < d)))) |
||

333 | |||

334 | axiom cmod_remainder2 : |
||

335 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) -> |
||

336 | ((-d) < safe_comp_mod(n,d))))) |
||

337 | |||

338 | axiom cmod_remainder3 : |
||

339 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) -> |
||

340 | (safe_comp_mod(n,d) <= 0)))) |
||

341 | |||

342 | axiom cmod_remainder4 : |
||

343 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) -> |
||

344 | (0 <= safe_comp_mod(n,d))))) |
||

345 | |||

346 | axiom cmod_remainder5 : |
||

347 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) -> |
||

348 | (safe_comp_mod(n,d) < (-d))))) |
||

349 | |||

350 | axiom cmod_remainder6 : |
||

351 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) -> |
||

352 | (d < safe_comp_mod(n,d))))) |
||

353 | |||

354 | axiom cmod_remainder7 : |
||

355 | (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) -> |
||

356 | (safe_comp_mod(n,d) <= 0)))) |
||

357 | |||

358 | axiom cdiv_neutral : |
||

359 | (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a)) |
||

360 | |||

361 | axiom cdiv_inv : |
||

362 | (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) -> |
||

363 | (safe_comp_div(a,a) = 1))) |
||

364 | |||

365 | (**************************************************************************) |
||

366 | (* *) |
||

367 | (* This file is part of WP plug-in of Frama-C. *) |
||

368 | (* *) |
||

369 | (* Copyright (C) 2007-2014 *) |
||

370 | (* CEA (Commissariat a l'energie atomique et aux energies *) |
||

371 | (* alternatives) *) |
||

372 | (* *) |
||

373 | (* you can redistribute it and/or modify it under the terms of the GNU *) |
||

374 | (* Lesser General Public License as published by the Free Software *) |
||

375 | (* Foundation, version 2.1. *) |
||

376 | (* *) |
||

377 | (* It is distributed in the hope that it will be useful, *) |
||

378 | (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) |
||

379 | (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) |
||

380 | (* GNU Lesser General Public License for more details. *) |
||

381 | (* *) |
||

382 | (* See the GNU Lesser General Public License version 2.1 *) |
||

383 | (* for more details (enclosed in the file licenses/LGPLv2.1). *) |
||

384 | (* *) |
||

385 | (**************************************************************************) |
||

386 | |||

387 | (* this is a prelude for Alt-Ergo*) |
||

388 | (** The theory BuiltIn_ must be appended to this file*) |
||

389 | (** The theory Bool_ must be appended to this file*) |
||

390 | (** The theory bool_Bool_ must be appended to this file*) |
||

391 | (** The theory int_Int_ must be appended to this file*) |
||

392 | logic is_uint8 : int -> prop |
||

393 | |||

394 | axiom is_uint8_def : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (0 <= x))) |
||

395 | |||

396 | axiom is_uint8_def1 : |
||

397 | (forall x:int [is_uint8(x)]. (is_uint8(x) -> (x < 256))) |
||

398 | |||

399 | axiom is_uint8_def2 : |
||

400 | (forall x:int [is_uint8(x)]. (((0 <= x) and (x < 256)) -> is_uint8(x))) |
||

401 | |||

402 | logic is_sint8 : int -> prop |
||

403 | |||

404 | axiom is_sint8_def : |
||

405 | (forall x:int [is_sint8(x)]. (is_sint8(x) -> ((-128) <= x))) |
||

406 | |||

407 | axiom is_sint8_def1 : |
||

408 | (forall x:int [is_sint8(x)]. (is_sint8(x) -> (x < 128))) |
||

409 | |||

410 | axiom is_sint8_def2 : |
||

411 | (forall x:int [is_sint8(x)]. ((((-128) <= x) and (x < 128)) -> |
||

412 | is_sint8(x))) |
||

413 | |||

414 | logic is_uint16 : int -> prop |
||

415 | |||

416 | axiom is_uint16_def : |
||

417 | (forall x:int [is_uint16(x)]. (is_uint16(x) -> (0 <= x))) |
||

418 | |||

419 | axiom is_uint16_def1 : |
||

420 | (forall x:int [is_uint16(x)]. (is_uint16(x) -> (x < 65536))) |
||

421 | |||

422 | axiom is_uint16_def2 : |
||

423 | (forall x:int [is_uint16(x)]. (((0 <= x) and (x < 65536)) -> |
||

424 | is_uint16(x))) |
||

425 | |||

426 | predicate is_sint16(x: int) = (((-32768) <= x) and (x < 32768)) |
||

427 | |||

428 | logic is_uint32 : int -> prop |
||

429 | |||

430 | axiom is_uint32_def : |
||

431 | (forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x))) |
||

432 | |||

433 | axiom is_uint32_def1 : |
||

434 | (forall x:int [is_uint32(x)]. (is_uint32(x) -> (x < 4294967296))) |
||

435 | |||

436 | axiom is_uint32_def2 : |
||

437 | (forall x:int [is_uint32(x)]. (((0 <= x) and (x < 4294967296)) -> |
||

438 | is_uint32(x))) |
||

439 | |||

440 | logic is_sint32 : int -> prop |
||

441 | |||

442 | axiom is_sint32_def : |
||

443 | (forall x:int [is_sint32(x)]. (is_sint32(x) -> ((-2147483648) <= x))) |
||

444 | |||

445 | axiom is_sint32_def1 : |
||

446 | (forall x:int [is_sint32(x)]. (is_sint32(x) -> (x < 2147483648))) |
||

447 | |||

448 | axiom is_sint32_def2 : |
||

449 | (forall x:int [is_sint32(x)]. ((((-2147483648) <= x) and |
||

450 | (x < 2147483648)) -> is_sint32(x))) |
||

451 | |||

452 | logic is_uint64 : int -> prop |
||

453 | |||

454 | axiom is_uint64_def : |
||

455 | (forall x:int [is_uint64(x)]. (is_uint64(x) -> (0 <= x))) |
||

456 | |||

457 | axiom is_uint64_def1 : |
||

458 | (forall x:int [is_uint64(x)]. (is_uint64(x) -> |
||

459 | (x < 18446744073709551616))) |
||

460 | |||

461 | axiom is_uint64_def2 : |
||

462 | (forall x:int [is_uint64(x)]. (((0 <= x) and |
||

463 | (x < 18446744073709551616)) -> is_uint64(x))) |
||

464 | |||

465 | logic is_sint64 : int -> prop |
||

466 | |||

467 | axiom is_sint64_def : |
||

468 | (forall x:int [is_sint64(x)]. (is_sint64(x) -> |
||

469 | ((-9223372036854775808) <= x))) |
||

470 | |||

471 | axiom is_sint64_def1 : |
||

472 | (forall x:int [is_sint64(x)]. (is_sint64(x) -> (x < 9223372036854775808))) |
||

473 | |||

474 | axiom is_sint64_def2 : |
||

475 | (forall x:int [is_sint64(x)]. ((((-9223372036854775808) <= x) and |
||

476 | (x < 9223372036854775808)) -> is_sint64(x))) |
||

477 | |||

478 | logic to_uint8 : int -> int |
||

479 | |||

480 | logic to_sint8 : int -> int |
||

481 | |||

482 | logic to_uint16 : int -> int |
||

483 | |||

484 | logic to_sint16 : int -> int |
||

485 | |||

486 | logic to_uint32 : int -> int |
||

487 | |||

488 | logic to_sint32 : int -> int |
||

489 | |||

490 | logic to_uint64 : int -> int |
||

491 | |||

492 | logic to_sint64 : int -> int |
||

493 | |||

494 | axiom is_to_uint8 : |
||

495 | (forall x:int [is_uint8(to_uint8(x))]. is_uint8(to_uint8(x))) |
||

496 | |||

497 | axiom is_to_sint8 : |
||

498 | (forall x:int [is_sint8(to_sint8(x))]. is_sint8(to_sint8(x))) |
||

499 | |||

500 | axiom is_to_uint16 : |
||

501 | (forall x:int [is_uint16(to_uint16(x))]. is_uint16(to_uint16(x))) |
||

502 | |||

503 | axiom is_to_sint16 : |
||

504 | (forall x:int [is_sint16(to_sint16(x))]. is_sint16(to_sint16(x))) |
||

505 | |||

506 | axiom is_to_uint32 : |
||

507 | (forall x:int [is_uint32(to_uint32(x))]. is_uint32(to_uint32(x))) |
||

508 | |||

509 | axiom is_to_sint32 : |
||

510 | (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x))) |
||

511 | |||

512 | axiom is_to_uint64 : |
||

513 | (forall x:int [is_uint64(to_uint64(x))]. is_uint64(to_uint64(x))) |
||

514 | |||

515 | axiom is_to_sint64 : |
||

516 | (forall x:int [is_sint64(to_sint64(x))]. is_sint64(to_sint64(x))) |
||

517 | |||

518 | axiom id_uint8 : |
||

519 | (forall x:int [to_uint8(x)]. (((0 <= x) and (x < 256)) -> |
||

520 | (to_uint8(x) = x))) |
||

521 | |||

522 | axiom id_sint8 : |
||

523 | (forall x:int [to_sint8(x)]. ((((-128) <= x) and (x < 128)) -> |
||

524 | (to_sint8(x) = x))) |
||

525 | |||

526 | axiom id_uint16 : |
||

527 | (forall x:int [to_uint16(x)]. (((0 <= x) and (x < 65536)) -> |
||

528 | (to_uint16(x) = x))) |
||

529 | |||

530 | axiom id_sint16 : |
||

531 | (forall x:int [to_sint16(x)]. ((((-32768) <= x) and (x < 32768)) -> |
||

532 | (to_sint16(x) = x))) |
||

533 | |||

534 | axiom id_uint32 : |
||

535 | (forall x:int [to_uint32(x)]. (((0 <= x) and (x < 4294967296)) -> |
||

536 | (to_uint32(x) = x))) |
||

537 | |||

538 | axiom id_sint32 : |
||

539 | (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and |
||

540 | (x < 2147483648)) -> (to_sint32(x) = x))) |
||

541 | |||

542 | axiom id_uint64 : |
||

543 | (forall x:int [to_uint64(x)]. (((0 <= x) and |
||

544 | (x < 18446744073709551616)) -> (to_uint64(x) = x))) |
||

545 | |||

546 | axiom id_sint64 : |
||

547 | (forall x:int [to_sint64(x)]. ((((-9223372036854775808) <= x) and |
||

548 | (x < 9223372036854775808)) -> (to_sint64(x) = x))) |
||

549 | |||

550 | logic lnot : int -> int |
||

551 | |||

552 | logic ac land : int, int -> int |
||

553 | |||

554 | logic ac lxor : int, int -> int |
||

555 | |||

556 | logic ac lor : int, int -> int |
||

557 | |||

558 | logic lsl : int, int -> int |
||

559 | |||

560 | logic lsr : int, int -> int |
||

561 | |||

562 | logic bit_testb : int, int -> bool |
||

563 | |||

564 | logic bit_test : int, int -> prop |
||

565 | |||

566 | (* ---------------------------------------------------------- *) |
||

567 | (* --- Global Definitions --- *) |
||

568 | (* ---------------------------------------------------------- *) |
||

569 | |||

570 | predicate P_trans_totoA() = true |
||

571 | |||

572 | predicate P_clock_d() = true |
||

573 | |||

574 | predicate P_trans_d |
||

575 | (x:int, |
||

576 | d:int) = |
||

577 | ((0 = d) and (x <= 0)) or ((1 = d) and (0 < x)) |
||

578 | |||

579 | predicate P_trans_totoB |
||

580 | (x:int, |
||

581 | d:int) = |
||

582 | P_trans_totoA and (P_clock_d -> P_trans_d(x, d)) |
||

583 | |||

584 | predicate P_clock_toto_2(d:int) = 1 = d |
||

585 | |||

586 | predicate P_trans_toto_2(x:int, toto_2_0:int) = (0 = x) <-> (0 <> toto_2_0) |
||

587 | |||

588 | predicate P_trans_totoC |
||

589 | (x:int, |
||

590 | d:int, |
||

591 | toto_2_0:int) = |
||

592 | P_trans_totoB(x, d) and |
||

593 | (P_clock_toto_2(d) -> P_trans_toto_2(x, toto_2_0)) |
||

594 | |||

595 | predicate P_clock_c(d:int) = 1 = d |
||

596 | |||

597 | predicate P_trans_c |
||

598 | (toto_2_0:int, |
||

599 | c:int) = |
||

600 | ((0 = c) and (0 <> toto_2_0)) or ((0 = toto_2_0) and (1 = c)) |
||

601 | |||

602 | predicate P_trans_totoD |
||

603 | (x:int, |
||

604 | d:int, |
||

605 | c:int) = |
||

606 | exists i : int. is_uint32(i) and P_trans_totoC(x, d, i) and |
||

607 | (P_clock_c(d) -> P_trans_c(i, c)) |
||

608 | |||

609 | predicate P_clock_b2(d:int, c:int) = (0 = c) and P_clock_c(d) |
||

610 | |||

611 | predicate P_trans_b2(b2_0:int) = 2 = b2_0 |
||

612 | |||

613 | predicate P_trans_totoE |
||

614 | (x:int, |
||

615 | d:int, |
||

616 | c:int, |
||

617 | b2_0:int) = |
||

618 | P_trans_totoD(x, d, c) and (P_clock_b2(d, c) -> P_trans_b2(b2_0)) |
||

619 | |||

620 | predicate P_clock_b1(d:int, c:int) = (1 = c) and P_clock_c(d) |
||

621 | |||

622 | predicate P_trans_b1(b1_0:int) = 1 = b1_0 |
||

623 | |||

624 | predicate P_trans_totoF |
||

625 | (x:int, |
||

626 | d:int, |
||

627 | c:int, |
||

628 | b2_0:int, |
||

629 | b1_0:int) = |
||

630 | P_trans_totoE(x, d, c, b2_0) and (P_clock_b1(d, c) -> P_trans_b1(b1_0)) |
||

631 | |||

632 | predicate P_clock_z(d:int) = P_clock_c(d) |
||

633 | |||

634 | predicate P_trans_z |
||

635 | (c:int, |
||

636 | b1_0:int, |
||

637 | b2_0:int, |
||

638 | z:int) = |
||

639 | ((1 = c) -> (b1_0 = z)) and ((0 = c) -> (b2_0 = z)) |
||

640 | |||

641 | predicate P_trans_totoG |
||

642 | (x:int, |
||

643 | d:int, |
||

644 | z:int) = |
||

645 | exists i_2,i_1,i : int. is_sint32(i) and is_sint32(i_1) and |
||

646 | is_uint32(i_2) and P_trans_totoF(x, d, i_2, i_1, i) and |
||

647 | (P_clock_z(d) -> P_trans_z(i_2, i, i_1, z)) |
||

648 | |||

649 | predicate P_clock_b3(d:int) = 0 = d |
||

650 | |||

651 | predicate P_trans_b3(b3_0:int) = 3 = b3_0 |
||

652 | |||

653 | predicate P_trans_totoH |
||

654 | (x:int, |
||

655 | d:int, |
||

656 | z:int, |
||

657 | b3_0:int) = |
||

658 | P_trans_totoG(x, d, z) and (P_clock_b3(d) -> P_trans_b3(b3_0)) |
||

659 | |||

660 | predicate P_clock_y() = P_clock_d |
||

661 | |||

662 | predicate P_trans_y |
||

663 | (d:int, |
||

664 | b3_0:int, |
||

665 | z:int, |
||

666 | y:int) = |
||

667 | ((0 = d) -> (b3_0 = y)) and ((1 = d) -> (y = z)) |
||

668 | |||

669 | predicate P_trans_totoI |
||

670 | (x:int, |
||

671 | y:int) = |
||

672 | exists i_2,i_1,i : int. is_sint32(i_1) and is_sint32(i_2) and |
||

673 | is_uint32(i) and P_trans_totoH(x, i, i_2, i_1) and |
||

674 | (P_clock_y -> P_trans_y(i, i_1, i_2, y)) |
||

675 | |||

676 | (**************************************************************************) |
||

677 | (* *) |
||

678 | (* This file is part of WP plug-in of Frama-C. *) |
||

679 | (* *) |
||

680 | (* Copyright (C) 2007-2014 *) |
||

681 | (* CEA (Commissariat a l'energie atomique et aux energies *) |
||

682 | (* alternatives) *) |
||

683 | (* *) |
||

684 | (* you can redistribute it and/or modify it under the terms of the GNU *) |
||

685 | (* Lesser General Public License as published by the Free Software *) |
||

686 | (* Foundation, version 2.1. *) |
||

687 | (* *) |
||

688 | (* It is distributed in the hope that it will be useful, *) |
||

689 | (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) |
||

690 | (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) |
||

691 | (* GNU Lesser General Public License for more details. *) |
||

692 | (* *) |
||

693 | (* See the GNU Lesser General Public License version 2.1 *) |
||

694 | (* for more details (enclosed in the file licenses/LGPLv2.1). *) |
||

695 | (* *) |
||

696 | (**************************************************************************) |
||

697 | |||

698 | (* this is a prelude for Alt-Ergo*) |
||

699 | (** The theory BuiltIn_ must be appended to this file*) |
||

700 | (** The theory Bool_ must be appended to this file*) |
||

701 | (** The theory bool_Bool_ must be appended to this file*) |
||

702 | (** The theory int_Int_ must be appended to this file*) |
||

703 | (** The theory map_Map_ must be appended to this file*) |
||

704 | type addr = { base : int; offset : int |
||

705 | } |
||

706 | |||

707 | logic addr_le : addr, addr -> prop |
||

708 | |||

709 | logic addr_lt : addr, addr -> prop |
||

710 | |||

711 | logic addr_le_bool : addr, addr -> bool |
||

712 | |||

713 | logic addr_lt_bool : addr, addr -> bool |
||

714 | |||

715 | axiom addr_le_def : |
||

716 | (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) -> |
||

717 | (addr_le(p, q) -> ((p).offset <= (q).offset)))) |
||

718 | |||

719 | axiom addr_le_def1 : |
||

720 | (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) -> |
||

721 | (((p).offset <= (q).offset) -> addr_le(p, q)))) |
||

722 | |||

723 | axiom addr_lt_def : |
||

724 | (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) -> |
||

725 | (addr_lt(p, q) -> ((p).offset < (q).offset)))) |
||

726 | |||

727 | axiom addr_lt_def1 : |
||

728 | (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) -> |
||

729 | (((p).offset < (q).offset) -> addr_lt(p, q)))) |
||

730 | |||

731 | axiom addr_le_bool_def : |
||

732 | (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) -> |
||

733 | (addr_le_bool(p, q) = true))) |
||

734 | |||

735 | axiom addr_le_bool_def1 : |
||

736 | (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p, |
||

737 | q) = true) -> addr_le(p, q))) |
||

738 | |||

739 | axiom addr_lt_bool_def : |
||

740 | (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) -> |
||

741 | (addr_lt_bool(p, q) = true))) |
||

742 | |||

743 | axiom addr_lt_bool_def1 : |
||

744 | (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p, |
||

745 | q) = true) -> addr_lt(p, q))) |
||

746 | |||

747 | function null() : addr = { base = 0; offset = 0 } |
||

748 | |||

749 | function global(b: int) : addr = { base = b; offset = 0 } |
||

750 | |||

751 | function shift(p: addr, k: int) : addr = { base = (p).base; offset = |
||

752 | ((p).offset + k) } |
||

753 | |||

754 | predicate included(p: addr, a: int, q: addr, b: int) = ((0 < a) -> |
||

755 | ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and |
||

756 | (((p).offset + a) <= ((q).offset + b)))))) |
||

757 | |||

758 | predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or |
||

759 | ((b <= 0) or ((not ((p).base = (q).base)) or |
||

760 | ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset))))) |
||

761 | |||

762 | predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr, |
||

763 | a1: int) = |
||

764 | (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) -> |
||

765 | ((m1[q]) = (m2[q])))) |
||

766 | |||

767 | predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr, |
||

768 | a1: int) = |
||

769 | (forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) -> |
||

770 | ((m1[q]) = (m2[q])))) |
||

771 | |||

772 | predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 < n) -> |
||

773 | ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base])))) |
||

774 | |||

775 | predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 < n) -> |
||

776 | ((0 < (p).base) and ((0 <= (p).offset) and |
||

777 | (((p).offset + n) <= (m[(p).base]))))) |
||

778 | |||

779 | axiom valid_rw_rd : |
||

780 | (forall m:(int,int) farray. |
||

781 | (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n))))) |
||

782 | |||

783 | axiom valid_string : |
||

784 | (forall m:(int,int) farray. |
||

785 | (forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and |
||

786 | ((p).offset < (m[(p).base]))) -> valid_rd(m, p, 1))))) |
||

787 | |||

788 | axiom valid_string1 : |
||

789 | (forall m:(int,int) farray. |
||

790 | (forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and |
||

791 | ((p).offset < (m[(p).base]))) -> (not valid_rw(m, p, 1)))))) |
||

792 | |||

793 | axiom separated_1 : |
||

794 | (forall p:addr. forall q:addr. |
||

795 | (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q, |
||

796 | b), { base = (p).base; offset = i }, { base = (q).base; offset = j }]. |
||

797 | (separated(p, a, q, b) -> ((((p).offset <= i) and |
||

798 | (i < ((p).offset + a))) -> ((((q).offset <= j) and |
||

799 | (j < ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = { |
||

800 | base = (q).base; offset = j }))))))) |
||

801 | |||

802 | logic region : int -> int |
||

803 | |||

804 | logic linked : (int,int) farray -> prop |
||

805 | |||

806 | logic sconst : (addr,int) farray -> prop |
||

807 | |||

808 | predicate framed(m: (addr,addr) farray) = |
||

809 | (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0)) |
||

810 | |||

811 | axiom separated_included : |
||

812 | (forall p:addr. forall q:addr. |
||

813 | (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)]. |
||

814 | ((0 < a) -> ((0 < b) -> (separated(p, a, q, b) -> (not included(p, a, q, |
||

815 | b))))))) |
||

816 | |||

817 | axiom included_trans : |
||

818 | (forall p:addr. forall q:addr. forall r:addr. |
||

819 | (forall a:int. forall b:int. forall c:int [included(p, a, q, b), |
||

820 | included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) -> |
||

821 | included(p, a, r, c))))) |
||

822 | |||

823 | axiom separated_trans : |
||

824 | (forall p:addr. forall q:addr. forall r:addr. |
||

825 | (forall a:int. forall b:int. forall c:int [included(p, a, q, b), |
||

826 | separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) -> |
||

827 | separated(p, a, r, c))))) |
||

828 | |||

829 | axiom separated_sym : |
||

830 | (forall p:addr. forall q:addr. |
||

831 | (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q, |
||

832 | b) -> separated(q, b, p, a)))) |
||

833 | |||

834 | axiom separated_sym1 : |
||

835 | (forall p:addr. forall q:addr. |
||

836 | (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p, |
||

837 | a) -> separated(p, a, q, b)))) |
||

838 | |||

839 | axiom eqmem_included : |
||

840 | (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray. |
||

841 | (forall p:addr. forall q:addr. |
||

842 | (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)]. |
||

843 | (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1)))))) |
||

844 | |||

845 | axiom eqmem_sym : |
||

846 | (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray. |
||

847 | (forall p:addr. |
||

848 | (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1))))) |
||

849 | |||

850 | axiom havoc_sym : |
||

851 | (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray. |
||

852 | (forall p:addr. |
||

853 | (forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1))))) |
||

854 | |||

855 | logic cast : addr -> int |
||

856 | |||

857 | axiom cast_injective : |
||

858 | (forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) -> |
||

859 | (p = q))) |
||

860 | |||

861 | logic hardware : int -> int |
||

862 | |||

863 | axiom hardnull : (hardware(0) = 0) |
||

864 | |||

865 | (* ---------------------------------------------------------- *) |
||

866 | (* --- Assertion (file clocks7/clocks7_7.c, line 155) --- *) |
||

867 | (* ---------------------------------------------------------- *) |
||

868 | |||

869 | goal toto_step_assert_4: |
||

870 | forall i : int. |
||

871 | forall t_4,t_3,t_2,t_1,t : (addr,int) farray. |
||

872 | forall a : addr. |
||

873 | P_trans_totoA -> |
||

874 | (0 < i) -> |
||

875 | P_clock_toto_2(1) -> |
||

876 | is_sint32(i) -> |
||

877 | is_sint32(t[a]) -> |
||

878 | is_sint32(t_1[a]) -> |
||

879 | is_sint32(t_2[a]) -> |
||

880 | is_sint32(t_3[a]) -> |
||

881 | is_sint32(t_4[a]) -> |
||

882 | P_trans_totoB(i, 1) -> |
||

883 | (0 = (ite((eqb(0, i)), 1, 0))) -> |
||

884 | (region(a.base) <= 0) -> |
||

885 | (P_clock_d -> P_trans_d(i, 1)) -> |
||

886 | P_trans_toto_2(i, 0) |