I attempted to verify a simple program using Frama-C's WP plugin. This program originates from Example 2.46 in the ANSI/ISO C Specification Language Version 1.20 documentation. I modified the double type variables to int to reduce verification complexity. The adapted program is as follows:
/*@
requires n >= 0 && \valid(t + (0..(n - 1))) ;
ensures \result == \sum(0, n - 1, \lambda integer k; t[k]);
*/
double array_sum(double t[], int n) {
int i;
double s = 0.0;
/*@
loop invariant 0 <= i <= n;
loop invariant s == \sum(0, i - 1, \lambda integer k; t[k]);
loop assigns s, i;
loop variant n - i;
*/
for(i = 0; i < n; i++) {
s += t[i];
}
return s;
}
When executing with:frama-c -wp -wp-prover Alt-Ergo,Z3 -wp-print -wp-timeout 10 sum.c > output.txt, the following errors occur:
[kernel] Parsing Benchmark/acsl-algorithms_verified/test.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Benchmark/acsl-algorithms_verified/test.c:3: Warning:
Lambda-functions not yet implemented
[wp] Benchmark/acsl-algorithms_verified/test.c:3: Warning:
array type non-supported({ ℤ}ℝ)
[wp] Benchmark/acsl-algorithms_verified/test.c:10: Warning:
Lambda-functions not yet implemented
[wp] Benchmark/acsl-algorithms_verified/test.c:10: Warning:
array type non-supported({ ℤ}ℝ)
[wp] 8 goals scheduled
[wp] [Qed] Goal typed_array_sum_loop_invariant_preserved : Valid (2ms)
[wp] [Qed] Goal typed_array_sum_loop_invariant_established : Valid
[wp] [Failed] Goal typed_array_sum_ensures (Stronger, 4 warnings)
Z3 4.8.6: Failed
Alt-Ergo : Timeout (Qed:2ms) (10s) (cached)
[wp] [Failed] Goal typed_array_sum_loop_invariant_2_established (Stronger, 2 warnings)
Z3 4.8.6: Unknown (Qed:0.76ms) (cached)
Alt-Ergo : Timeout (Qed:0.76ms) (10s) (cached)
[wp] [Failed] Goal typed_array_sum_loop_invariant_2_preserved (Stronger, 2 warnings)
Z3 4.8.6: Failed
Alt-Ergo : Timeout (Qed:2ms) (10s) (cached)
[wp] [Qed] Goal typed_array_sum_loop_variant_decrease : Valid (1ms)
[wp] [Qed] Goal typed_array_sum_loop_assigns : Valid
[wp] [Qed] Goal typed_array_sum_loop_variant_positive : Valid (1ms)
[wp] [Cache] found:6
[wp] Proved goals: 5 / 8
Qed: 5 (0.49ms-1ms-2ms)
Alt-Ergo : 0 (interrupted: 3) (cached: 3)
Z3 4.8.6: 0 (unknown: 1) (cached: 3) (failed: 2)
------------------------------------------------------------
Function array_sum
------------------------------------------------------------
Goal Post-condition (file Benchmark/acsl-algorithms_verified/test.c, line 3) in 'array_sum':
Benchmark/acsl-algorithms_verified/test.c:3: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:3: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Assume {
Type: is_sint32(i) /\ is_sint32(n).
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_float64(t, 0), n).
(* Invariant *)
Have: 0 <= n.
(* Invariant *)
Have: (0 <= i) /\ (i <= n).
(* Else *)
Have: n <= i.
}
Prove: of_f64(array_sum_0) = w.
Prover Z3 4.8.6 returns Failed
Prover Alt-Ergo returns Timeout (Qed:2ms) (10s) (cached)
------------------------------------------------------------
Goal Preservation of Invariant (file Benchmark/acsl-algorithms_verified/test.c, line 9):
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Prove: true.
Prover Qed returns Valid (2ms)
------------------------------------------------------------
Goal Establishment of Invariant (file Benchmark/acsl-algorithms_verified/test.c, line 9):
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Preservation of Invariant (file Benchmark/acsl-algorithms_verified/test.c, line 10):
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_float64(t, 0), n).
(* Invariant *)
Have: 0 <= n.
(* Invariant *)
Have: (0 <= i) /\ (i <= n).
(* Then *)
Have: i < n.
(* Invariant *)
Have: (-1) <= i.
}
Prove: of_f64(add_f64(s, Mf64_0[shift_float64(t, i)])) = w.
Prover Z3 4.8.6 returns Failed
Prover Alt-Ergo returns Timeout (Qed:2ms) (10s) (cached)
------------------------------------------------------------
Goal Establishment of Invariant (file Benchmark/acsl-algorithms_verified/test.c, line 10):
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Assume {
Type: is_sint32(n).
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_float64(t, 0), n).
(* Invariant *)
Have: 0 <= n.
}
Prove: w = .0.
Prover Z3 4.8.6 returns Unknown (Qed:0.76ms) (cached)
Prover Alt-Ergo returns Timeout (Qed:0.76ms) (10s) (cached)
------------------------------------------------------------
Goal Loop assigns (file Benchmark/acsl-algorithms_verified/test.c, line 11):
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file Benchmark/acsl-algorithms_verified/test.c, line 14):
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Prove: true.
Prover Qed returns Valid (1ms)
------------------------------------------------------------
Goal Positivity of Loop variant at loop (file Benchmark/acsl-algorithms_verified/test.c, line 14):
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: array type non-supported({ ℤ}ℝ)
Benchmark/acsl-algorithms_verified/test.c:10: warning from wp:
- Warning: Hide sub-term definition
Reason: Lambda-functions not yet implemented
Prove: true.
Prover Qed returns Valid (1ms)
------------------------------------------------------------
[wp:pedantic-assigns] Benchmark/acsl-algorithms_verified/test.c:5: Warning:
No 'assigns' specification for function 'array_sum'.
Callers assumptions might be imprecise.
I have two questions:
[wp] Benchmark/acsl-algorithms_verified/test.c:3: Warning: Lambda-functions not yet implemented [wp] Benchmark/acsl-algorithms_verified/test.c:3: Warning: array type non-supported({ ℤ}ℝ)
and how can I eliminate them?My frama-c's version is 25.0 (Manganese).
Currently, the sum function is not supported by WP. Thus, you have to build a (first order) definition for this. Like in this example. Note that here, it uses an axiomatic definition, but it can also be directly defined:
/*@
logic integer sum(int* array, integer begin, integer end) =
begin >= end ? 0 : array[end-1] + sum(array, begin, end-1);
*/