Skip to content
Snippets Groups Projects
Commit 50db0caa authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'fix/eva/recursion-test' into 'master' 

[Eva] Do not run the recursion test with the apron ptests config.

See merge request frama-c/frama-c!3156
parents 0f94bac7 ab58a0ff
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 187 additions and 1332 deletions
tests/value/oracle/recursion.0.res.oracle
+ 102
− 102
View file @ 50db0caa
...@@ -5,256 +5,256 @@ ...@@ -5,256 +5,256 @@
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
nondet ∈ [--..--] nondet ∈ [--..--]
p ∈ {0} p ∈ {0}
[eva:recursion] tests/value/recursion.c:18: [eva:recursion] tests/value/recursion.c:21:
detected recursive call of function five. detected recursive call of function five.
[eva] tests/value/recursion.c:18: Warning: [eva] tests/value/recursion.c:21: Warning:
Using specification of function five for recursive calls. Using specification of function five for recursive calls.
Analysis of function five is thus incomplete and its soundness Analysis of function five is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function five [eva] using specification for function five
[eva:alarm] tests/value/recursion.c:15: Warning: [eva:alarm] tests/value/recursion.c:18: Warning:
function five: postcondition got status unknown. function five: postcondition got status unknown.
[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5} [eva] tests/value/recursion.c:345: Frama_C_show_each_5: {5}
[eva:recursion] tests/value/recursion.c:28: [eva:recursion] tests/value/recursion.c:31:
detected recursive call of function sum. detected recursive call of function sum.
[eva] tests/value/recursion.c:28: Warning: [eva] tests/value/recursion.c:31: Warning:
Using specification of function sum for recursive calls. Using specification of function sum for recursive calls.
Analysis of function sum is thus incomplete and its soundness Analysis of function sum is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function sum [eva] using specification for function sum
[eva:alarm] tests/value/recursion.c:24: Warning: [eva:alarm] tests/value/recursion.c:27: Warning:
function sum: postcondition got status unknown. function sum: postcondition got status unknown.
[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91} [eva] tests/value/recursion.c:347: Frama_C_show_each_91: {91}
[eva:recursion] tests/value/recursion.c:37: [eva:recursion] tests/value/recursion.c:40:
detected recursive call of function factorial. detected recursive call of function factorial.
[eva] tests/value/recursion.c:37: Warning: [eva] tests/value/recursion.c:40: Warning:
Using specification of function factorial for recursive calls. Using specification of function factorial for recursive calls.
Analysis of function factorial is thus incomplete and its soundness Analysis of function factorial is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function factorial [eva] using specification for function factorial
[eva] tests/value/recursion.c:346: Frama_C_show_each_120: [0..4294967295] [eva] tests/value/recursion.c:349: Frama_C_show_each_120: [0..4294967295]
[eva:recursion] tests/value/recursion.c:46: [eva:recursion] tests/value/recursion.c:49:
detected recursive call of function syracuse. detected recursive call of function syracuse.
[eva] tests/value/recursion.c:46: Warning: [eva] tests/value/recursion.c:49: Warning:
Using specification of function syracuse for recursive calls. Using specification of function syracuse for recursive calls.
Analysis of function syracuse is thus incomplete and its soundness Analysis of function syracuse is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function syracuse [eva] using specification for function syracuse
[eva] tests/value/recursion.c:348: Frama_C_show_each_1: [0..4294967294] [eva] tests/value/recursion.c:351: Frama_C_show_each_1: [0..4294967294]
[eva:recursion] tests/value/recursion.c:59: [eva:recursion] tests/value/recursion.c:62:
detected recursive call of function fibonacci. detected recursive call of function fibonacci.
[eva] tests/value/recursion.c:59: Warning: [eva] tests/value/recursion.c:62: Warning:
Using specification of function fibonacci for recursive calls. Using specification of function fibonacci for recursive calls.
Analysis of function fibonacci is thus incomplete and its soundness Analysis of function fibonacci is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function fibonacci [eva] using specification for function fibonacci
[eva:recursion] tests/value/recursion.c:60: [eva:recursion] tests/value/recursion.c:63:
detected recursive call of function fibonacci. detected recursive call of function fibonacci.
[eva] tests/value/recursion.c:60: Warning: [eva] tests/value/recursion.c:63: Warning:
Using specification of function fibonacci for recursive calls. Using specification of function fibonacci for recursive calls.
Analysis of function fibonacci is thus incomplete and its soundness Analysis of function fibonacci is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] tests/value/recursion.c:350: Frama_C_show_each_89: [0..4294967295] [eva] tests/value/recursion.c:353: Frama_C_show_each_89: [0..4294967295]
[eva:recursion] tests/value/recursion.c:76: [eva:recursion] tests/value/recursion.c:79:
detected recursive call of function sum_ptr. detected recursive call of function sum_ptr.
[eva] tests/value/recursion.c:76: Warning: [eva] tests/value/recursion.c:79: Warning:
Using specification of function sum_ptr for recursive calls. Using specification of function sum_ptr for recursive calls.
Analysis of function sum_ptr is thus incomplete and its soundness Analysis of function sum_ptr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function sum_ptr [eva] using specification for function sum_ptr
[eva:alarm] tests/value/recursion.c:68: Warning: [eva:alarm] tests/value/recursion.c:71: Warning:
function sum_ptr: postcondition got status unknown. function sum_ptr: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:69: Warning: [eva:alarm] tests/value/recursion.c:72: Warning:
function sum_ptr: postcondition got status unknown. function sum_ptr: postcondition got status unknown.
[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91} [eva] tests/value/recursion.c:358: Frama_C_show_each_91: {91}
[eva:recursion] tests/value/recursion.c:89: [eva:recursion] tests/value/recursion.c:92:
detected recursive call of function factorial_ptr. detected recursive call of function factorial_ptr.
[eva] tests/value/recursion.c:89: Warning: [eva] tests/value/recursion.c:92: Warning:
Using specification of function factorial_ptr for recursive calls. Using specification of function factorial_ptr for recursive calls.
Analysis of function factorial_ptr is thus incomplete and its soundness Analysis of function factorial_ptr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function factorial_ptr [eva] using specification for function factorial_ptr
[eva:alarm] tests/value/recursion.c:90: Warning: [eva:alarm] tests/value/recursion.c:93: Warning:
accessing uninitialized left-value. assert \initialized(&res); accessing uninitialized left-value. assert \initialized(&res);
[eva] tests/value/recursion.c:358: Frama_C_show_each_120: [0..4294967295] [eva] tests/value/recursion.c:361: Frama_C_show_each_120: [0..4294967295]
[eva:recursion] tests/value/recursion.c:101: [eva:recursion] tests/value/recursion.c:104:
detected recursive call of function syracuse_ptr. detected recursive call of function syracuse_ptr.
[eva] tests/value/recursion.c:101: Warning: [eva] tests/value/recursion.c:104: Warning:
Using specification of function syracuse_ptr for recursive calls. Using specification of function syracuse_ptr for recursive calls.
Analysis of function syracuse_ptr is thus incomplete and its soundness Analysis of function syracuse_ptr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function syracuse_ptr [eva] using specification for function syracuse_ptr
[eva:alarm] tests/value/recursion.c:102: Warning: [eva:alarm] tests/value/recursion.c:105: Warning:
accessing uninitialized left-value. assert \initialized(&prev_res); accessing uninitialized left-value. assert \initialized(&prev_res);
[eva] tests/value/recursion.c:361: Frama_C_show_each_1: [0..4294967294] [eva] tests/value/recursion.c:364: Frama_C_show_each_1: [0..4294967294]
[eva:recursion] tests/value/recursion.c:117: [eva:recursion] tests/value/recursion.c:120:
detected recursive call of function fibonacci_ptr. detected recursive call of function fibonacci_ptr.
[eva] tests/value/recursion.c:117: Warning: [eva] tests/value/recursion.c:120: Warning:
Using specification of function fibonacci_ptr for recursive calls. Using specification of function fibonacci_ptr for recursive calls.
Analysis of function fibonacci_ptr is thus incomplete and its soundness Analysis of function fibonacci_ptr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function fibonacci_ptr [eva] using specification for function fibonacci_ptr
[eva:recursion] tests/value/recursion.c:119: [eva:recursion] tests/value/recursion.c:122:
detected recursive call of function fibonacci_ptr. detected recursive call of function fibonacci_ptr.
[eva] tests/value/recursion.c:119: Warning: [eva] tests/value/recursion.c:122: Warning:
Using specification of function fibonacci_ptr for recursive calls. Using specification of function fibonacci_ptr for recursive calls.
Analysis of function fibonacci_ptr is thus incomplete and its soundness Analysis of function fibonacci_ptr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva:alarm] tests/value/recursion.c:120: Warning: [eva:alarm] tests/value/recursion.c:123: Warning:
accessing uninitialized left-value. assert \initialized(&x); accessing uninitialized left-value. assert \initialized(&x);
[eva:alarm] tests/value/recursion.c:120: Warning: [eva:alarm] tests/value/recursion.c:123: Warning:
accessing uninitialized left-value. assert \initialized(&y); accessing uninitialized left-value. assert \initialized(&y);
[eva] tests/value/recursion.c:364: Frama_C_show_each_89: [0..4294967295] [eva] tests/value/recursion.c:367: Frama_C_show_each_89: [0..4294967295]
[eva:recursion] tests/value/recursion.c:137: [eva:recursion] tests/value/recursion.c:140:
detected recursive call of function sum_and_fact. detected recursive call of function sum_and_fact.
[eva] tests/value/recursion.c:137: Warning: [eva] tests/value/recursion.c:140: Warning:
Using specification of function sum_and_fact for recursive calls. Using specification of function sum_and_fact for recursive calls.
Analysis of function sum_and_fact is thus incomplete and its soundness Analysis of function sum_and_fact is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function sum_and_fact [eva] using specification for function sum_and_fact
[eva:alarm] tests/value/recursion.c:128: Warning: [eva:alarm] tests/value/recursion.c:131: Warning:
function sum_and_fact: postcondition got status unknown. function sum_and_fact: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:129: Warning: [eva:alarm] tests/value/recursion.c:132: Warning:
function sum_and_fact: postcondition got status unknown. function sum_and_fact: postcondition got status unknown.
[eva] tests/value/recursion.c:368: [eva] tests/value/recursion.c:371:
Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8 Frama_C_show_each_36_40320: {36}, [0..4294967288],0%8
[eva:recursion] tests/value/recursion.c:161: [eva:recursion] tests/value/recursion.c:164:
detected recursive call of function odd. detected recursive call of function odd.
[eva] tests/value/recursion.c:161: Warning: [eva] tests/value/recursion.c:164: Warning:
Using specification of function odd for recursive calls. Using specification of function odd for recursive calls.
Analysis of function odd is thus incomplete and its soundness Analysis of function odd is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function odd [eva] using specification for function odd
[eva:alarm] tests/value/recursion.c:149: Warning: [eva:alarm] tests/value/recursion.c:152: Warning:
function odd: postcondition got status unknown. function odd: postcondition got status unknown.
[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1} [eva] tests/value/recursion.c:376: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0} [eva] tests/value/recursion.c:379: Frama_C_show_each_0: {0}, {0}
[eva:recursion] tests/value/recursion.c:183: [eva:recursion] tests/value/recursion.c:186:
detected recursive call of function odd_ptr. detected recursive call of function odd_ptr.
[eva] tests/value/recursion.c:183: Warning: [eva] tests/value/recursion.c:186: Warning:
Using specification of function odd_ptr for recursive calls. Using specification of function odd_ptr for recursive calls.
Analysis of function odd_ptr is thus incomplete and its soundness Analysis of function odd_ptr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function odd_ptr [eva] using specification for function odd_ptr
[eva:alarm] tests/value/recursion.c:167: Warning: [eva:alarm] tests/value/recursion.c:170: Warning:
function odd_ptr: postcondition got status unknown. function odd_ptr: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:184: Warning: [eva:alarm] tests/value/recursion.c:187: Warning:
accessing uninitialized left-value. assert \initialized(&y); accessing uninitialized left-value. assert \initialized(&y);
[eva:alarm] tests/value/recursion.c:179: Warning: [eva:alarm] tests/value/recursion.c:182: Warning:
function even_ptr: postcondition got status unknown. function even_ptr: postcondition got status unknown.
[eva:recursion] tests/value/recursion.c:171: [eva:recursion] tests/value/recursion.c:174:
detected recursive call of function even_ptr. detected recursive call of function even_ptr.
[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1} [eva] tests/value/recursion.c:382: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0} [eva] tests/value/recursion.c:385: Frama_C_show_each_0: {0}, {0}
[eva] using specification for function Frama_C_interval [eva] using specification for function Frama_C_interval
[eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
[eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66] [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
[eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [0..4294967295] [eva] tests/value/recursion.c:394: Frama_C_show_each_6_66: [6..66]
[eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [0..4294967295] [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [0..4294967295]
[eva:alarm] tests/value/recursion.c:222: Warning: [eva] tests/value/recursion.c:400: Frama_C_show_each_2_89: [0..4294967295]
[eva:alarm] tests/value/recursion.c:225: Warning:
function fill_array: precondition got status invalid. function fill_array: precondition got status invalid.
[eva:alarm] tests/value/recursion.c:226: Warning: [eva:alarm] tests/value/recursion.c:229: Warning:
function fill_array: precondition got status unknown. function fill_array: precondition got status unknown.
[eva:recursion] tests/value/recursion.c:200: [eva:recursion] tests/value/recursion.c:203:
detected recursive call of function fill_array. detected recursive call of function fill_array.
[eva] tests/value/recursion.c:200: Warning: [eva] tests/value/recursion.c:203: Warning:
Using specification of function fill_array for recursive calls. Using specification of function fill_array for recursive calls.
Analysis of function fill_array is thus incomplete and its soundness Analysis of function fill_array is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function fill_array [eva] using specification for function fill_array
[eva:alarm] tests/value/recursion.c:200: Warning: [eva:alarm] tests/value/recursion.c:203: Warning:
function fill_array: precondition got status unknown. function fill_array: precondition got status unknown.
[eva:alarm] tests/value/recursion.c:194: Warning: [eva:alarm] tests/value/recursion.c:197: Warning:
function fill_array: postcondition got status unknown. function fill_array: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:228: Warning: [eva:alarm] tests/value/recursion.c:231: Warning:
function binary_search: precondition \initialized(data + (start .. end)) got status unknown. function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
[eva:recursion] tests/value/recursion.c:214: [eva:recursion] tests/value/recursion.c:217:
detected recursive call of function binary_search. detected recursive call of function binary_search.
[eva] tests/value/recursion.c:214: Warning: [eva] tests/value/recursion.c:217: Warning:
Using specification of function binary_search for recursive calls. Using specification of function binary_search for recursive calls.
Analysis of function binary_search is thus incomplete and its soundness Analysis of function binary_search is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function binary_search [eva] using specification for function binary_search
[eva:recursion] tests/value/recursion.c:216: [eva:recursion] tests/value/recursion.c:219:
detected recursive call of function binary_search. detected recursive call of function binary_search.
[eva] tests/value/recursion.c:216: Warning: [eva] tests/value/recursion.c:219: Warning:
Using specification of function binary_search for recursive calls. Using specification of function binary_search for recursive calls.
Analysis of function binary_search is thus incomplete and its soundness Analysis of function binary_search is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] tests/value/recursion.c:229: [eva] tests/value/recursion.c:232:
Frama_C_show_each_3: [-2147483648..2147483647] Frama_C_show_each_3: [-2147483648..2147483647]
[eva] tests/value/recursion.c:231: [eva] tests/value/recursion.c:234:
Frama_C_show_each_12: [-2147483648..2147483647] Frama_C_show_each_12: [-2147483648..2147483647]
[eva] tests/value/recursion.c:233: [eva] tests/value/recursion.c:236:
Frama_C_show_each_minus1: [-2147483648..2147483647] Frama_C_show_each_minus1: [-2147483648..2147483647]
[eva] tests/value/recursion.c:238:
Frama_C_show_each_7_11: [-2147483648..2147483647]
[eva] tests/value/recursion.c:241: [eva] tests/value/recursion.c:241:
Frama_C_show_each_7_11: [-2147483648..2147483647]
[eva] tests/value/recursion.c:244:
Frama_C_show_each_minus_1_15: [-2147483648..2147483647] Frama_C_show_each_minus_1_15: [-2147483648..2147483647]
[eva:recursion] tests/value/recursion.c:252: [eva:recursion] tests/value/recursion.c:255:
detected recursive call of function alarm. detected recursive call of function alarm.
[eva] tests/value/recursion.c:252: Warning: [eva] tests/value/recursion.c:255: Warning:
Using specification of function alarm for recursive calls. Using specification of function alarm for recursive calls.
Analysis of function alarm is thus incomplete and its soundness Analysis of function alarm is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function alarm [eva] using specification for function alarm
[eva:alarm] tests/value/recursion.c:247: Warning: [eva:alarm] tests/value/recursion.c:250: Warning:
function alarm: postcondition got status unknown. function alarm: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:252: Warning: [eva:alarm] tests/value/recursion.c:255: Warning:
signed overflow. assert i * tmp ≤ 2147483647; signed overflow. assert i * tmp ≤ 2147483647;
(tmp from alarm(i - 1)) (tmp from alarm(i - 1))
[eva] tests/value/recursion.c:406: [eva] tests/value/recursion.c:409:
Frama_C_show_each_unreachable: [20..2147483640],0%20 Frama_C_show_each_unreachable: [20..2147483640],0%20
[eva:recursion] tests/value/recursion.c:261: [eva:recursion] tests/value/recursion.c:264:
detected recursive call of function precond. detected recursive call of function precond.
[eva] tests/value/recursion.c:261: Warning: [eva] tests/value/recursion.c:264: Warning:
Using specification of function precond for recursive calls. Using specification of function precond for recursive calls.
Analysis of function precond is thus incomplete and its soundness Analysis of function precond is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[inout] Warning: no assigns clauses for function precond. [inout] Warning: no assigns clauses for function precond.
Results will be imprecise. Results will be imprecise.
[eva] using specification for function precond [eva] using specification for function precond
[eva] tests/value/recursion.c:261: Warning: [eva] tests/value/recursion.c:264: Warning:
Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect. Cannot handle empty assigns clause. Assuming assigns \nothing: be aware this is probably incorrect.
[eva:recursion] tests/value/recursion.c:276: [eva:recursion] tests/value/recursion.c:279:
detected recursive call of function escaping_local. detected recursive call of function escaping_local.
[eva] tests/value/recursion.c:276: Warning: [eva] tests/value/recursion.c:279: Warning:
Using specification of function escaping_local for recursive calls. Using specification of function escaping_local for recursive calls.
Analysis of function escaping_local is thus incomplete and its soundness Analysis of function escaping_local is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function escaping_local [eva] using specification for function escaping_local
[eva:alarm] tests/value/recursion.c:278: Warning: [eva:alarm] tests/value/recursion.c:281: Warning:
out of bounds write. assert \valid(p); out of bounds write. assert \valid(p);
[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {5} [eva] tests/value/recursion.c:282: Frama_C_show_each_1: {5}
[eva:locals-escaping] tests/value/recursion.c:277: Warning: [eva:locals-escaping] tests/value/recursion.c:280: Warning:
locals {x} escaping the scope of a block of escaping_local through p locals {x} escaping the scope of a block of escaping_local through p
[eva:recursion] tests/value/recursion.c:291: [eva:recursion] tests/value/recursion.c:294:
detected recursive call of function escaping_formal. detected recursive call of function escaping_formal.
[eva] tests/value/recursion.c:291: Warning: [eva] tests/value/recursion.c:294: Warning:
Using specification of function escaping_formal for recursive calls. Using specification of function escaping_formal for recursive calls.
Analysis of function escaping_formal is thus incomplete and its soundness Analysis of function escaping_formal is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function escaping_formal [eva] using specification for function escaping_formal
[eva:alarm] tests/value/recursion.c:293: Warning: [eva:alarm] tests/value/recursion.c:296: Warning:
out of bounds write. assert \valid(p); out of bounds write. assert \valid(p);
[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {5} [eva] tests/value/recursion.c:297: Frama_C_show_each_1: {5}
[eva:locals-escaping] tests/value/recursion.c:411: Warning: [eva:locals-escaping] tests/value/recursion.c:414: Warning:
locals {x} escaping the scope of escaping_formal through p locals {x} escaping the scope of escaping_formal through p
[eva:recursion] tests/value/recursion.c:307: [eva:recursion] tests/value/recursion.c:310:
detected recursive call of function escaping_stack. detected recursive call of function escaping_stack.
[eva] tests/value/recursion.c:307: Warning: [eva] tests/value/recursion.c:310: Warning:
Using specification of function escaping_stack for recursive calls. Using specification of function escaping_stack for recursive calls.
Analysis of function escaping_stack is thus incomplete and its soundness Analysis of function escaping_stack is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function escaping_stack [eva] using specification for function escaping_stack
[eva:alarm] tests/value/recursion.c:309: Warning: [eva:alarm] tests/value/recursion.c:312: Warning:
out of bounds write. assert \valid(p); out of bounds write. assert \valid(p);
[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {5} [eva] tests/value/recursion.c:313: Frama_C_show_each_1_2: {5}
[eva:locals-escaping] tests/value/recursion.c:308: Warning: [eva:locals-escaping] tests/value/recursion.c:311: Warning:
locals {x} escaping the scope of a block of escaping_stack through p locals {x} escaping the scope of a block of escaping_stack through p
[eva:recursion] tests/value/recursion.c:323: [eva:recursion] tests/value/recursion.c:326:
detected recursive call of function decr. detected recursive call of function decr.
[eva] tests/value/recursion.c:323: Warning: [eva] tests/value/recursion.c:326: Warning:
Using specification of function decr for recursive calls. Using specification of function decr for recursive calls.
Analysis of function decr is thus incomplete and its soundness Analysis of function decr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
...@@ -276,7 +276,7 @@ ...@@ -276,7 +276,7 @@
[eva:final-states] Values at end of function escaping_stack: [eva:final-states] Values at end of function escaping_stack:
p ∈ p ∈
{{ garbled mix of &{a} {{ garbled mix of &{a}
(origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR (origin: Library function {tests/value/recursion.c:310}) }} or ESCAPINGADDR
a ∈ [--..--] a ∈ [--..--]
[eva:final-states] Values at end of function even: [eva:final-states] Values at end of function even:
__retres ∈ UNINITIALIZED __retres ∈ UNINITIALIZED
...@@ -349,7 +349,7 @@ Cannot filter: dumping raw memory (including unchanged variables) ...@@ -349,7 +349,7 @@ Cannot filter: dumping raw memory (including unchanged variables)
nondet ∈ [--..--] nondet ∈ [--..--]
p ∈ p ∈
{{ garbled mix of &{a} {{ garbled mix of &{a}
(origin: Library function {tests/value/recursion.c:307}) }} or ESCAPINGADDR (origin: Library function {tests/value/recursion.c:310}) }} or ESCAPINGADDR
a ∈ [--..--] a ∈ [--..--]
b ∈ {0} b ∈ {0}
x ∈ [10..20] x ∈ [10..20]
......
tests/value/oracle/recursion.1.res.oracle
+ 74
− 74
View file @ 50db0caa
...@@ -5,136 +5,136 @@ ...@@ -5,136 +5,136 @@
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
nondet ∈ [--..--] nondet ∈ [--..--]
p ∈ {0} p ∈ {0}
[eva:recursion] tests/value/recursion.c:18: [eva:recursion] tests/value/recursion.c:21:
detected recursive call of function five. detected recursive call of function five.
[eva] tests/value/recursion.c:18: Warning: [eva] tests/value/recursion.c:21: Warning:
Using specification of function five for recursive calls of depth 20. Using specification of function five for recursive calls of depth 20.
Analysis of function five is thus incomplete and its soundness Analysis of function five is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
[eva] using specification for function five [eva] using specification for function five
[eva:alarm] tests/value/recursion.c:15: Warning: [eva:alarm] tests/value/recursion.c:18: Warning:
function five: postcondition got status unknown. function five: postcondition got status unknown.
[eva] tests/value/recursion.c:342: Frama_C_show_each_5: {5} [eva] tests/value/recursion.c:345: Frama_C_show_each_5: {5}
[eva:recursion] tests/value/recursion.c:28: [eva:recursion] tests/value/recursion.c:31:
detected recursive call of function sum. detected recursive call of function sum.
[eva] tests/value/recursion.c:344: Frama_C_show_each_91: {91} [eva] tests/value/recursion.c:347: Frama_C_show_each_91: {91}
[eva:recursion] tests/value/recursion.c:37: [eva:recursion] tests/value/recursion.c:40:
detected recursive call of function factorial. detected recursive call of function factorial.
[eva] tests/value/recursion.c:346: Frama_C_show_each_120: {120} [eva] tests/value/recursion.c:349: Frama_C_show_each_120: {120}
[eva:recursion] tests/value/recursion.c:46: [eva:recursion] tests/value/recursion.c:49:
detected recursive call of function syracuse. detected recursive call of function syracuse.
[eva] tests/value/recursion.c:348: Frama_C_show_each_1: {1} [eva] tests/value/recursion.c:351: Frama_C_show_each_1: {1}
[eva:recursion] tests/value/recursion.c:59: [eva:recursion] tests/value/recursion.c:62:
detected recursive call of function fibonacci. detected recursive call of function fibonacci.
[eva:recursion] tests/value/recursion.c:60: [eva:recursion] tests/value/recursion.c:63:
detected recursive call of function fibonacci. detected recursive call of function fibonacci.
[eva] tests/value/recursion.c:350: Frama_C_show_each_89: {89} [eva] tests/value/recursion.c:353: Frama_C_show_each_89: {89}
[eva:recursion] tests/value/recursion.c:76: [eva:recursion] tests/value/recursion.c:79:
detected recursive call of function sum_ptr. detected recursive call of function sum_ptr.
[eva] tests/value/recursion.c:355: Frama_C_show_each_91: {91} [eva] tests/value/recursion.c:358: Frama_C_show_each_91: {91}
[eva:recursion] tests/value/recursion.c:89: [eva:recursion] tests/value/recursion.c:92:
detected recursive call of function factorial_ptr. detected recursive call of function factorial_ptr.
[eva] tests/value/recursion.c:358: Frama_C_show_each_120: {120} [eva] tests/value/recursion.c:361: Frama_C_show_each_120: {120}
[eva:recursion] tests/value/recursion.c:101: [eva:recursion] tests/value/recursion.c:104:
detected recursive call of function syracuse_ptr. detected recursive call of function syracuse_ptr.
[eva] tests/value/recursion.c:361: Frama_C_show_each_1: {1} [eva] tests/value/recursion.c:364: Frama_C_show_each_1: {1}
[eva:recursion] tests/value/recursion.c:117: [eva:recursion] tests/value/recursion.c:120:
detected recursive call of function fibonacci_ptr. detected recursive call of function fibonacci_ptr.
[eva:recursion] tests/value/recursion.c:119: [eva:recursion] tests/value/recursion.c:122:
detected recursive call of function fibonacci_ptr. detected recursive call of function fibonacci_ptr.
[eva] tests/value/recursion.c:364: Frama_C_show_each_89: {89} [eva] tests/value/recursion.c:367: Frama_C_show_each_89: {89}
[eva:recursion] tests/value/recursion.c:137: [eva:recursion] tests/value/recursion.c:140:
detected recursive call of function sum_and_fact. detected recursive call of function sum_and_fact.
[eva] tests/value/recursion.c:368: Frama_C_show_each_36_40320: {36}, {40320} [eva] tests/value/recursion.c:371: Frama_C_show_each_36_40320: {36}, {40320}
[eva:recursion] tests/value/recursion.c:161: [eva:recursion] tests/value/recursion.c:164:
detected recursive call of function odd. detected recursive call of function odd.
[eva:recursion] tests/value/recursion.c:152: [eva:recursion] tests/value/recursion.c:155:
detected recursive call of function even. detected recursive call of function even.
[eva] tests/value/recursion.c:373: Frama_C_show_each_1: {1}, {1} [eva] tests/value/recursion.c:376: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:376: Frama_C_show_each_0: {0}, {0} [eva] tests/value/recursion.c:379: Frama_C_show_each_0: {0}, {0}
[eva:recursion] tests/value/recursion.c:183: [eva:recursion] tests/value/recursion.c:186:
detected recursive call of function odd_ptr. detected recursive call of function odd_ptr.
[eva:recursion] tests/value/recursion.c:171: [eva:recursion] tests/value/recursion.c:174:
detected recursive call of function even_ptr. detected recursive call of function even_ptr.
[eva] tests/value/recursion.c:379: Frama_C_show_each_1: {1}, {1} [eva] tests/value/recursion.c:382: Frama_C_show_each_1: {1}, {1}
[eva] tests/value/recursion.c:382: Frama_C_show_each_0: {0}, {0} [eva] tests/value/recursion.c:385: Frama_C_show_each_0: {0}, {0}
[eva] using specification for function Frama_C_interval [eva] using specification for function Frama_C_interval
[eva:alarm] tests/value/recursion.c:24: Warning: [eva:alarm] tests/value/recursion.c:27: Warning:
function sum: postcondition got status unknown. function sum: postcondition got status unknown.
[eva] tests/value/recursion.c:388: Frama_C_show_each_6_66: [6..66]
[eva:alarm] tests/value/recursion.c:69: Warning:
function sum_ptr: postcondition got status unknown.
[eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66] [eva] tests/value/recursion.c:391: Frama_C_show_each_6_66: [6..66]
[eva] tests/value/recursion.c:394: Frama_C_show_each_2_89: [2..89] [eva:alarm] tests/value/recursion.c:72: Warning:
function sum_ptr: postcondition got status unknown.
[eva] tests/value/recursion.c:394: Frama_C_show_each_6_66: [6..66]
[eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [2..89] [eva] tests/value/recursion.c:397: Frama_C_show_each_2_89: [2..89]
[eva:alarm] tests/value/recursion.c:222: Warning: [eva] tests/value/recursion.c:400: Frama_C_show_each_2_89: [2..89]
[eva:alarm] tests/value/recursion.c:225: Warning:
function fill_array: precondition got status invalid. function fill_array: precondition got status invalid.
[eva:alarm] tests/value/recursion.c:226: Warning: [eva:alarm] tests/value/recursion.c:229: Warning:
function fill_array: precondition got status unknown. function fill_array: precondition got status unknown.
[eva:recursion] tests/value/recursion.c:200: [eva:recursion] tests/value/recursion.c:203:
detected recursive call of function fill_array. detected recursive call of function fill_array.
[eva:alarm] tests/value/recursion.c:200: Warning: [eva:alarm] tests/value/recursion.c:203: Warning:
function fill_array: precondition got status unknown. function fill_array: precondition got status unknown.
[eva:alarm] tests/value/recursion.c:199: Warning: [eva:alarm] tests/value/recursion.c:202: Warning:
out of bounds write. assert \valid(data + start); out of bounds write. assert \valid(data + start);
[kernel] tests/value/recursion.c:199: Warning: [kernel] tests/value/recursion.c:202: Warning:
all target addresses were invalid. This path is assumed to be dead. all target addresses were invalid. This path is assumed to be dead.
[eva:alarm] tests/value/recursion.c:194: Warning: [eva:alarm] tests/value/recursion.c:197: Warning:
function fill_array: postcondition got status unknown. function fill_array: postcondition got status unknown.
[eva:alarm] tests/value/recursion.c:228: Warning: [eva:alarm] tests/value/recursion.c:231: Warning:
function binary_search: precondition \initialized(data + (start .. end)) got status unknown. function binary_search: precondition \initialized(data + (start .. end)) got status unknown.
[eva:recursion] tests/value/recursion.c:214: [eva:recursion] tests/value/recursion.c:217:
detected recursive call of function binary_search. detected recursive call of function binary_search.
[eva] tests/value/recursion.c:229: Frama_C_show_each_3: {3} [eva] tests/value/recursion.c:232: Frama_C_show_each_3: {3}
[eva:recursion] tests/value/recursion.c:216: [eva:recursion] tests/value/recursion.c:219:
detected recursive call of function binary_search. detected recursive call of function binary_search.
[eva] tests/value/recursion.c:231: Frama_C_show_each_12: {12} [eva] tests/value/recursion.c:234: Frama_C_show_each_12: {12}
[eva] tests/value/recursion.c:233: Frama_C_show_each_minus1: {-1} [eva] tests/value/recursion.c:236: Frama_C_show_each_minus1: {-1}
[eva] tests/value/recursion.c:238: Frama_C_show_each_7_11: {7; 8; 9; 10; 11} [eva] tests/value/recursion.c:241: Frama_C_show_each_7_11: {7; 8; 9; 10; 11}
[eva] tests/value/recursion.c:241: Frama_C_show_each_minus_1_15: [-1..15] [eva] tests/value/recursion.c:244: Frama_C_show_each_minus_1_15: [-1..15]
[eva:recursion] tests/value/recursion.c:252: [eva:recursion] tests/value/recursion.c:255:
detected recursive call of function alarm. detected recursive call of function alarm.
[eva:alarm] tests/value/recursion.c:252: Warning: [eva:alarm] tests/value/recursion.c:255: Warning:
signed overflow. assert i * tmp ≤ 2147483647; signed overflow. assert i * tmp ≤ 2147483647;
(tmp from alarm(i - 1)) (tmp from alarm(i - 1))
[eva:recursion] tests/value/recursion.c:261: [eva:recursion] tests/value/recursion.c:264:
detected recursive call of function precond. detected recursive call of function precond.
[eva:alarm] tests/value/recursion.c:261: Warning: [eva:alarm] tests/value/recursion.c:264: Warning:
function precond: precondition got status invalid. function precond: precondition got status invalid.
[eva:recursion] tests/value/recursion.c:276: [eva:recursion] tests/value/recursion.c:279:
detected recursive call of function escaping_local. detected recursive call of function escaping_local.
[eva] tests/value/recursion.c:279: Frama_C_show_each_1: {1} [eva] tests/value/recursion.c:282: Frama_C_show_each_1: {1}
[eva:locals-escaping] tests/value/recursion.c:277: Warning: [eva:locals-escaping] tests/value/recursion.c:280: Warning:
locals {x} escaping the scope of a block of escaping_local through p locals {x} escaping the scope of a block of escaping_local through p
[eva:alarm] tests/value/recursion.c:278: Warning: [eva:alarm] tests/value/recursion.c:281: Warning:
accessing left-value that contains escaping addresses. accessing left-value that contains escaping addresses.
assert ¬\dangling(&p); assert ¬\dangling(&p);
[kernel] tests/value/recursion.c:278: Warning: [kernel] tests/value/recursion.c:281: Warning:
all target addresses were invalid. This path is assumed to be dead. all target addresses were invalid. This path is assumed to be dead.
[eva:recursion] tests/value/recursion.c:291: [eva:recursion] tests/value/recursion.c:294:
detected recursive call of function escaping_formal. detected recursive call of function escaping_formal.
[eva] tests/value/recursion.c:294: Frama_C_show_each_1: {1} [eva] tests/value/recursion.c:297: Frama_C_show_each_1: {1}
[eva:locals-escaping] tests/value/recursion.c:291: Warning: [eva:locals-escaping] tests/value/recursion.c:294: Warning:
locals {x} escaping the scope of escaping_formal through p locals {x} escaping the scope of escaping_formal through p
[eva:alarm] tests/value/recursion.c:293: Warning: [eva:alarm] tests/value/recursion.c:296: Warning:
accessing left-value that contains escaping addresses. accessing left-value that contains escaping addresses.
assert ¬\dangling(&p); assert ¬\dangling(&p);
[kernel] tests/value/recursion.c:293: Warning: [kernel] tests/value/recursion.c:296: Warning:
all target addresses were invalid. This path is assumed to be dead. all target addresses were invalid. This path is assumed to be dead.
[eva:recursion] tests/value/recursion.c:307: [eva:recursion] tests/value/recursion.c:310:
detected recursive call of function escaping_stack. detected recursive call of function escaping_stack.
[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {1} [eva] tests/value/recursion.c:313: Frama_C_show_each_1_2: {1}
[eva] tests/value/recursion.c:310: Frama_C_show_each_1_2: {2} [eva] tests/value/recursion.c:313: Frama_C_show_each_1_2: {2}
[eva:locals-escaping] tests/value/recursion.c:308: Warning: [eva:locals-escaping] tests/value/recursion.c:311: Warning:
locals {x} escaping the scope of a block of escaping_stack through p locals {x} escaping the scope of a block of escaping_stack through p
[eva:alarm] tests/value/recursion.c:309: Warning: [eva:alarm] tests/value/recursion.c:312: Warning:
accessing left-value that contains escaping addresses. accessing left-value that contains escaping addresses.
assert ¬\dangling(&p); assert ¬\dangling(&p);
[kernel] tests/value/recursion.c:309: Warning: [kernel] tests/value/recursion.c:312: Warning:
all target addresses were invalid. This path is assumed to be dead. all target addresses were invalid. This path is assumed to be dead.
[eva:recursion] tests/value/recursion.c:323: [eva:recursion] tests/value/recursion.c:326:
detected recursive call of function decr. detected recursive call of function decr.
[eva] tests/value/recursion.c:323: Warning: [eva] tests/value/recursion.c:326: Warning:
Using specification of function decr for recursive calls of depth 20. Using specification of function decr for recursive calls of depth 20.
Analysis of function decr is thus incomplete and its soundness Analysis of function decr is thus incomplete and its soundness
relies on the written specification. relies on the written specification.
......
tests/value/oracle/recursion.2.res.oracle
+ 4
− 4
View file @ 50db0caa
...@@ -5,12 +5,12 @@ ...@@ -5,12 +5,12 @@
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
nondet ∈ [--..--] nondet ∈ [--..--]
p ∈ {0} p ∈ {0}
[eva:recursion] tests/value/recursion.c:422: [eva:recursion] tests/value/recursion.c:425:
detected recursive call of function sum_nospec. detected recursive call of function sum_nospec.
[eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10} [eva] tests/value/recursion.c:432: Frama_C_show_each_10: {10}
[eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36} [eva] tests/value/recursion.c:437: Frama_C_show_each_36: {36}
[eva] using specification for function Frama_C_interval [eva] using specification for function Frama_C_interval
[eva] tests/value/recursion.c:422: User Error: [eva] tests/value/recursion.c:425: User Error:
Recursive call to sum_nospec without a specification. Try to increase Recursive call to sum_nospec without a specification. Try to increase
the -eva-unroll-recursive-calls parameter or write a specification the -eva-unroll-recursive-calls parameter or write a specification
for function sum_nospec. for function sum_nospec.
......
tests/value/oracle_apron/recursion.0.res.oracle deleted 100644 → 0
+ 0
− 628
View file @ 0f94bac7
This diff is collapsed.
tests/value/oracle_apron/recursion.1.res.oracle deleted 100644 → 0
+ 0
− 510
View file @ 0f94bac7
This diff is collapsed.
tests/value/oracle_apron/recursion.2.res.oracle deleted 100644 → 0
+ 0
− 10
View file @ 0f94bac7
10,12d9
< [eva] tests/value/recursion.c:429: Frama_C_show_each_10: {10}
< [eva] tests/value/recursion.c:434: Frama_C_show_each_36: {36}
< [eva] using specification for function Frama_C_interval
14,16c11
< Recursive call to sum_nospec without a specification. Try to increase
< the -eva-unroll-recursive-calls parameter or write a specification
< for function sum_nospec.
---
> The binding to APRON domains does not support recursive calls.
tests/value/recursion.c
+ 7
− 4
View file @ 50db0caa
/* run.config_apron
DONTRUN: The apron binding does not support recursion.
*/
/* run.config* /* run.config*
STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 0" STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 0"
STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 20" STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 20"
EXIT: 1 EXIT: 1
STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 5 -main main_fail" STDOPT: +"-eva-no-show-progress -eva-unroll-recursive-calls 5 -main main_fail"
*/ */
#include <__fc_builtin.h> #include <__fc_builtin.h>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment