From 03865a1e67f57d7b414eed9902fbf3bb7de5bcde Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 13 May 2019 15:43:52 +0200
Subject: [PATCH] [Eva] Updates alternative test oracles.
---
tests/builtins/diff_bitwise | 57 +++++++++++++++++++------------------
1 file changed, 30 insertions(+), 27 deletions(-)
diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise
index b20a057439a..3fcbca67573 100644
--- a/tests/builtins/diff_bitwise
+++ b/tests/builtins/diff_bitwise
@@ -13,29 +13,30 @@ diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_bitwise/
> [eva:malloc] tests/builtins/allocated.c:127:
> resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/allocated.1.res.oracle
-191a192,197
+191a192,194
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
-> [eva] tests/builtins/allocated.c:87: Call to builtin free
-> [eva:malloc] tests/builtins/allocated.c:87:
-> strong free on bases: {__malloc_main_l82_7}
-208a215,217
+208a212,214
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-223a233,235
+223a230,232
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-238a251,253
+238a248,250
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-254,256d268
-< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+252,254c264,266
< [eva] tests/builtins/allocated.c:82:
< Call to builtin Frama_C_malloc_fresh for function malloc
+< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+---
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_7}
323a336,356
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
@@ -58,9 +59,10 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
-326d358
-< [eva] Semantic level unrolling superposing up to 300 states
-329a362,382
+329,330d361
+< Trace partitioning superposing up to 300 states
+< [eva] tests/builtins/allocated.c:84:
+333a365,385
> strong free on bases: {__malloc_main_l82_37}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
@@ -82,7 +84,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> strong free on bases: {__malloc_main_l82_31}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-399c452,470
+403c455,473
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -104,7 +106,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-471c542,560
+475c545,563
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -126,7 +128,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-543c632,650
+547c635,653
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -148,7 +150,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-615c722,740
+619c725,743
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -170,7 +172,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-687c812,830
+691c815,833
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -192,7 +194,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-759c902,920
+763c905,923
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -214,7 +216,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-831c992,1010
+835c995,1013
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -236,20 +238,21 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-901,903c1080
+905,907c1083,1084
< [eva] tests/builtins/allocated.c:87: Call to builtin free
< [eva:malloc] tests/builtins/allocated.c:87:
< strong free on bases: {__malloc_main_l82_7}
---
-> [eva] Semantic level unrolling superposing up to 500 states
-1065,1067c1242,1243
+> [eva] tests/builtins/allocated.c:81:
+> Trace partitioning superposing up to 500 states
+1069,1071c1246,1247
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
-1136a1313,1333
+1140a1317,1337
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
@@ -271,11 +274,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
-1180c1377
+1184c1381
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
---
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
-1203a1401,1407
+1207a1405,1411
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
@@ -283,11 +286,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
-1227c1431
+1231c1435
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
---
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
-1239,1240c1443,1448
+1243,1244c1447,1452
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
---
--
GitLab