Skip to content
Snippets Groups Projects
Commit 47ef8ed7 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] rename a test and add new cases 

- object_pointer end of structure
- dangling -> not object_pointer
parent 8f12090f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_acsl/invalid_pointer.c → src/plugins/wp/tests/wp_acsl/object_pointer.i
+ 10
− 0
View file @ 47ef8ed7
......@@ -54,7 +54,17 @@ void compound(void)
//@check G: \object_pointer(&(p->g));
//@check F2: \object_pointer(&(p->f)+2);
//@check G2: !\object_pointer(&(p->g)+2);
//@check E: \object_pointer(p+1);
int k ;
struct A a ;
//@check AM: (0 <= k <= 10) <==> \object_pointer(&a.m[k]);
}
void dangling(void){
int *p ;
{
int l ;
p = &l ;
}
//@ check !\object_pointer(p);
}
src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle → src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
+ 39
− 22
View file @ 47ef8ed7
# frama-c -wp [...]
[kernel] Parsing invalid_pointer.c (with preprocessing)
[kernel] Parsing object_pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] [Valid] Goal array_exits (Cfg) (Unreachable)
[wp] [Valid] Goal array_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal compound_exits (Cfg) (Unreachable)
[wp] [Valid] Goal compound_terminates (Cfg) (Trivial)
[wp] [Valid] Goal dangling_exits (Cfg) (Unreachable)
[wp] [Valid] Goal dangling_terminates (Cfg) (Trivial)
[wp] [Valid] Goal memvar_exits (Cfg) (Unreachable)
[wp] [Valid] Goal memvar_terminates (Cfg) (Trivial)
[wp] [Valid] Goal pointer_exits (Cfg) (Unreachable)
[wp] [Valid] Goal pointer_terminates (Cfg) (Trivial)
[wp] invalid_pointer.c:23: Warning: void object
[wp] object_pointer.i:23: Warning: void object
------------------------------------------------------------
Function array
------------------------------------------------------------
Goal Check 'ARR' (file invalid_pointer.c, line 32):
Goal Check 'ARR' (file object_pointer.i, line 32):
Assume { Type: is_sint32(k). (* Heap *) Type: linked(Malloc_0). }
Prove: ((0 <= k) /\ (k <= 25)) <->
valid_obj(Malloc_0[L_a_33 <- 25], shift_sint32(global(L_a_33), k), 1).
......@@ -25,76 +27,91 @@ Prove: ((0 <= k) /\ (k <= 25)) <->
Function compound
------------------------------------------------------------
Goal Check 'M1' (file invalid_pointer.c, line 47):
Goal Check 'M1' (file object_pointer.i, line 47):
Prove: true.
------------------------------------------------------------
Goal Check 'P0' (file invalid_pointer.c, line 48):
Goal Check 'P0' (file object_pointer.i, line 48):
Prove: true.
------------------------------------------------------------
Goal Check 'P1' (file invalid_pointer.c, line 49):
Goal Check 'P1' (file object_pointer.i, line 49):
Prove: true.
------------------------------------------------------------
Goal Check 'P2' (file invalid_pointer.c, line 50):
Goal Check 'P2' (file object_pointer.i, line 50):
Prove: true.
------------------------------------------------------------
Goal Check 'F' (file invalid_pointer.c, line 53):
Goal Check 'F' (file object_pointer.i, line 53):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_f(global(L_s_38)), 1).
------------------------------------------------------------
Goal Check 'G' (file invalid_pointer.c, line 54):
Goal Check 'G' (file object_pointer.i, line 54):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_g(global(L_s_38)), 1).
------------------------------------------------------------
Goal Check 'F2' (file invalid_pointer.c, line 55):
Goal Check 'F2' (file object_pointer.i, line 55):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_s_38 <- 2],
shift_sint32(shiftfield_F1_S_f(global(L_s_38)), 2), 1).
------------------------------------------------------------
Goal Check 'G2' (file invalid_pointer.c, line 56):
Goal Check 'G2' (file object_pointer.i, line 56):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: !valid_obj(Malloc_0[L_s_38 <- 2],
shift_sint32(shiftfield_F1_S_g(global(L_s_38)), 2), 1).
------------------------------------------------------------
Goal Check 'AM' (file invalid_pointer.c, line 59):
Goal Check 'E' (file object_pointer.i, line 57):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_s_38 <- 2], shift_S1_S(global(L_s_38), 1), 2).
------------------------------------------------------------
Goal Check 'AM' (file object_pointer.i, line 60):
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function dangling
------------------------------------------------------------
Goal Check (file object_pointer.i, line 69):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: !valid_obj(Malloc_0[L_l_45 <- 0], global(L_l_45), 1).
------------------------------------------------------------
------------------------------------------------------------
Function memvar
------------------------------------------------------------
Goal Check 'M1' (file invalid_pointer.c, line 6):
Goal Check 'M1' (file object_pointer.i, line 6):
Prove: true.
------------------------------------------------------------
Goal Check 'P0' (file invalid_pointer.c, line 7):
Goal Check 'P0' (file object_pointer.i, line 7):
Prove: true.
------------------------------------------------------------
Goal Check 'P1' (file invalid_pointer.c, line 8):
Goal Check 'P1' (file object_pointer.i, line 8):
Prove: true.
------------------------------------------------------------
Goal Check 'P2' (file invalid_pointer.c, line 9):
Goal Check 'P2' (file object_pointer.i, line 9):
Prove: true.
------------------------------------------------------------
......@@ -102,36 +119,36 @@ Prove: true.
Function pointer
------------------------------------------------------------
Goal Check 'M1' (file invalid_pointer.c, line 19):
Goal Check 'M1' (file object_pointer.i, line 19):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), -1), 1).
------------------------------------------------------------
Goal Check 'P0' (file invalid_pointer.c, line 20):
Goal Check 'P0' (file object_pointer.i, line 20):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_x_28 <- 1], global(L_x_28), 1).
------------------------------------------------------------
Goal Check 'P1' (file invalid_pointer.c, line 21):
Goal Check 'P1' (file object_pointer.i, line 21):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 1), 1).
------------------------------------------------------------
Goal Check 'P2' (file invalid_pointer.c, line 22):
Goal Check 'P2' (file object_pointer.i, line 22):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 2), 1).
------------------------------------------------------------
Goal Check 'qed_NULL' (file invalid_pointer.c, line 23):
Goal Check 'qed_NULL' (file object_pointer.i, line 23):
Prove: true.
------------------------------------------------------------
Goal Check 'prover_NULL' (file invalid_pointer.c, line 24):
Goal Check 'prover_NULL' (file object_pointer.i, line 24):
Assume { (* Heap *) Type: linked(Malloc_0). }
Prove: valid_obj(Malloc_0[L_x_28 <- 1], L_GET, 1).
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle → src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
+ 13
− 7
View file @ 47ef8ed7
# frama-c -wp [...]
[kernel] Parsing invalid_pointer.c (with preprocessing)
[kernel] Parsing object_pointer.i (no preprocessing)
[wp] Running WP plugin...
[wp] [Valid] Goal array_exits (Cfg) (Unreachable)
[wp] [Valid] Goal array_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal compound_exits (Cfg) (Unreachable)
[wp] [Valid] Goal compound_terminates (Cfg) (Trivial)
[wp] [Valid] Goal dangling_exits (Cfg) (Unreachable)
[wp] [Valid] Goal dangling_terminates (Cfg) (Trivial)
[wp] [Valid] Goal memvar_exits (Cfg) (Unreachable)
[wp] [Valid] Goal memvar_terminates (Cfg) (Trivial)
[wp] [Valid] Goal pointer_exits (Cfg) (Unreachable)
[wp] [Valid] Goal pointer_terminates (Cfg) (Trivial)
[wp] invalid_pointer.c:23: Warning: void object
[wp] 20 goals scheduled
[wp] object_pointer.i:23: Warning: void object
[wp] 22 goals scheduled
[wp] [Valid] typed_memvar_check_M1 (Qed)
[wp] [Valid] typed_memvar_check_P0 (Qed)
[wp] [Valid] typed_memvar_check_P1 (Qed)
......@@ -31,16 +33,20 @@
[wp] [Valid] typed_compound_check_G (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_F2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_G2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_compound_check_E (Alt-Ergo) (Cached)
[wp] [Valid] typed_compound_check_AM (Qed)
[wp] Proved goals: 28 / 28
Terminating: 4
Unreachable: 4
[wp] [Unsuccess] typed_dangling_check (Alt-Ergo) (Cached)
[wp] Proved goals: 30 / 32
Terminating: 5
Unreachable: 5
Qed: 10
Alt-Ergo: 10
Unsuccess: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
memvar 4 - 4 100%
pointer 1 5 6 100%
array - 1 1 100%
compound 5 4 9 100%
compound 5 4 10 90.0%
dangling - - 1 0.0%
------------------------------------------------------------
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