From b24febdc5bf60a6b38c5f4d71cd54ec43adc5805 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thibault.martin@cea.fr>
Date: Mon, 7 Oct 2019 11:20:23 +0200
Subject: [PATCH] Ajout d'un test pour #714
---
.../oracle/temporary_location.res.oracle | 50 +++++++++++++++++++
tests/syntax/temporary_location.c | 19 +++++++
tests/syntax/temporary_location.ml | 18 +++++++
3 files changed, 87 insertions(+)
create mode 100644 tests/syntax/oracle/temporary_location.res.oracle
create mode 100644 tests/syntax/temporary_location.c
create mode 100644 tests/syntax/temporary_location.ml
diff --git a/tests/syntax/oracle/temporary_location.res.oracle b/tests/syntax/oracle/temporary_location.res.oracle
new file mode 100644
index 00000000000..8ba7b0ae166
--- /dev/null
+++ b/tests/syntax/oracle/temporary_location.res.oracle
@@ -0,0 +1,50 @@
+[kernel] Parsing tests/syntax/temporary_location.c (with preprocessing)
+[kernel] __retres -> tests/syntax/temporary_location.c:7
+[kernel] __retres -> tests/syntax/temporary_location.c:7
+[kernel] __retres -> tests/syntax/temporary_location.c:7
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+[kernel] tmp_0 -> tests/syntax/temporary_location.c:11
+[kernel] f -> tests/syntax/temporary_location.c:6
+[kernel] tmp_0 -> tests/syntax/temporary_location.c:11
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] tmp -> tests/syntax/temporary_location.c:16
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] y -> tests/syntax/temporary_location.c:16
+[kernel] tmp -> tests/syntax/temporary_location.c:16
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+[kernel] y -> tests/syntax/temporary_location.c:16
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+/* Generated by Frama-C */
+int f(void)
+{
+ int __retres;
+ __retres = 1;
+ return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int tmp_0;
+ tmp_0 = f();
+ if (tmp_0) {
+ __retres = 0;
+ goto return_label;
+ }
+ else {
+ int tmp;
+ int x = 0;
+ tmp = x;
+ x ++;
+ int y = tmp + 1;
+ __retres = y + 3;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
+
diff --git a/tests/syntax/temporary_location.c b/tests/syntax/temporary_location.c
new file mode 100644
index 00000000000..765e6bccede
--- /dev/null
+++ b/tests/syntax/temporary_location.c
@@ -0,0 +1,19 @@
+/* run.config
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+*/
+
+int f(void) {
+ return 1;
+}
+
+int main(void) {
+ if(f()){
+ return 0;
+ }
+ else {
+ int x = 0;
+ int y = x++ + 1;
+ return y + 3;
+ }
+}
diff --git a/tests/syntax/temporary_location.ml b/tests/syntax/temporary_location.ml
new file mode 100644
index 00000000000..c6792bd916b
--- /dev/null
+++ b/tests/syntax/temporary_location.ml
@@ -0,0 +1,18 @@
+open Cil_types
+
+class vis = object(_)
+ inherit Visitor.frama_c_inplace
+
+ method! vvrbl vi =
+ Kernel.result "%s -> %a" vi.vname Printer.pp_location vi.vdecl;
+ Cil.DoChildren
+
+end
+
+let main () =
+ Ast.compute ();
+ Cil.visitCilFile (new vis :> Cil.cilVisitor) (Ast.get ())
+
+let () =
+ Db.Main.extend main
+
--
GitLab