File: assigns.res.oracle

package info (click to toggle)
frama-c 20161101%2Bsilicon%2Bdfsg-5
links: PTS, VCS
area: main
in suites: stretch
size: 42,324 kB
ctags: 35,695
sloc: ml: 200,142; ansic: 31,465; makefile: 2,334; sh: 1,643; lisp: 259; python: 85; asm: 26
file content (1012 lines) | stat: -rw-r--r-- 37,165 bytes
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/assigns.i (no preprocessing)
tests/value/assigns.i:31:[kernel] warning: parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  v ∈ [--..--]
  G ∈ {0}
  T[0..99] ∈ {0}
  Tpost[0..99] ∈ {0}
  t[0..9] ∈ {0}
  t2[0..99999] ∈ {0}
  t3[0..99999] ∈ {0}
  x ∈ {0}
  k ∈ {53}
  y1 ∈ {0}
  y2 ∈ {0}
  y3 ∈ {0}
  t_main3_1[0..6][0..7] ∈ {0}
  t_main3_2[0..2][0..3][0..4] ∈ {0}
  t_main4[0..999] ∈ {0}
  u_main4[0..99] ∈ {0}
[value] computing for function main1 <- main.
        Called from tests/value/assigns.i:110.
[value] computing for function F1 <- main1 <- main.
        Called from tests/value/assigns.i:46.
[value] using specification for function F1
[value] Done for function F1
tests/value/assigns.i:48:[value] entering loop for the first time
[value] computing for function f <- main1 <- main.
        Called from tests/value/assigns.i:49.
[value] using specification for function f
[value] Done for function f
[value] computing for function f <- main1 <- main.
        Called from tests/value/assigns.i:49.
[value] Done for function f
[value] computing for function f <- main1 <- main.
        Called from tests/value/assigns.i:49.
[value] Done for function f
[value] computing for function f <- main1 <- main.
        Called from tests/value/assigns.i:49.
[value] Done for function f
[value] computing for function f <- main1 <- main.
        Called from tests/value/assigns.i:49.
[value] Done for function f
tests/value/assigns.i:51:[value] warning: signed overflow. assert -2147483648 ≤ 2 * (int)(&T);
tests/value/assigns.i:51:[value] warning: signed overflow. assert 2 * (int)(&T) ≤ 2147483647;
[value] computing for function g <- main1 <- main.
        Called from tests/value/assigns.i:51.
[value] using specification for function g
[value] Done for function g
tests/value/assigns.i:52:[value] warning: signed overflow. assert -2147483648 ≤ 2 * (int)(&t3);
tests/value/assigns.i:52:[value] warning: signed overflow. assert 2 * (int)(&t3) ≤ 2147483647;
[value] computing for function h <- main1 <- main.
        Called from tests/value/assigns.i:52.
[value] using specification for function h
[value] Done for function h
[value] computing for function j <- main1 <- main.
        Called from tests/value/assigns.i:54.
tests/value/assigns.i:54:[value] Cannot evaluate range bound foo(*p)
        (unsupported ACSL construct: logic functions or predicates). Approximating
[value] using specification for function j
[value] Done for function j
[value] computing for function assigns_post <- main1 <- main.
        Called from tests/value/assigns.i:56.
[value] using specification for function assigns_post
tests/value/assigns.i:39:[value] warning: no \from part
                 for clause 'assigns Tpost[\at(\old(i),Post)], Tpost[\at(k,Post)];' of
                 function assigns_post
tests/value/assigns.i:56:[value] warning: cannot interpret 'from' clause 'assigns \at(x,Post) \from \at(x,Post);'
                 of function assigns_post
                 (no environment to evaluate \at(_,Post))
tests/value/assigns.i:56:[value] warning: cannot interpret assigns Tpost[\at(k,Post)] in function assigns_post
                 (no environment to evaluate \at(_,Post)); effects will be ignored
[value] Done for function assigns_post
[value] Recording results for main1
[value] Done for function main1
[value] computing for function main2 <- main.
        Called from tests/value/assigns.i:111.
[value] computing for function ff1 <- main2 <- main.
        Called from tests/value/assigns.i:76.
[value] using specification for function ff1
tests/value/assigns.i:60:[value] warning: no 'assigns \result \from ...' clause specified for function ff1
[value] Done for function ff1
[value] computing for function ff3 <- main2 <- main.
        Called from tests/value/assigns.i:78.
[value] using specification for function ff3
tests/value/assigns.i:68:[value] warning: no \from part for clause 'assigns y1, y3;' of function ff3
[value] Done for function ff3
[value] computing for function ff4 <- main2 <- main.
        Called from tests/value/assigns.i:79.
tests/value/assigns.i:79:[kernel] warning: Neither code nor specification for function ff4, generating default assigns from the prototype
[value] using specification for function ff4
[value] Done for function ff4
[value] computing for function ff5 <- main2 <- main.
        Called from tests/value/assigns.i:80.
