From 37e947b8a9becd2cae35dea2efade82e32c050df Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 16 Apr 2024 15:10:22 +0200
Subject: [PATCH] [tests] add test for diffing ACSL extensions
---
tests/syntax/ast_diff_1.i | 12 +++++++
tests/syntax/ast_diff_2.c | 10 ++++++
tests/syntax/oracle/ast_diff_1.0.res.oracle | 10 ++++--
tests/syntax/oracle/ast_diff_1.1.res.oracle | 36 ++++++++++++---------
4 files changed, 51 insertions(+), 17 deletions(-)
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 7afc3a0e3b3..86b0c7606e6 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -1,4 +1,6 @@
/* run.config
+ COMMENT: we need Eva for the loop unroll ACSL extension
+ PLUGIN: eva
MODULE: @PTEST_NAME@
OPT: -then -ast-diff %{dep:ast_diff_2.c}
OPT: -then -ast-diff %{dep:ast_diff_2.c} -cpp-extra-args="-DADD_ENUM_TAG"
@@ -107,3 +109,13 @@ void se() {
struct s S;
S.c[0] = 1;
}
+
+void with_loop_unroll_same() {
+ //@ loop unroll 5;
+ for (int i = 0; i < 5; i++);
+}
+
+void with_loop_unroll_diff() {
+ //@ loop unroll 4;
+ for (int i = 0; i < 5; i++);
+}
diff --git a/tests/syntax/ast_diff_2.c b/tests/syntax/ast_diff_2.c
index c0bd72914c1..f0009e13c18 100644
--- a/tests/syntax/ast_diff_2.c
+++ b/tests/syntax/ast_diff_2.c
@@ -102,3 +102,13 @@ void se() {
struct s S;
S.c[0] = 1;
}
+
+void with_loop_unroll_same() {
+ //@ loop unroll 5;
+ for (int i = 0; i < 5; i++);
+}
+
+void with_loop_unroll_diff() {
+ //@ loop unroll 5;
+ for (int i = 0; i < 5; i++);
+}
diff --git a/tests/syntax/oracle/ast_diff_1.0.res.oracle b/tests/syntax/oracle/ast_diff_1.0.res.oracle
index 040eb7eac6a..ef54b4b6f7e 100644
--- a/tests/syntax/oracle/ast_diff_1.0.res.oracle
+++ b/tests/syntax/oracle/ast_diff_1.0.res.oracle
@@ -21,10 +21,14 @@
[AST diff test] Variable g: => g
[AST diff test] Variable se: => se
[AST diff test] Variable S: => S
-[AST diff test] Variable has_static_local_x: => has_static_local_y
+[AST diff test] Variable with_loop_unroll_same: => with_loop_unroll_same
+[AST diff test] Variable i_0: => i_0
[AST diff test] Variable h: => h
-[AST diff test] Variable __retres: => __retres
+[AST diff test] Variable with_loop_unroll_diff: => with_loop_unroll_diff
+[AST diff test] Variable i_0: => i_0
+[AST diff test] Variable has_static_local_x: => has_static_local_y
[AST diff test] Variable use_logic_builtin: => use_logic_builtin
+[AST diff test] Variable __retres: => __retres
[AST diff test] Variable x: => x
[AST diff test] Variable y: => y
[AST diff test] Variable has_static_local: => has_static_local
@@ -39,7 +43,9 @@
[AST diff test] Function with_goto_unchanged: => with_goto_unchanged
[AST diff test] Function g: N/A
[AST diff test] Function se: => se
+[AST diff test] Function with_loop_unroll_same: => with_loop_unroll_same
[AST diff test] Function h: -> h (body changed)
+[AST diff test] Function with_loop_unroll_diff: => with_loop_unroll_diff
[AST diff test] Function use_logic_builtin: => use_logic_builtin
[AST diff test] Function has_static_local: => has_static_local
[AST diff test] Function decl: => decl
diff --git a/tests/syntax/oracle/ast_diff_1.1.res.oracle b/tests/syntax/oracle/ast_diff_1.1.res.oracle
index 1fe85b83738..21e1ebbe13b 100644
--- a/tests/syntax/oracle/ast_diff_1.1.res.oracle
+++ b/tests/syntax/oracle/ast_diff_1.1.res.oracle
@@ -2,15 +2,6 @@
[kernel] Parsing ast_diff_2.c (with preprocessing)
[kernel] Parsing ast_diff_1.i (no preprocessing)
[AST diff test] Showing correspondances between orig_default and default
-[AST diff test] Variable use_logic_builtin: => use_logic_builtin
-[AST diff test] Variable x: => x
-[AST diff test] Variable y: => y
-[AST diff test] Variable has_static_local: => has_static_local
-[AST diff test] Variable decl: => decl
-[AST diff test] Variable used_in_decl: => used_in_decl
-[AST diff test] Variable ptr_func: => ptr_func
-[AST diff test] Variable i: => i
-[AST diff test] Variable local_var_use: => local_var_use
[AST diff test] Variable v: => w
[AST diff test] Variable a: => q
[AST diff test] Variable x: => z
@@ -27,17 +18,32 @@
[AST diff test] Variable c: => c
[AST diff test] Variable g: => g
[AST diff test] Variable se: => se
-[AST diff test] Variable has_static_local_x: => has_static_local_y
+[AST diff test] Variable with_loop_unroll_same: => with_loop_unroll_same
+[AST diff test] Variable i_0: => i_0
[AST diff test] Variable h: => h
-[AST diff test] Function use_logic_builtin: => use_logic_builtin
-[AST diff test] Function has_static_local: => has_static_local
-[AST diff test] Function decl: => decl
-[AST diff test] Function i: => i
-[AST diff test] Function local_var_use: => local_var_use
+[AST diff test] Variable with_loop_unroll_diff: => with_loop_unroll_diff
+[AST diff test] Variable i_0: => i_0
+[AST diff test] Variable has_static_local_x: => has_static_local_y
+[AST diff test] Variable use_logic_builtin: => use_logic_builtin
+[AST diff test] Variable x: => x
+[AST diff test] Variable y: => y
+[AST diff test] Variable has_static_local: => has_static_local
+[AST diff test] Variable decl: => decl
+[AST diff test] Variable used_in_decl: => used_in_decl
+[AST diff test] Variable ptr_func: => ptr_func
+[AST diff test] Variable i: => i
+[AST diff test] Variable local_var_use: => local_var_use
[AST diff test] Function use_s: N/A
[AST diff test] Function with_goto_changed: -> with_goto_changed (body changed)
[AST diff test] Function f: => f
[AST diff test] Function with_goto_unchanged: => with_goto_unchanged
[AST diff test] Function g: N/A
[AST diff test] Function se: -> se (body changed)
+[AST diff test] Function with_loop_unroll_same: => with_loop_unroll_same
[AST diff test] Function h: -> h (body changed)
+[AST diff test] Function with_loop_unroll_diff: => with_loop_unroll_diff
+[AST diff test] Function use_logic_builtin: => use_logic_builtin
+[AST diff test] Function has_static_local: => has_static_local
+[AST diff test] Function decl: => decl
+[AST diff test] Function i: => i
+[AST diff test] Function local_var_use: => local_var_use
--
GitLab