# * Copyright 2015, NICTA
# *
# * This software may be distributed and modified according to the terms of
# * the BSD 2-Clause license. Note that NO WARRANTY is provided.
# * See "LICENSE_BSD2.txt" for details.
# *
# * @TAG(NICTA_BSD)


Function 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
1 Basic Ret 0
6 Basic 2 1 i#v Word 32 Op Plus Word 32 2 Var i#v Word 32 Num 1 Word 32
7 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
8 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
9 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
10 Basic 9 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32
11 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
2 Basic 3 1 loop#2#count Word 32 Op Plus Word 32 2 Var loop#2#count Word 32 Num 1 Word 32
3 Cond 4 Err Op True Bool 0
4 Cond 11 1 Op SignedLess Bool 2 Var i#v Word 32 Num 100 Word 32
5 Basic 3 1 loop#2#count Word 32 Num 0 Word 32
12 Basic 5 1 i#v Word 32 Var x#v Word 32
EntryPoint 12

Function 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
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 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
4 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
EntryPoint 4

Function 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
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 Basic 1 1 ret__int#v Word 32 Num 1 Word 32
4 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
5 Cond 4 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 32 Symbol global_x Word 32
EntryPoint 5

Function 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
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 Basic 1 1 ret__int#v Word 32 Num 1 Word 32
4 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
5 Cond 4 Err Op PGlobalValid Bool 3 Var HTD HTD Type Word 32 Symbol global_x Word 32
EntryPoint 5

Function 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
1 Basic Ret 0
2 Cond 1 Err Op False Bool 0
3 Basic 1 1 ret__unsigned#v Word 32 Var end#v Word 32
8 Basic 4 1 f#v Word 32 Op Plus Word 32 2 Var f#v Word 32 Num 1024 Word 32
9 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
10 Basic 1 1 ret__unsigned#v Word 32 Op WordCastSigned Word 32 1 Num 21 Word 32
11 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
12 Basic 11 1 ret__int#v Word 32 Var rv#space#ret__int#v Word 32
13 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
14 Basic 13 1 r#v Word 32 Var rv#space#ret__int#v Word 32
15 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
4 Basic 5 1 loop#4#count Word 32 Op Plus Word 32 2 Var loop#4#count Word 32 Num 1 Word 32
5 Cond 6 Err Op True Bool 0
6 Cond 15 3 Op Less Bool 2 Op WordCastSigned Word 32 1 Var f#v Word 32 Var end#v Word 32
7 Basic 5 1 loop#4#count Word 32 Num 0 Word 32
16 Basic 7 1 f#v Word 32 Op WordCast Word 32 1 Var start#v Word 32
EntryPoint 16