tests/value/assigns.i:80:[kernel] warning: Neither code nor specification for function ff5, generating default assigns from the prototype
[value] using specification for function ff5
[value] Done for function ff5
[value] computing for function ff2 <- main2 <- main.
        Called from tests/value/assigns.i:82.
tests/value/assigns.i:82:[kernel] warning: Neither code nor specification for function ff2, generating default assigns from the prototype
[value] using specification for function ff2
[value] Done for function ff2
[value] computing for function ff2_bis <- main2 <- main.
        Called from tests/value/assigns.i:83.
[value] using specification for function ff2_bis
tests/value/assigns.i:64:[value] warning: no 'assigns \result \from ...' clause specified for function ff2_bis
[value] Done for function ff2_bis
tests/value/assigns.i:84:[value] warning: pointer comparison. assert \pointer_comparable((void *)p, (void *)(&x));
[value] Recording results for main2
[value] Done for function main2
[value] computing for function main3 <- main.
        Called from tests/value/assigns.i:112.
tests/value/assigns.i:112:[kernel] warning: Neither code nor specification for function main3, generating default assigns from the prototype
[value] using specification for function main3
[value] Done for function main3
[value] computing for function main4 <- main.
        Called from tests/value/assigns.i:113.
[value] computing for function f_main4_1 <- main4 <- main.
        Called from tests/value/assigns.i:104.
tests/value/assigns.i:104:[kernel] more than 200(1000) elements to enumerate. Approximating.
[value] using specification for function f_main4_1
tests/value/assigns.i:104:[kernel] more than 200(1000) locations to update in array. Approximating.
[value] Done for function f_main4_1
[value] computing for function f_main4_2 <- main4 <- main.
        Called from tests/value/assigns.i:105.
[value] using specification for function f_main4_2
tests/value/assigns.i:105:[kernel] more than 200(1000) locations to update in array. Approximating.
[value] Done for function f_main4_2
[value] Recording results for main4
[value] Done for function main4
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main1:
  T[0..99] ∈ [--..--]
  Tpost[0..17] ∈ {0}
       [18] ∈ [--..--]
       [19..99] ∈ {0}
  t[0].f1 ∈ {0}
   {[0].f2; [1..5]} ∈ [--..--]
   [6..9] ∈ {0}
  t2[0..99999] ∈ [--..--]
  t3[0..99999] ∈ [--..--]
  x ∈ {{ ANYTHING }}
[value:final-states] Values at end of function main2:
  y1 ∈ [--..--]
  y2 ∈ [--..--]
  y3 ∈ [--..--]
  l ∈ [--..--]
  p ∈ {{ NULL + [--..--] ; &alloced_return_ff2 + [0..2147483644],0%4 }}
  q ∈ {{ NULL + [--..--] ; &alloced_return_ff2_bis + [0..2147483644],0%4 }}
  __retres ∈ {1}
