From 19475eeca2e06e912cf541f72133d871c5e69d46 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 23 Oct 2019 19:51:00 +0200
Subject: [PATCH] [tests] checks that typing reject prog with two locals with
same name and scope
even if one is ghost and the other non-ghost
---
tests/syntax/ghost_local_ill_formed.i | 12 ++++++++++++
.../syntax/oracle/ghost_local_ill_formed.res.oracle | 6 ++++++
2 files changed, 18 insertions(+)
create mode 100644 tests/syntax/ghost_local_ill_formed.i
create mode 100644 tests/syntax/oracle/ghost_local_ill_formed.res.oracle
diff --git a/tests/syntax/ghost_local_ill_formed.i b/tests/syntax/ghost_local_ill_formed.i
new file mode 100644
index 00000000000..964f39e9080
--- /dev/null
+++ b/tests/syntax/ghost_local_ill_formed.i
@@ -0,0 +1,12 @@
+void titi() {
+ int c = 0;
+ L0: ;
+ /* ill-formed: in ghost mode, we have two local c in the same scope. */
+ /*@ ghost int c = 1; */
+ L1: ;
+ c = 2;
+ /*@ assert c == 1; */
+ /*@ assert \at(c,L0) == 0; */
+ /*@ assert \at(c,L1) == 1; */
+ /*@ assert c == 2; */
+}
diff --git a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
new file mode 100644
index 00000000000..7e293cd87e7
--- /dev/null
+++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/syntax/ghost_local_ill_formed.i (no preprocessing)
+[kernel] tests/syntax/ghost_local_ill_formed.i:5: User Error:
+ redefinition of 'c' in the same scope.
+ Previous declaration was at tests/syntax/ghost_local_ill_formed.i:2
+[kernel] User Error: stopping on file "tests/syntax/ghost_local_ill_formed.i" that has errors.
+[kernel] Frama-C aborted: invalid user input.
--
GitLab