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

History | View | Annotate | Download (32.8 KB)

1 |
(**************************************************************************) |
---|---|

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 174) --- *) |

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

868 | |

869 |
goal toto_step_assert_15: |

870 |
forall i : int. |

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

872 |
forall a : addr. |

873 |
P_trans_totoA -> |

874 |
(0 < i) -> |

875 |
P_clock_z(1) -> |

876 |
is_sint32(i) -> |

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

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

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

880 |
P_trans_totoB(i, 1) -> |

881 |
P_trans_totoC(i, 1, 0) -> |

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

883 |
(P_clock_b1(1, 1) -> P_trans_b1(1)) -> |

884 |
(P_clock_c(1) -> P_trans_c(0, 1)) -> |

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

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

887 |
(P_clock_toto_2(1) -> P_trans_toto_2(i, 0)) -> |

888 |
P_trans_totoF(i, 1, 1, 1, 1) -> |

889 |
P_trans_z(1, 1, 1, 1) |

890 |