[wp] Update oracles

src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle

@@ -31,19 +31,20 @@ 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).
+  Type: IsArray1_sint8(x) /\ 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).
+      linked(Malloc_0) /\ sconst(Mchar_0).
   (* Goal *)
   When: (0 <= i) /\ (i <= 9).
   (* Initializer *)

src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle

@@ -216,16 +216,17 @@ end
     
     (* use frama_c_wp.memory.Memory *)
     
-    (* use Chunk *)
-    
     (* use S1_X *)
     
+    (* use Chunk *)
+    
     (* use Compound *)
     
     goal wp_goal :
       forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
-       addr -> int, a:addr.
+       addr -> int, a:addr, x:S1_X.
        region (base a) <= 0 ->
+       IsS1_X x ->
        is_sint16_chunk t3 ->
        is_sint32_chunk t4 ->
        is_sint8_chunk t2 ->
@@ -240,15 +241,15 @@ end
 
 Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
 Assume {
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0) /\
       IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
   (* Heap *)
   Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
       cinits(Init_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
   (* Block In *)
   Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
@@ -261,16 +262,16 @@ Prove: valid_rd(Malloc_0, p, 3).
 Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
 Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
 Assume {
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
   (* Heap *)
   Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
       cinits(Init_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+  Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
       is_sint8_chunk(Mchar_0).
   (* Block In *)
   Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/04c1fcb3dde99404e56f398c9d3c7b31.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1563,
+  "steps": 286 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/09419c3fbb6dc84c7ea4daf3841c155f.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0323,
+  "steps": 171 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/0af3d5135623c7629e8792c15c73e11e.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0323,
+  "steps": 171 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/1d2ed0d831c17546d006475b478b59c1.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0322,
+  "steps": 171 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/281d06f1268fc1f6bae73c9b23a370f6.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0337,
+  "steps": 171 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/35644610983981a71b83b5427a68f6c0.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0377,
+  "steps": 171 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/6367c7d1e56f1af80ad76d813e09b66a.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.138,
+  "steps": 269 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/675a842c7ec32528e5e21888634a1279.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0463,
+  "steps": 123 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/7ea33aa4c8dc9c1ed12a312a5a7b96ed.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1203,
+  "steps": 252 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/a76226839c540aad032cd3b9de095b89.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.1085,
+  "steps": 235 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/bd67f73e3ff115a9f45b4244c20611fe.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0154,
+  "steps": 64 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e046513e2f30f1a1946d5d6e40ef9129.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0847,
+  "steps": 184 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e434135b1fa122e6a232e26709df80a5.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0129,
+  "steps": 62 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e8e066b606c41e89f82b2aa3eef46a68.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0853,
+  "steps": 201 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/e9c784c595bc40819eff858fbcc12bab.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0314,
+  "steps": 171 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/efda69b6f9003dcb53f99c442ec8c4de.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0722,
+  "steps": 167 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f6b163a1cc48d21b279ce315660ffd85.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0881,
+  "steps": 218 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.0.session/cache/f97c74763d0222ed9be7c3fa666ce4e9.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0487,
+  "steps": 171 }