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