From 289c25467a4443c78f855ed261d7a1531c2a3662 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 18 Jun 2024 19:17:49 +0200
Subject: [PATCH] [slicing] treat more extensions in logic-deps
---
src/kernel_services/analysis/logic_deps.ml | 18 ++++++++++++++++++
tests/slicing/oracle/adpcm.res.oracle | 15 ++++++++-------
2 files changed, 26 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 1c63dce0dc7..d416534d0ac 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -500,6 +500,24 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
results l
| AStmtSpec _ -> (* TODO *)
raise (NYI "[logic_interp] statement contract")
+ | AExtended(_,_, { ext_kind = Ext_preds preds }) ->
+ (* to select the declaration of the variables *)
+ List.fold_left
+ (fun results pred -> {
+ results with
+ locals = Varinfo.Set.union (extract_locals_from_pred pred) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_pred pred) results.labels
+ })
+ results preds
+ | AExtended(_,_, { ext_kind = Ext_terms terms }) ->
+ (* to select the declaration of the variables *)
+ List.fold_left
+ (fun results term -> {
+ results with
+ locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
+ })
+ results terms
| AExtended _ -> raise (NYI "[logic_interp] extension")
(* Used by annotations entry points. *)
diff --git a/tests/slicing/oracle/adpcm.res.oracle b/tests/slicing/oracle/adpcm.res.oracle
index e11347f6b73..496702e3225 100644
--- a/tests/slicing/oracle/adpcm.res.oracle
+++ b/tests/slicing/oracle/adpcm.res.oracle
@@ -1531,13 +1531,6 @@ Slicing project worklist [default] =
[pdg] computing for function logscl
[pdg] done for function logscl
[slicing] applying actions: 3/3...
-[slicing] tests/test/adpcm.c:277: Warning: Dropping unsupported ACSL annotation
-[slicing] tests/test/adpcm.c:288: Warning: Dropping unsupported ACSL annotation
-[slicing] tests/test/adpcm.c:418: Warning: Dropping unsupported ACSL annotation
-[slicing] tests/test/adpcm.c:453: Warning: Dropping unsupported ACSL annotation
-[slicing] tests/test/adpcm.c:506: Warning: Dropping unsupported ACSL annotation
-[slicing] tests/test/adpcm.c:512: Warning: Dropping unsupported ACSL annotation
-[slicing] tests/test/adpcm.c:607: Warning: Dropping unsupported ACSL annotation
[sparecode] remove unused global declarations from project 'Sliced code tmp'
[sparecode] removed unused global declarations in new project 'Sliced code'
/* Generated by Frama-C */
@@ -1828,6 +1821,7 @@ void encode_slice_1(int xin1, int xin2)
h_ptr ++;
xb = (long)*tmp_1 * (long)*tmp_2;
i = 0;
+ /*@ loop unfold 11; */
while (i < 10) {
{
int *tmp_3;
@@ -1856,6 +1850,7 @@ void encode_slice_1(int xin1, int xin2)
xb += (long)*tqmf_ptr * (long)*tmp_9;
tqmf_ptr1 = tqmf_ptr - 2;
i = 0;
+ /*@ loop unfold 23; */
while (i < 22) {
int *tmp_10;
int *tmp_11;
@@ -1925,6 +1920,7 @@ int filtez_slice_1(int *bpl, int *dlt_0)
dlt_0 ++;
zl = (long)*tmp * (long)*tmp_0;
i = 1;
+ /*@ loop unfold 7; */
while (i < 6) {
int *tmp_1;
int *tmp_2;
@@ -1961,6 +1957,7 @@ int quantl_slice_1(int el_0, int detl_0)
wd = (long)abs_slice_1(el_0);
mil = 0;
decis = (long)decis_levl[mil] * (long)detl_0 >> 15L;
+ /*@ loop unfold 30; */
while (1) {
if (wd <= decis) {
if (! (mil < 29)) break;
@@ -2003,6 +2000,7 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
int wd3;
if (dlt_0 == 0) {
i = 0;
+ /*@ loop unfold 7; */
while (i < 6) {
*(bli + i) = (int)(255L * (long)*(bli + i) >> 8L);
i ++;
@@ -2010,6 +2008,7 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
}
else {
i = 0;
+ /*@ loop unfold 7; */
while (i < 6) {
if ((long)dlt_0 * (long)*(dlti + i) >= (long)0) wd2 = 128;
else wd2 = -128;
@@ -2071,6 +2070,8 @@ void main(void)
{
int i;
i = 0;
+ /*@ loop unfold 11;
+ loop \eva::widen_hints "all", 32767; */
while (i < 10) {
encode_slice_1(test_data[i],test_data[i + 1]);
i += 2;
--
GitLab