1# * Copyright 2015, NICTA
2# *
3# * This software may be distributed and modified according to the terms of
4# * the BSD 2-Clause license. Note that NO WARRANTY is provided.
5# * See "LICENSE_BSD2.txt" for details.
6# *
7# * @TAG(NICTA_BSD)
8
9
10Function Loop.f 6 p#v Word 32 x#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 4 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
111 Basic Ret 0
126 Basic 2 1 i#v Word 32 Op Plus Word 32 2 Var i#v Word 32 Num 1 Word 32
137 Cond 6 Err Op Equals Bool 2 Op SignedLessEquals Bool 2 Var i#v Word 32 Op Plus Word 32 2 Var i#v Word 32 Num 1 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Num 1 Word 32
148 Basic 7 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Op Plus Word 32 2 Var p#v Word 32 Op Times Word 32 2 Op WordCastSigned Word 32 1 Var i#v Word 32 Num 4 Word 32 Var ret__int#v Word 32
159 Cond 8 Err Op PAlignValid Bool 2 Type Word 32 Op Plus Word 32 2 Var p#v Word 32 Op Times Word 32 2 Op WordCastSigned Word 32 1 Var i#v Word 32 Num 4 Word 32
1610 Basic 9 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32
1711 Call 10 Loop.g 5 Var i#v Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 64 32 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
182 Basic 3 1 loop#2#count Word 32 Op Plus Word 32 2 Var loop#2#count Word 32 Num 1 Word 32
193 Cond 4 Err Op True Bool 0
204 Cond 11 1 Op SignedLess Bool 2 Var i#v Word 32 Num 100 Word 32
215 Basic 3 1 loop#2#count Word 32 Num 0 Word 32
2212 Basic 5 1 i#v Word 32 Var x#v Word 32
23EntryPoint 12
24
25Function Loop.g 5 i#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
261 Basic Ret 0
272 Cond 1 Err Op False Bool 0
283 Basic 1 1 ret__int#v Word 32 Op Plus Word 32 2 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32 Op BWAnd Word 32 2 Var i#v Word 32 Num 15 Word 32
294 Cond 3 Err Op And Bool 2 Op Equals Bool 2 Op SignedLessEquals Bool 2 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32 Op Plus Word 32 2 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32 Op BWAnd Word 32 2 Var i#v Word 32 Num 15 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Op BWAnd Word 32 2 Var i#v Word 32 Num 15 Word 32 Op Equals Bool 2 Op Times Word 64 2 Op WordCastSigned Word 64 1 Var i#v Word 32 Op WordCastSigned Word 64 1 Num 8 Word 32 Op WordCastSigned Word 64 1 Op Times Word 32 2 Var i#v Word 32 Num 8 Word 32
30EntryPoint 4
31
32Function Loop.check_one 5 result#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
331 Basic Ret 0
342 Cond 1 Err Op False Bool 0
353 Basic 1 1 ret__int#v Word 32 Num 1 Word 32
364 Basic 3 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Symbol global_x Word 32 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Symbol global_x Word 32 Op WordCastSigned Word 32 1 Num 1 Word 32
375 Cond 4 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 32 Symbol global_x Word 32
38EntryPoint 5
39
40Function Loop.create_one 5 identifier#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
411 Basic Ret 0
422 Cond 1 Err Op False Bool 0
433 Basic 1 1 ret__int#v Word 32 Num 1 Word 32
444 Basic 3 1 Mem Mem Op MemUpdate Mem 3 Var Mem Mem Symbol global_x Word 32 Op Plus Word 32 2 Op MemAcc Word 32 2 Var Mem Mem Symbol global_x Word 32 Op WordCastSigned Word 32 1 Num 1 Word 32
455 Cond 4 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 32 Symbol global_x Word 32
46EntryPoint 5
47
48Function Loop.create_loop 6 start#v Word 32 end#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32 5 ret__unsigned#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
491 Basic Ret 0
502 Cond 1 Err Op False Bool 0
513 Basic 1 1 ret__unsigned#v Word 32 Var end#v Word 32
528 Basic 4 1 f#v Word 32 Op Plus Word 32 2 Var f#v Word 32 Num 1024 Word 32
539 Cond 8 Err Op Equals Bool 2 Op SignedLessEquals Bool 2 Var f#v Word 32 Op Plus Word 32 2 Var f#v Word 32 Num 1024 Word 32 Op SignedLessEquals Bool 2 Num 0 Word 32 Num 1024 Word 32
5410 Basic 1 1 ret__unsigned#v Word 32 Op WordCastSigned Word 32 1 Num 21 Word 32
5511 Cond 10 9 Op Not Bool 1 Op Not Bool 1 Op Equals Bool 2 Var ret__int#v Word 32 Num 0 Word 32
5612 Basic 11 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32
5713 Call 12 Loop.check_one 5 Var r#v Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 64 32 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
5814 Basic 13 1 r#v Word 32 Var rv#space#ret__int#v Word 32
5915 Call 14 Loop.create_one 5 Op WordCastSigned Word 32 1 Var f#v Word 32 Var Mem Mem Var HTD HTD Var PMS PMS Var GhostAssertions WordArray 64 32 5 rv#space#ret__int#v Word 32 Mem Mem HTD HTD PMS PMS GhostAssertions WordArray 64 32
604 Basic 5 1 loop#4#count Word 32 Op Plus Word 32 2 Var loop#4#count Word 32 Num 1 Word 32
615 Cond 6 Err Op True Bool 0
626 Cond 15 3 Op Less Bool 2 Op WordCastSigned Word 32 1 Var f#v Word 32 Var end#v Word 32
637 Basic 5 1 loop#4#count Word 32 Num 0 Word 32
6416 Basic 7 1 f#v Word 32 Op WordCast Word 32 1 Var start#v Word 32
65EntryPoint 16
66