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

[wp] Fix a bug with int chunks ranks + add a test

parent f948e96e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/MemTyped.ml
+ 12
− 5
View file @ 0d76acb2
......@@ -130,15 +130,22 @@ struct
let self = "typed"
let int_rank = function
| CBool -> 0
| k -> Ctypes.i_bytes k * (if Ctypes.signed k then 2 else 1)
| UInt8 -> 1
| SInt8 -> 2
| UInt16 -> 3
| SInt16 -> 4
| UInt32 -> 5
| SInt32 -> 6
| UInt64 -> 7
| SInt64 -> 8
let rank = function
| M_char -> -1
| M_int i -> int_rank i
| M_f32 -> 17
| M_f64 -> 18
| M_pointer -> 19
| T_alloc -> 20
| M_f32 -> 9
| M_f64 -> 10
| M_pointer -> 11
| T_alloc -> 12
let hash = rank
let name = function
| M_int _ -> "Mint"
......
src/plugins/wp/tests/wp_acsl/chunk_typing.i 0 → 100644
+ 54
− 0
View file @ 0d76acb2
/* run.config
OPT: -wp-rte -wp-prop="-NO_CHECK,-rte"
*/
/* run.config_qualif
OPT: -wp-rte -wp-prop="-NO_CHECK,-rte"
*/
const char x[10] ;
/*@
requires \valid(&i8[0..9]) && \valid(&u8[0..9]) && \valid(&i16[0..9]) && \valid(&u16[0..9])
&& \valid(&i32[0..9]) && \valid(&u32[0..9]) && \valid(&i64[0..9]) && \valid(&u64[0..9]);
ensures \forall integer k ;
0 <= k < 10 ==>
x[k]+8 ==
i8[k]+7 == u8[k]+6 ==
i16[k]+5 == u16[k]+4 ==
i32[k]+3 == u32[k]+2 ==
i64[k]+1 == u64[k];
*/
void function(signed char i8[10],
unsigned char u8[10],
signed short i16[10],
unsigned short u16[10],
signed int i32[10],
unsigned int u32[10],
signed long long int i64[10],
unsigned long long int u64[10])
{
/*@
loop invariant NO_CHECK: 0 <= i <= 10;
loop invariant \forall integer k ; 0 <= k < i ==> i8[k] == 1 ;
loop invariant \forall integer k ; 0 <= k < i ==> u8[k] == 2 ;
loop invariant \forall integer k ; 0 <= k < i ==> i16[k] == 3 ;
loop invariant \forall integer k ; 0 <= k < i ==> u16[k] == 4 ;
loop invariant \forall integer k ; 0 <= k < i ==> i32[k] == 5 ;
loop invariant \forall integer k ; 0 <= k < i ==> u32[k] == 6 ;
loop invariant \forall integer k ; 0 <= k < i ==> i64[k] == 7 ;
loop invariant \forall integer k ; 0 <= k < i ==> u64[k] == 8 ;
loop assigns NO_CHECK: i, i8[0..9], u8[0..9], i16[0..9], u16[0..9], i32[0..9], u32[0..9], i64[0..9], u64[0..9] ;
loop variant NO_CHECK: 10-i;
*/
for(int i = 0; i < 10; ++i){
i8[i] = 1 ;
u8[i] = 2 ;
i16[i] = 3 ;
u16[i] = 4 ;
i32[i] = 5 ;
u32[i] = 6 ;
i64[i] = 7 ;
u64[i] = 8 ;
}
}
src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle 0 → 100644
+ 965
− 0
View file @ 0d76acb2
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[rte] annotating function function
------------------------------------------------------------
Function function
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/chunk_typing.i, line 13) in 'function':
Let a = shift_sint8(i8_0, 0).
Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, 10).
Let a_2 = shift_uint8(u8_0, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 10).
Let a_4 = shift_sint16(i16_0, 0).
Let a_5 = havoc(Mint_undef_1, Mint_1, a_4, 10).
Let a_6 = shift_uint16(u16_0, 0).
Let a_7 = havoc(Mint_undef_2, Mint_2, a_6, 10).
Let a_8 = shift_sint32(i32_0, 0).
Let a_9 = havoc(Mint_undef_3, Mint_3, a_8, 10).
Let a_10 = shift_uint32(u32_0, 0).
Let a_11 = havoc(Mint_undef_4, Mint_4, a_10, 10).
Let a_12 = shift_sint64(i64_0, 0).
Let a_13 = havoc(Mint_undef_5, Mint_5, a_12, 10).
Let a_14 = shift_uint64(u64_0, 0).
Let a_15 = havoc(Mint_undef_6, Mint_6, a_14, 10).
Let a_16 = a_1[shift_sint8(i8_0, i)].
Let a_17 = a_3[shift_uint8(u8_0, i)].
Let a_18 = a_5[shift_sint16(i16_0, i)].
Let a_19 = a_7[shift_uint16(u16_0, i)].
Let a_20 = a_9[shift_sint32(i32_0, i)].
Let a_21 = a_11[shift_uint32(u32_0, i)].
Let a_22 = a_13[shift_sint64(i64_0, i)].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_3) /\
is_sint64_chunk(Mint_5) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_2) /\ is_uint32_chunk(Mint_4) /\
is_uint64_chunk(Mint_6) /\ is_uint8_chunk(Mint_0) /\ is_sint32(i_1) /\
is_sint16_chunk(a_5) /\ is_sint32_chunk(a_9) /\
is_sint64_chunk(a_13) /\ is_sint8_chunk(a_1) /\ is_uint16_chunk(a_7) /\
is_uint32_chunk(a_11) /\ is_uint64_chunk(a_15) /\ is_uint8_chunk(a_3).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
IsArray1_sint8(x) /\ linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i) /\ (i <= 9).
(* Initializer *)
Init: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (x[i_2] = 0))).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_4, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a, 10) /\
valid_rw(Malloc_0, a_6, 10) /\ valid_rw(Malloc_0, a_10, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_2, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_15[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_13[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_11[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_9[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_7[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_5[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_3[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(a_1[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
Prove: (a_16 = (1 + x[i])) /\ (a_17 = (1 + a_16)) /\ (a_18 = (1 + a_17)) /\
(a_19 = (1 + a_18)) /\ (a_20 = (1 + a_19)) /\ (a_21 = (1 + a_20)) /\
(a_22 = (1 + a_21)) /\ (a_15[shift_uint64(u64_0, i)] = (1 + a_22)).
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 32):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
Let a_24 = a_9[a_7 <- 1].
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_24) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_sint8(i8_0, i_1)] = 1.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 32):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 33):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_0, Mint_0, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_5, Mint_5, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_6, Mint_6, a_22, 10).
Let a_24 = a_11[a_6 <- 2].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_4) /\ is_uint32_chunk(Mint_5) /\
is_uint64_chunk(Mint_6) /\ is_uint8_chunk(Mint_0) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_24).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_uint8(u8_0, i_1)] = 2.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 33):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 34):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_0, Mint_0, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_1, Mint_1, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
Let a_24 = a_13[a_5 <- 3].
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_24) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_sint16(i16_0, i_1)] = 3.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 34):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 35):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_0, Mint_0, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
Let a_24 = a_15[a_4 <- 4].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_0) /\ is_uint32_chunk(Mint_4) /\
is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_24) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_uint16(u16_0, i_1)] = 4.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 35):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 36):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_0, Mint_0, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_2, Mint_2, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
Let a_24 = a_17[a_3 <- 5].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_0) /\
is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_24) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_sint32(i32_0, i_1)] = 5.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 36):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 37):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
Let a_24 = a_19[a_2 <- 6].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_4) /\ is_uint32_chunk(Mint_0) /\
is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_24) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_uint32(u32_0, i_1)] = 6.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 37):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 38):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_3, Mint_3, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_4, Mint_4, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_0, Mint_0, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_5, Mint_5, a_22, 10).
Let a_24 = a_21[a_1 <- 7].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
is_sint64_chunk(Mint_0) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_24) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_23[a <- 8]) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_sint64(i64_0, i_1)] = 7.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 38):
Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file tests/wp_acsl/chunk_typing.i, line 39):
Let a = shift_uint64(u64_0, i).
Let a_1 = shift_sint64(i64_0, i).
Let a_2 = shift_uint32(u32_0, i).
Let a_3 = shift_sint32(i32_0, i).
Let a_4 = shift_uint16(u16_0, i).
Let a_5 = shift_sint16(i16_0, i).
Let a_6 = shift_uint8(u8_0, i).
Let a_7 = shift_sint8(i8_0, i).
Let a_8 = shift_sint8(i8_0, 0).
Let a_9 = havoc(Mchar_undef_0, Mchar_0, a_8, 10).
Let a_10 = shift_uint8(u8_0, 0).
Let a_11 = havoc(Mint_undef_6, Mint_6, a_10, 10).
Let a_12 = shift_sint16(i16_0, 0).
Let a_13 = havoc(Mint_undef_1, Mint_1, a_12, 10).
Let a_14 = shift_uint16(u16_0, 0).
Let a_15 = havoc(Mint_undef_4, Mint_4, a_14, 10).
Let a_16 = shift_sint32(i32_0, 0).
Let a_17 = havoc(Mint_undef_2, Mint_2, a_16, 10).
Let a_18 = shift_uint32(u32_0, 0).
Let a_19 = havoc(Mint_undef_5, Mint_5, a_18, 10).
Let a_20 = shift_sint64(i64_0, 0).
Let a_21 = havoc(Mint_undef_3, Mint_3, a_20, 10).
Let a_22 = shift_uint64(u64_0, 0).
Let a_23 = havoc(Mint_undef_0, Mint_0, a_22, 10).
Let a_24 = a_23[a <- 8].
Assume {
Type: is_sint16_chunk(Mint_1) /\ is_sint32_chunk(Mint_2) /\
is_sint64_chunk(Mint_3) /\ is_sint8_chunk(Mchar_0) /\
is_uint16_chunk(Mint_4) /\ is_uint32_chunk(Mint_5) /\
is_uint64_chunk(Mint_0) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
is_sint16_chunk(a_13) /\ is_sint32_chunk(a_17) /\
is_sint64_chunk(a_21) /\ is_sint8_chunk(a_9) /\
is_uint16_chunk(a_15) /\ is_uint32_chunk(a_19) /\
is_uint64_chunk(a_23) /\ is_uint8_chunk(a_11) /\
is_sint16_chunk(a_13[a_5 <- 3]) /\ is_sint32_chunk(a_17[a_3 <- 5]) /\
is_sint64_chunk(a_21[a_1 <- 7]) /\ is_sint8_chunk(a_9[a_7 <- 1]) /\
is_uint16_chunk(a_15[a_4 <- 4]) /\ is_uint32_chunk(a_19[a_2 <- 6]) /\
is_uint64_chunk(a_24) /\ is_uint8_chunk(a_11[a_6 <- 2]).
(* Heap *)
Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
(region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
(region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
(region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_12, 10) /\ valid_rw(Malloc_0, a_16, 10) /\
valid_rw(Malloc_0, a_20, 10) /\ valid_rw(Malloc_0, a_8, 10) /\
valid_rw(Malloc_0, a_14, 10) /\ valid_rw(Malloc_0, a_18, 10) /\
valid_rw(Malloc_0, a_22, 10) /\ valid_rw(Malloc_0, a_10, 10).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_23[shift_uint64(u64_0, i_2)] = 8))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_21[shift_sint64(i64_0, i_2)] = 7))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_19[shift_uint32(u32_0, i_2)] = 6))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_17[shift_sint32(i32_0, i_2)] = 5))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_15[shift_uint16(u16_0, i_2)] = 4))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_13[shift_sint16(i16_0, i_2)] = 3))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_11[shift_uint8(u8_0, i_2)] = 2))).
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_9[shift_sint8(i8_0, i_2)] = 1))).
(* Invariant 'NO_CHECK' *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
Have: i <= 9.
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_7, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_6, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_5, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_4, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_3, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_2, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a_1, 1).
(* Assertion 'rte,mem_access' *)
Have: valid_rw(Malloc_0, a, 1).
(* Assertion 'rte,signed_overflow' *)
Have: i <= 2147483646.
}
Prove: a_24[shift_uint64(u64_0, i_1)] = 8.
------------------------------------------------------------
Goal Establishment of Invariant (file tests/wp_acsl/chunk_typing.i, line 39):
Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'function':
/*@
behavior typed:
requires \separated(x+(..),
\union(i8+(..),u8+(..),i16+(..),u16+(..),i32+(..),u32+(..),
i64+(..),u64+(..)));
*/
void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
int * /*[10]*/ i32, unsigned int * /*[10]*/ u32,
long long * /*[10]*/ i64, unsigned long long * /*[10]*/ u64);
src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle 0 → 100644
+ 41
− 0
View file @ 0d76acb2
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_acsl/chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[rte] annotating function function
[wp] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_2_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_3_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_3_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_4_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_4_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_5_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_5_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_6_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_6_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_7_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_7_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_8_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_8_established : Valid
[wp] Proved goals: 17 / 17
Qed: 8
Alt-Ergo: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
function 8 9 17 100%
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'function':
/*@
behavior typed:
requires \separated(x+(..),
\union(i8+(..),u8+(..),i16+(..),u16+(..),i32+(..),u32+(..),
i64+(..),u64+(..)));
*/
void function(signed char * /*[10]*/ i8, unsigned char * /*[10]*/ u8,
short * /*[10]*/ i16, unsigned short * /*[10]*/ u16,
int * /*[10]*/ i32, unsigned int * /*[10]*/ u32,
long long * /*[10]*/ i64, unsigned long long * /*[10]*/ u64);
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