[value:final-states] Values at end of function main4:
  t_main4{[0..998]; [999].f1} ∈ [--..--]
         [999].f2 ∈ {0}
  u_main4[0].f1 ∈ [--..--]
         [0].f2 ∈ {0}
         [1].f1 ∈ [--..--]
         [1].f2 ∈ {0}
         [2].f1 ∈ [--..--]
         [2].f2 ∈ {0}
         [3].f1 ∈ [--..--]
         [3].f2 ∈ {0}
         [4].f1 ∈ [--..--]
         [4].f2 ∈ {0}
         [5].f1 ∈ [--..--]
         [5].f2 ∈ {0}
         [6].f1 ∈ [--..--]
         [6].f2 ∈ {0}
         [7].f1 ∈ [--..--]
         [7].f2 ∈ {0}
         [8].f1 ∈ [--..--]
         [8].f2 ∈ {0}
         [9].f1 ∈ [--..--]
         [9].f2 ∈ {0}
         [10].f1 ∈ [--..--]
         [10].f2 ∈ {0}
         [11].f1 ∈ [--..--]
         [11].f2 ∈ {0}
         [12].f1 ∈ [--..--]
         [12].f2 ∈ {0}
         [13].f1 ∈ [--..--]
         [13].f2 ∈ {0}
         [14].f1 ∈ [--..--]
         [14].f2 ∈ {0}
         [15].f1 ∈ [--..--]
         [15].f2 ∈ {0}
         [16].f1 ∈ [--..--]
         [16].f2 ∈ {0}
         [17].f1 ∈ [--..--]
         [17].f2 ∈ {0}
         [18].f1 ∈ [--..--]
         [18].f2 ∈ {0}
         [19].f1 ∈ [--..--]
         [19].f2 ∈ {0}
         [20].f1 ∈ [--..--]
         [20].f2 ∈ {0}
         [21].f1 ∈ [--..--]
         [21].f2 ∈ {0}
         [22].f1 ∈ [--..--]
         [22].f2 ∈ {0}
         [23].f1 ∈ [--..--]
         [23].f2 ∈ {0}
         [24].f1 ∈ [--..--]
         [24].f2 ∈ {0}
         [25].f1 ∈ [--..--]
         [25].f2 ∈ {0}
         [26].f1 ∈ [--..--]
         [26].f2 ∈ {0}
         [27].f1 ∈ [--..--]
         [27].f2 ∈ {0}
         [28].f1 ∈ [--..--]
         [28].f2 ∈ {0}
         [29].f1 ∈ [--..--]
         [29].f2 ∈ {0}
         [30].f1 ∈ [--..--]
         [30].f2 ∈ {0}
         [31].f1 ∈ [--..--]
         [31].f2 ∈ {0}
         [32].f1 ∈ [--..--]
         [32].f2 ∈ {0}
         [33].f1 ∈ [--..--]
         [33].f2 ∈ {0}
         [34].f1 ∈ [--..--]
         [34].f2 ∈ {0}
         [35].f1 ∈ [--..--]
         [35].f2 ∈ {0}
         [36].f1 ∈ [--..--]
         [36].f2 ∈ {0}
         [37].f1 ∈ [--..--]
         [37].f2 ∈ {0}
         [38].f1 ∈ [--..--]
         [38].f2 ∈ {0}
         [39].f1 ∈ [--..--]
         [39].f2 ∈ {0}
         [40].f1 ∈ [--..--]
         [40].f2 ∈ {0}
         [41].f1 ∈ [--..--]
         [41].f2 ∈ {0}
         [42].f1 ∈ [--..--]
         [42].f2 ∈ {0}
         [43].f1 ∈ [--..--]
         [43].f2 ∈ {0}
         [44].f1 ∈ [--..--]
         [44].f2 ∈ {0}
         [45].f1 ∈ [--..--]
         [45].f2 ∈ {0}
         [46].f1 ∈ [--..--]
         [46].f2 ∈ {0}
         [47].f1 ∈ [--..--]
         [47].f2 ∈ {0}
         [48].f1 ∈ [--..--]
         [48].f2 ∈ {0}
         [49].f1 ∈ [--..--]
         [49].f2 ∈ {0}
         [50].f1 ∈ [--..--]
         [50].f2 ∈ {0}
         [51].f1 ∈ [--..--]
         [51].f2 ∈ {0}
         [52].f1 ∈ [--..--]
         [52].f2 ∈ {0}
         [53].f1 ∈ [--..--]
         [53].f2 ∈ {0}
         [54].f1 ∈ [--..--]
         [54].f2 ∈ {0}
         [55].f1 ∈ [--..--]
         [55].f2 ∈ {0}
         [56].f1 ∈ [--..--]
         [56].f2 ∈ {0}
         [57].f1 ∈ [--..--]
         [57].f2 ∈ {0}
         [58].f1 ∈ [--..--]
         [58].f2 ∈ {0}
         [59].f1 ∈ [--..--]
         [59].f2 ∈ {0}
         [60].f1 ∈ [--..--]
         [60].f2 ∈ {0}
         [61].f1 ∈ [--..--]
         [61].f2 ∈ {0}
         [62].f1 ∈ [--..--]
         [62].f2 ∈ {0}
         [63].f1 ∈ [--..--]
         [63].f2 ∈ {0}
         [64].f1 ∈ [--..--]
         [64].f2 ∈ {0}
         [65].f1 ∈ [--..--]
         [65].f2 ∈ {0}
         [66].f1 ∈ [--..--]
         [66].f2 ∈ {0}
         [67].f1 ∈ [--..--]
         [67].f2 ∈ {0}
         [68].f1 ∈ [--..--]
         [68].f2 ∈ {0}
         [69].f1 ∈ [--..--]
         [69].f2 ∈ {0}
         [70].f1 ∈ [--..--]
         [70].f2 ∈ {0}
         [71].f1 ∈ [--..--]
         [71].f2 ∈ {0}
         [72].f1 ∈ [--..--]
         [72].f2 ∈ {0}
         [73].f1 ∈ [--..--]
         [73].f2 ∈ {0}
         [74].f1 ∈ [--..--]
         [74].f2 ∈ {0}
         [75].f1 ∈ [--..--]
         [75].f2 ∈ {0}
         [76].f1 ∈ [--..--]
         [76].f2 ∈ {0}
         [77].f1 ∈ [--..--]
         [77].f2 ∈ {0}
         [78].f1 ∈ [--..--]
         [78].f2 ∈ {0}
         [79].f1 ∈ [--..--]
         [79].f2 ∈ {0}
         [80].f1 ∈ [--..--]
         [80].f2 ∈ {0}
         [81].f1 ∈ [--..--]
         [81].f2 ∈ {0}
         [82].f1 ∈ [--..--]
         [82].f2 ∈ {0}
         [83].f1 ∈ [--..--]
         [83].f2 ∈ {0}
         [84].f1 ∈ [--..--]
         [84].f2 ∈ {0}
         [85].f1 ∈ [--..--]
         [85].f2 ∈ {0}
         [86].f1 ∈ [--..--]
         [86].f2 ∈ {0}
         [87].f1 ∈ [--..--]
         [87].f2 ∈ {0}
         [88].f1 ∈ [--..--]
         [88].f2 ∈ {0}
         [89].f1 ∈ [--..--]
         [89].f2 ∈ {0}
         [90].f1 ∈ [--..--]
         [90].f2 ∈ {0}
         [91].f1 ∈ [--..--]
         [91].f2 ∈ {0}
         [92].f1 ∈ [--..--]
         [92].f2 ∈ {0}
         [93].f1 ∈ [--..--]
         [93].f2 ∈ {0}
         [94].f1 ∈ [--..--]
         [94].f2 ∈ {0}
         [95].f1 ∈ [--..--]
         [95].f2 ∈ {0}
         [96].f1 ∈ [--..--]
         [96].f2 ∈ {0}
         [97].f1 ∈ [--..--]
         [97].f2 ∈ {0}
         [98].f1 ∈ [--..--]
         [98].f2 ∈ {0}
         [99].f1 ∈ [--..--]
         [99].f2 ∈ {0}
[value:final-states] Values at end of function main:
  T[0..99] ∈ [--..--]
  Tpost[0..17] ∈ {0}
       [18] ∈ [--..--]
       [19..99] ∈ {0}
  t[0].f1 ∈ {0}
   {[0].f2; [1..5]} ∈ [--..--]
   [6..9] ∈ {0}
  t2[0..99999] ∈ [--..--]
  t3[0..99999] ∈ [--..--]
  x ∈ {{ ANYTHING }}
  y1 ∈ [--..--]
  y2 ∈ [--..--]
  y3 ∈ [--..--]
  t_main3_1[0][0..7] ∈ [--..--]
           [1..6][0..7] ∈ {0}
  t_main3_2[0..2][0..3][0..4] ∈ [--..--]
  t_main4{[0..998]; [999].f1} ∈ [--..--]
         [999].f2 ∈ {0}
  u_main4[0].f1 ∈ [--..--]
         [0].f2 ∈ {0}
         [1].f1 ∈ [--..--]
         [1].f2 ∈ {0}
         [2].f1 ∈ [--..--]
         [2].f2 ∈ {0}
         [3].f1 ∈ [--..--]
         [3].f2 ∈ {0}
         [4].f1 ∈ [--..--]
         [4].f2 ∈ {0}
         [5].f1 ∈ [--..--]
         [5].f2 ∈ {0}
         [6].f1 ∈ [--..--]
         [6].f2 ∈ {0}
         [7].f1 ∈ [--..--]
         [7].f2 ∈ {0}
         [8].f1 ∈ [--..--]
         [8].f2 ∈ {0}
         [9].f1 ∈ [--..--]
         [9].f2 ∈ {0}
         [10].f1 ∈ [--..--]
         [10].f2 ∈ {0}
         [11].f1 ∈ [--..--]
         [11].f2 ∈ {0}
         [12].f1 ∈ [--..--]
         [12].f2 ∈ {0}
         [13].f1 ∈ [--..--]
         [13].f2 ∈ {0}
         [14].f1 ∈ [--..--]
         [14].f2 ∈ {0}
         [15].f1 ∈ [--..--]
         [15].f2 ∈ {0}
         [16].f1 ∈ [--..--]
         [16].f2 ∈ {0}
         [17].f1 ∈ [--..--]
         [17].f2 ∈ {0}
         [18].f1 ∈ [--..--]
         [18].f2 ∈ {0}
         [19].f1 ∈ [--..--]
         [19].f2 ∈ {0}
         [20].f1 ∈ [--..--]
         [20].f2 ∈ {0}
         [21].f1 ∈ [--..--]
         [21].f2 ∈ {0}
         [22].f1 ∈ [--..--]
         [22].f2 ∈ {0}
         [23].f1 ∈ [--..--]
         [23].f2 ∈ {0}
         [24].f1 ∈ [--..--]
         [24].f2 ∈ {0}
         [25].f1 ∈ [--..--]
         [25].f2 ∈ {0}
         [26].f1 ∈ [--..--]
         [26].f2 ∈ {0}
         [27].f1 ∈ [--..--]
         [27].f2 ∈ {0}
         [28].f1 ∈ [--..--]
         [28].f2 ∈ {0}
         [29].f1 ∈ [--..--]
         [29].f2 ∈ {0}
         [30].f1 ∈ [--..--]
         [30].f2 ∈ {0}
         [31].f1 ∈ [--..--]
         [31].f2 ∈ {0}
         [32].f1 ∈ [--..--]
         [32].f2 ∈ {0}
         [33].f1 ∈ [--..--]
         [33].f2 ∈ {0}
         [34].f1 ∈ [--..--]
         [34].f2 ∈ {0}
         [35].f1 ∈ [--..--]
         [35].f2 ∈ {0}
         [36].f1 ∈ [--..--]
         [36].f2 ∈ {0}
         [37].f1 ∈ [--..--]
         [37].f2 ∈ {0}
         [38].f1 ∈ [--..--]
         [38].f2 ∈ {0}
         [39].f1 ∈ [--..--]
         [39].f2 ∈ {0}
         [40].f1 ∈ [--..--]
         [40].f2 ∈ {0}
         [41].f1 ∈ [--..--]
         [41].f2 ∈ {0}
         [42].f1 ∈ [--..--]
         [42].f2 ∈ {0}
         [43].f1 ∈ [--..--]
         [43].f2 ∈ {0}
         [44].f1 ∈ [--..--]
         [44].f2 ∈ {0}
         [45].f1 ∈ [--..--]
         [45].f2 ∈ {0}
         [46].f1 ∈ [--..--]
         [46].f2 ∈ {0}
         [47].f1 ∈ [--..--]
         [47].f2 ∈ {0}
         [48].f1 ∈ [--..--]
         [48].f2 ∈ {0}
         [49].f1 ∈ [--..--]
         [49].f2 ∈ {0}
         [50].f1 ∈ [--..--]
         [50].f2 ∈ {0}
         [51].f1 ∈ [--..--]
         [51].f2 ∈ {0}
         [52].f1 ∈ [--..--]
         [52].f2 ∈ {0}
         [53].f1 ∈ [--..--]
         [53].f2 ∈ {0}
         [54].f1 ∈ [--..--]
         [54].f2 ∈ {0}
         [55].f1 ∈ [--..--]
         [55].f2 ∈ {0}
         [56].f1 ∈ [--..--]
         [56].f2 ∈ {0}
         [57].f1 ∈ [--..--]
         [57].f2 ∈ {0}
         [58].f1 ∈ [--..--]
         [58].f2 ∈ {0}
         [59].f1 ∈ [--..--]
         [59].f2 ∈ {0}
         [60].f1 ∈ [--..--]
         [60].f2 ∈ {0}
         [61].f1 ∈ [--..--]
         [61].f2 ∈ {0}
         [62].f1 ∈ [--..--]
         [62].f2 ∈ {0}
         [63].f1 ∈ [--..--]
         [63].f2 ∈ {0}
         [64].f1 ∈ [--..--]
         [64].f2 ∈ {0}
         [65].f1 ∈ [--..--]
         [65].f2 ∈ {0}
         [66].f1 ∈ [--..--]
         [66].f2 ∈ {0}
         [67].f1 ∈ [--..--]
         [67].f2 ∈ {0}
         [68].f1 ∈ [--..--]
         [68].f2 ∈ {0}
         [69].f1 ∈ [--..--]
         [69].f2 ∈ {0}
         [70].f1 ∈ [--..--]
         [70].f2 ∈ {0}
         [71].f1 ∈ [--..--]
         [71].f2 ∈ {0}
         [72].f1 ∈ [--..--]
         [72].f2 ∈ {0}
         [73].f1 ∈ [--..--]
         [73].f2 ∈ {0}
         [74].f1 ∈ [--..--]
         [74].f2 ∈ {0}
         [75].f1 ∈ [--..--]
         [75].f2 ∈ {0}
         [76].f1 ∈ [--..--]
         [76].f2 ∈ {0}
         [77].f1 ∈ [--..--]
         [77].f2 ∈ {0}
         [78].f1 ∈ [--..--]
         [78].f2 ∈ {0}
         [79].f1 ∈ [--..--]
         [79].f2 ∈ {0}
         [80].f1 ∈ [--..--]
         [80].f2 ∈ {0}
         [81].f1 ∈ [--..--]
         [81].f2 ∈ {0}
         [82].f1 ∈ [--..--]
         [82].f2 ∈ {0}
         [83].f1 ∈ [--..--]
         [83].f2 ∈ {0}
         [84].f1 ∈ [--..--]
         [84].f2 ∈ {0}
         [85].f1 ∈ [--..--]
         [85].f2 ∈ {0}
         [86].f1 ∈ [--..--]
         [86].f2 ∈ {0}
         [87].f1 ∈ [--..--]
         [87].f2 ∈ {0}
         [88].f1 ∈ [--..--]
         [88].f2 ∈ {0}
         [89].f1 ∈ [--..--]
         [89].f2 ∈ {0}
         [90].f1 ∈ [--..--]
         [90].f2 ∈ {0}
         [91].f1 ∈ [--..--]
         [91].f2 ∈ {0}
         [92].f1 ∈ [--..--]
         [92].f2 ∈ {0}
         [93].f1 ∈ [--..--]
         [93].f2 ∈ {0}
         [94].f1 ∈ [--..--]
         [94].f2 ∈ {0}
         [95].f1 ∈ [--..--]
         [95].f2 ∈ {0}
         [96].f1 ∈ [--..--]
         [96].f2 ∈ {0}
         [97].f1 ∈ [--..--]
         [97].f2 ∈ {0}
         [98].f1 ∈ [--..--]
         [98].f2 ∈ {0}
         [99].f1 ∈ [--..--]
         [99].f2 ∈ {0}
[from] Computing for function main1
[from] Computing for function F1 <-main1
[from] Done for function F1
[from] Computing for function f <-main1
[from] Done for function f
[from] Computing for function g <-main1
[from] Done for function g
[from] Computing for function h <-main1
[from] Done for function h
[from] Computing for function j <-main1
[from] Done for function j
[from] Computing for function assigns_post <-main1
[from] Done for function assigns_post
[from] Done for function main1
[from] Computing for function main2
[from] Computing for function ff1 <-main2
[from] Done for function ff1
[from] Computing for function ff3 <-main2
[from] Done for function ff3
[from] Computing for function ff4 <-main2
[from] Done for function ff4
[from] Computing for function ff5 <-main2
[from] Done for function ff5
[from] Computing for function ff2 <-main2
[from] Done for function ff2
[from] Computing for function ff2_bis <-main2
[from] Done for function ff2_bis
[from] Done for function main2
[from] Computing for function main4
[from] Computing for function f_main4_1 <-main4
tests/value/assigns.i:104:[kernel] more than 200(1000) dependencies to update. Approximating.
[from] Done for function f_main4_1
[from] Computing for function f_main4_2 <-main4
tests/value/assigns.i:105:[kernel] more than 200(1000) dependencies to update. Approximating.
[from] Done for function f_main4_2
[from] Done for function main4
[from] Computing for function main
[from] Computing for function main3 <-main
[from] Done for function main3
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function F1:
  T[0..99] FROM T[0..99] (and SELF)
[from] Function assigns_post:
  Tpost{[18]; [53]} FROM ANYTHING(origin:Unknown) (and SELF)
  x FROM x (and SELF)
[from] Function f:
  t{[0].f2; [1..5]} FROM t{[1..5]; [6].f1} (and SELF)
[from] Function f_main4_1:
  t_main4{[0..998]; [999].f1} FROM \nothing (and SELF)
  u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
          [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
          [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
          [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
          [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
          [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
          [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
          [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
          [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
          [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
          [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
          [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
          [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
          [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
          [99].f1}
         FROM \nothing (and SELF)
[from] Function f_main4_2:
  t_main4{[0..998]; [999].f1} FROM \nothing (and SELF)
  u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
          [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
          [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
          [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
          [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
          [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
          [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
          [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
          [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
          [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
          [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
          [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
          [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
          [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
          [99].f1}
         FROM \nothing
[from] Function ff1:
  \result FROM ANYTHING(origin:Unknown)
[from] Function ff2:
  \result FROM \nothing
[from] Function ff2_bis:
  \result FROM ANYTHING(origin:Unknown)
[from] Function ff3:
  y1 FROM ANYTHING(origin:Unknown) (and SELF)
  y2 FROM y2 (and SELF)
  y3 FROM ANYTHING(origin:Unknown) (and SELF)
[from] Function ff4:
  NO EFFECTS
[from] Function ff5:
  \result FROM \nothing
[from] Function g:
  t2[0..99999] FROM \nothing (and SELF)
[from] Function h:
  t3[0..99999] FROM \nothing (and SELF)
[from] Function j:
  T[9..96] FROM \nothing (and SELF)
[from] Function main1:
  T[0..99] FROM T[0..99] (and SELF)
  Tpost{[18]; [53]} FROM ANYTHING(origin:Unknown) (and SELF)
  t{[0].f2; [1..5]} FROM t{[1..5]; [6].f1} (and SELF)
  t2[0..99999] FROM \nothing (and SELF)
  t3[0..99999] FROM \nothing (and SELF)
  x FROM x (and SELF)
[from] Function main2:
  y1 FROM ANYTHING(origin:Unknown) (and SELF)
  y2 FROM y2 (and SELF)
  y3 FROM ANYTHING(origin:Unknown) (and SELF)
  \result FROM \nothing
[from] Function main3:
  t_main3_1[0][0..7]
           FROM t_main3_1[0][0..7]; t_main3_2[0..2][0..3][0..4] (and SELF)
  t_main3_2[0..2][0..3][0..4] FROM t_main3_1[0][0..7];
                                   t_main3_2[0..2][0..3][0..4] (and SELF)
  \result FROM t_main3_1[0][0..7]; t_main3_2[0..2][0..3][0..4]
[from] Function main4:
  t_main4{[0..998]; [999].f1} FROM \nothing (and SELF)
  u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
          [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
          [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
          [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
          [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
          [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
          [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
          [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
          [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
          [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
          [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
          [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
          [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
          [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
          [99].f1}
         FROM \nothing
[from] Function main:
  T[0..99] FROM T[0..99] (and SELF)
  Tpost{[18]; [53]} FROM ANYTHING(origin:Unknown) (and SELF)
  t{[0].f2; [1..5]} FROM t{[1..5]; [6].f1} (and SELF)
  t2[0..99999] FROM \nothing (and SELF)
  t3[0..99999] FROM \nothing (and SELF)
  x FROM x (and SELF)
  y1 FROM ANYTHING(origin:Unknown) (and SELF)
  y2 FROM y2 (and SELF)
  y3 FROM ANYTHING(origin:Unknown) (and SELF)
  t_main3_1[0][0..7]
           FROM t_main3_1[0][0..7]; t_main3_2[0..2][0..3][0..4] (and SELF)
  t_main3_2[0..2][0..3][0..4] FROM t_main3_1[0][0..7];
                                   t_main3_2[0..2][0..3][0..4] (and SELF)
  t_main4{[0..998]; [999].f1} FROM \nothing (and SELF)
  u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
          [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
          [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
          [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
          [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
          [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
          [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
          [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
          [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
          [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
          [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
          [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
          [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
          [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
          [99].f1}
         FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
          T[0..99]; Tpost{[18]; [53]}; t{[0].f2; [1..5]}; t2[0..99999]; t3[0..99999];
          x; i
[inout] Inputs for function main1:
          ANYTHING(origin:Unknown)
[inout] InOut (internal) for function main1:
        Operational inputs:
          ANYTHING(origin:Unknown)
        Operational inputs on termination:
          ANYTHING(origin:Unknown)
        Sure outputs:
          i
[inout] Out (internal) for function main2:
          y1; y2; y3; l; p; q; __retres
[inout] Inputs for function main2:
          ANYTHING(origin:Unknown)
[inout] InOut (internal) for function main2:
        Operational inputs:
          ANYTHING(origin:Unknown)
        Operational inputs on termination:
          ANYTHING(origin:Unknown)
        Sure outputs:
          l; p; q; __retres
[inout] Out (internal) for function main4:
          t_main4{[0..998]; [999].f1};
          u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
                  [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
                  [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
                  [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
                  [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
                  [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
                  [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
                  [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
                  [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
                  [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
                  [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
                  [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
                  [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
                  [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
                  [99].f1}
[inout] Inputs for function main4:
          v
[inout] InOut (internal) for function main4:
        Operational inputs:
          v
        Operational inputs on termination:
          v
        Sure outputs:
          u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
                  [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
                  [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
                  [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
                  [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
                  [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
                  [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
                  [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
                  [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
                  [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
                  [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
                  [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
                  [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
                  [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
                  [99].f1}
[inout] Out (internal) for function main:
          T[0..99]; Tpost{[18]; [53]}; t{[0].f2; [1..5]}; t2[0..99999]; t3[0..99999];
          x; y1; y2; y3; t_main3_1[0][0..7]; t_main3_2[0..2][0..3][0..4];
          t_main4{[0..998]; [999].f1};
          u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
                  [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
                  [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
                  [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
                  [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
                  [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
                  [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
                  [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
                  [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
                  [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
                  [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
                  [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
                  [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
                  [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
                  [99].f1}
[inout] Inputs for function main:
          ANYTHING(origin:Unknown)
[inout] InOut (internal) for function main:
        Operational inputs:
          ANYTHING(origin:Unknown)
        Operational inputs on termination:
          ANYTHING(origin:Unknown)
        Sure outputs:
          u_main4{[0].f1; [1].f1; [2].f1; [3].f1; [4].f1; [5].f1; [6].f1; [7].f1;
                  [8].f1; [9].f1; [10].f1; [11].f1; [12].f1; [13].f1; [14].f1;
                  [15].f1; [16].f1; [17].f1; [18].f1; [19].f1; [20].f1; [21].f1;
                  [22].f1; [23].f1; [24].f1; [25].f1; [26].f1; [27].f1; [28].f1;
                  [29].f1; [30].f1; [31].f1; [32].f1; [33].f1; [34].f1; [35].f1;
                  [36].f1; [37].f1; [38].f1; [39].f1; [40].f1; [41].f1; [42].f1;
                  [43].f1; [44].f1; [45].f1; [46].f1; [47].f1; [48].f1; [49].f1;
                  [50].f1; [51].f1; [52].f1; [53].f1; [54].f1; [55].f1; [56].f1;
                  [57].f1; [58].f1; [59].f1; [60].f1; [61].f1; [62].f1; [63].f1;
                  [64].f1; [65].f1; [66].f1; [67].f1; [68].f1; [69].f1; [70].f1;
                  [71].f1; [72].f1; [73].f1; [74].f1; [75].f1; [76].f1; [77].f1;
                  [78].f1; [79].f1; [80].f1; [81].f1; [82].f1; [83].f1; [84].f1;
                  [85].f1; [86].f1; [87].f1; [88].f1; [89].f1; [90].f1; [91].f1;
                  [92].f1; [93].f1; [94].f1; [95].f1; [96].f1; [97].f1; [98].f1;
                  [99].f1}
/* Generated by Frama-C */
struct __anonstruct_ts_1 {
   int f1 ;
   int f2 ;
};
typedef struct __anonstruct_ts_1 ts;
int volatile v;
int G;
/*@ assigns *(s + (..));
    assigns *(s + (..)) \from *(s + (..)); */
extern void F1(char *s);

char T[100];
char Tpost[100];
ts t[10];
int t2[100000];
int t3[100000];
/*@ assigns *(p + (0 .. 3));
    assigns *(p + (0 .. 3)) \from *(p + (4 .. 7));
 */
extern void f(char *p);

/*@ assigns t2[(unsigned char)len + 1 .. (unsigned char)len + 1];
    assigns t2[(unsigned char)len + 1 .. (unsigned char)len + 1]
      \from \nothing;
 */
extern void g(int len);

/*@ assigns *(p + (..));
    assigns *(p + (..)) \from \nothing; */
extern void h(int *p);

/*@ logic int foo(int p) ;
 */
/*@ assigns *(p + (0 .. foo(*p)));
    assigns *(p + (0 .. foo(*p))) \from \nothing;
 */
extern void j(int *p);

int x;
int k = 53;
/*@ assigns \at(x,Post), Tpost[\at(\old(i),Post)], Tpost[\at(k,Post)];
    assigns \at(x,Post) \from \at(x,Post);
 */
extern void assigns_post(int i);

void main1(void)
{
  F1(T);
  {
    int i;
    i = 0;
    while (i <= 5) {
      f((char *)(& t[i].f2));
      i ++;
    }
  }
  /*@ assert Value: signed_overflow: -2147483648 ≤ 2 * (int)(&T); */
  /*@ assert Value: signed_overflow: 2 * (int)(&T) ≤ 2147483647; */
  g(2 * (int)(& T));
  /*@ assert Value: signed_overflow: -2147483648 ≤ 2 * (int)(&t3); */
  /*@ assert Value: signed_overflow: 2 * (int)(&t3) ≤ 2147483647; */
  h((int *)(2 * (int)(& t3)));
  j((int *)(& T[9]));
  assigns_post(18);
  return;
}

/*@ assigns \nothing; */
extern int ff1();

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int *ff2();

/*@ assigns \nothing; */
extern int *ff2_bis();

int y1;
int y2;
int y3;
/*@ assigns y1, y2, y3;
    assigns y2 \from y2; */
extern void ff3();

/*@ assigns \nothing; */
extern void ff4();

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int ff5();

int main2(void)
{
  int __retres;
  int l;
  int *p;
  int *q;
  l = ff1();
  ff3();
  ff4();
  ff5();
  p = ff2();
  q = ff2_bis();
  /*@ assert
      Value: ptr_comparison: \pointer_comparable((void *)p, (void *)(&x));
  */
  if (p != & x) {
    __retres = 1;
    goto return_label;
  }
  __retres = 0;
  return_label: return __retres;
}

int t_main3_1[7][8];
int t_main3_2[3][4][5];
/*@ assigns \result, (*a)[0 .. 7], (*(b + (0 .. 2)))[0 .. 3][0 .. 4];
    assigns \result \from (*a)[0 .. 7], (*(b + (0 .. 2)))[0 .. 3][0 .. 4];
    assigns (*a)[0 .. 7]
      \from (*a)[0 .. 7], (*(b + (0 .. 2)))[0 .. 3][0 .. 4];
    assigns (*(b + (0 .. 2)))[0 .. 3][0 .. 4]
      \from (*a)[0 .. 7], (*(b + (0 .. 2)))[0 .. 3][0 .. 4];
 */
extern int main3(int (*a)[8], int (* /*[3]*/ b)[4][5]);

ts t_main4[1000];
ts u_main4[100];
/*@ assigns t_main4[i].f1, u_main4[i].f1;
    assigns t_main4[i].f1 \from \nothing;
    assigns u_main4[i].f1 \from \nothing;
 */
extern void f_main4_1(int i);

/*@ assigns t_main4[0 .. 999].f1, u_main4[0 .. 99].f1;
    assigns t_main4[0 .. 999].f1 \from \nothing;
    assigns u_main4[0 .. 99].f1 \from \nothing;
 */
extern void f_main4_2();

void main4(void)
{
  f_main4_1(v);
  f_main4_2();
  return;
}

void main(void)
{
  main1();
  main2();
  main3(t_main3_1,t_main3_2);
  main4();
  return;
}