diff --git a/Changelog b/Changelog
index 5dab589c8ceb37ee25958137e63c378b70faa046..b26eccb84dcbd1b45dc282e85df27739e89d53d8 100644
--- a/Changelog
+++ b/Changelog
@@ -17,9 +17,33 @@
Open Source Release <next-release>
##################################
+####################################
+Open Source Release 19.0 (Potassium)
+####################################
+
+-* RTE [2019/05/24] fixes a crash when visiting variable declarations
+- Eva [2019/04/19] The new annotation /*@ split exp; */ enumerates the
+ possible values of an expression and continues the analysis
+ for each of these value separately, until a /*@ merge exp; */
+ is encountered. It is also possible to maintain this partitioning
+ at all times with the option -eva-partition-value exp.
+- Eva [2019/04/19] New option -eva-partition-history N to delay the join
+ of abstract states for up to N merging points, thus keeping these
+ states separate longer. Useful when a reasoning depends on the
+ path taken to reach a control point, but can increase the analysis
+ time exponentially in N.
+- Eva [2019/04/19] Loop unroll annotations now accept non-constant but
+ bounded expressions as the maximum number of unrollings to perform.
-* Kernel [2019/04/09] Avoid crashing on one-letter attributes. Fixes #2432
-* Obfuscator [2019/04/09] Also obfuscate formals in function pointer types.
Fixes #2433.
+- Eva [2019/04/05] Prints an analysis summary at the end, outlining the
+ analysis coverage and the number of errors, warnings and emitted
+ alarms. It can be disabled with the option -eva-msg-key=-summary
+- Eva [2019/04/03] New option -eva-precision to globally configure the
+ analysis from 0 (fast but imprecise) to 11 (accurate but slow).
+ A precision of 5 is often a reasonable trade-off. This meta-option
+ automatically sets up other options that can also be overriden.
- Inout [2019/04/01] Fix performance issue when initializing large arrays.
- ACSL [2019/03/08] Add check annotation, similar to assert except that
it does not introduce additional hypotheses on the program state
diff --git a/INSTALL.md b/INSTALL.md
index 1aee10e1768f5042fa56a4bcc3b1652ce59a36cc..d7c390f5c978b6d91875836cf99f709914d84be5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -78,14 +78,14 @@ so that we can add it to the Frama-C `depext` package.
### Known working configuration
The following set of packages is known to be a working configuration for
-Frama-C 18 (Argon):
+Frama-C 19 (Potassium):
- OCaml 4.05.0
- alt-ergo-free.2.0.0 (optional)
- apron.20160125 (optional)
- coq.8.9.0 (optional)
-- lablgtk.2.18.5
-- mlgmpidl.1.2.7 (optional)
+- lablgtk.2.18.5 | lablgtk3.3.0.beta5 + lablgtk3-sourceview3.3.0.beta5
+- mlgmpidl.1.2.9 (optional)
- ocamlgraph.1.8.8
- why3.1.2.0 (optional)
- why3-coq.1.2.0 (optional)
@@ -206,7 +206,7 @@ Debian/Ubuntu: `apt-get install frama-c`
Fedora: `dnf install frama-c`
-Arch Linux: `yaourt -S frama-c`
+Arch Linux: `pikaur -S frama-c`
## Compiling from source
@@ -219,7 +219,7 @@ Arch Linux: `yaourt -S frama-c`
Note that OCaml >= 4.02.3 is needed in order to compile Frama-C.
2. (Optional) For the GUI, also install Gtk, GtkSourceView, GnomeCanvas and
- Lablgtk2 if not already installed.
+ Lablgtk2 or Lablgtk3 + Lablgtksourceview3 if not already installed.
See section 'REQUIREMENTS' below for indications on the names of the
packages to install, or use 'opam depext' as explained in section 'Opam'
above.
@@ -254,9 +254,9 @@ Arch Linux: `yaourt -S frama-c`
The Frama-C GUI also requires:
- Gtk (>= 2.4)
-- GtkSourceView 2.x
-- GnomeCanvas 2.x
-- LablGtk >= 2.18.5
+- GtkSourceView 2.x or 3.x (compatible with your Gtk version)
+- GnomeCanvas 2.x (only for Gtk 2.x)
+- LablGtk >= 2.18.5 or Lablgtk3 >= beta5 + corresponding Lablgtksourceview3
Plugins may have their own requirements.
Consult their specific documentations for details.
diff --git a/VERSION b/VERSION
index 3a48ff126f4f03ea3b2eb133fb1b2de6bb40e772..8f08de2f1dcbcd644edd53ebb9dbf9ce6bb2f9e9 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-18.0+dev
\ No newline at end of file
+19.0-beta
\ No newline at end of file
diff --git a/VERSION_CODENAME b/VERSION_CODENAME
index fadca8279f3625001cf7cc3aba222a3640c7c4da..8d95dee9720e5b6f4f1900350d74569e45a0f7ff 100644
--- a/VERSION_CODENAME
+++ b/VERSION_CODENAME
@@ -1 +1 @@
-Argon
\ No newline at end of file
+Potassium
\ No newline at end of file
diff --git a/doc/release/branch.tex b/doc/release/branch.tex
index d20f396842f71dfd00f7f0ba2843b2d26caefad5..cee2baa582779a3ef7f7abfef40047396a44ff54 100644
--- a/doc/release/branch.tex
+++ b/doc/release/branch.tex
@@ -54,9 +54,9 @@ the Changelog.
\begin{itemize}
\item Add the following in the Changelog, in \texttt{stable/element}
\begin{verbatim}
- #############################
- Open Source Release <element>
- #############################
+ ####################################
+ Open Source Release <nb> (<element>)
+ ####################################
\end{verbatim}
This should go directly below
diff --git a/opam/opam b/opam/opam
index bda948e9199b27790ffd9fac8029f18e26587ee0..6d397bf21e359a873874cea691ddf2ca6a149489 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "18.0"
+version: "19.0.beta1"
maintainer: "francois.bobot@cea.fr"
authors: [
"Michele Alberti"
@@ -28,6 +28,7 @@ authors: [
"David Maison"
"Claude Marché"
"André Maroneze"
+ "Thibault Martin"
"Melody Méaulle"
"Benjamin Monate"
"Yannick Moy"
@@ -36,6 +37,7 @@ authors: [
"Guillaume Petiot"
"Virgile Prevosto"
"Armand Puccetti"
+ "Virgile Robles"
"Muriel Roger"
"Julien Signoles"
"Kostyantyn Vorobyov"
@@ -44,7 +46,7 @@ authors: [
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://github.com/Frama-C/Frama-C-snapshot.git#latest"
-doc: "http://frama-c.com/download/user-manual-18.0-Argon.pdf"
+doc: "http://frama-c.com/download/user-manual-19.0-Potassium.pdf"
bug-reports: "https://bts.frama-c.com/"
tags: [
"deductive"
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index df7931022fe0916c4305b2b531a9c302032d2a14..d9be7dfb47901441f0af3e63a90546f2722bdf26 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -523,6 +523,7 @@ endif # FRAMAC_INTERNAL
$(TARGET_META):
$(PRINT_MAKING) $(notdir $@)
$(RM) $@
+ $(MKDIR) $(dir $@)
$(ECHO) "description = \"$($(notdir $@).DESCRIPTION)\"" >> $@
$(ECHO) "version = \"$($(notdir $@).VERSION)\"" >> $@
$(ECHO) "requires = \"frama-c.kernel $($(notdir $@).REQUIRES)\"" >> $@
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index 055d3b33c18c680a827179523038538884c4782f..9c7a1deca88295e697376d398d26d6c7e38360ca 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -46,6 +46,7 @@ let show main_ui =
"David Maison";
"Claude Marché";
"André Maroneze";
+ "Thibault Martin";
"Melody Méaulle";
"Benjamin Monate";
"Yannick Moy";
@@ -54,6 +55,7 @@ let show main_ui =
"Guillaume Petiot";
"Virgile Prevosto";
"Armand Puccetti";
+ "Virgile Robles";
"Muriel Roger";
"Julien Signoles";
"Kostyantyn Vorobyov";
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 664c6cce8929d7a36618b53fc429e11033cf2c19..a5e8ad38578f28365e4d918436372992d73386f9 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -108,10 +108,21 @@ class annot_visitor kf flags on_alarm = object (self)
method private generate_assertion: 'a. 'a Rte.alarm_gen -> 'a -> unit =
fun fgen ->
- let stmt = Extlib.the (self#current_stmt) in
- let on_alarm ~invalid a = on_alarm stmt ~invalid a in
+ let curr_stmt = self#current_stmt in
+ let on_alarm ~invalid a =
+ match curr_stmt with
+ | None -> Options.warning ~current:true
+ "Alarm generated outside any statement:@ %a"
+ Alarms.pretty a
+ | Some stmt -> on_alarm stmt ~invalid a
+ in
fgen ~remove_trivial:flags.Flags.remove_trivial ~on_alarm
+ (* Do not visit variable declarations, as no alarm should be emitted here,
+ and there is no statement to emit an alarm anyway ([generate_assertion]
+ or [Alarms.register] would then crash). *)
+ method !vvdec _ = Cil.SkipChildren
+
method! vstmt s = match s.skind with
| UnspecifiedSequence l ->
(* UnspecifiedSequences may contain lvals for side-effects, that
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index ad8f3ee31756e09f77fa14d3b11e581c534ae6bf..c90573422be52a7c907c16cf8a120da6b736ec73 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -21,6 +21,10 @@
###############################################################################
- Qed [2019/05/09] Transforms some boolean quantifications into let constructs
+##########################
+Plugin WP 19.0 (Potassium)
+##########################
+
- Wp [2019/05/09] Fixes -wp-simplify-is-cint simplifier
- Wp [2019/04/26] Now requires -warn-invalid-bool
- Wp [2019/04/26] Removed option -wp-bool-range
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index ee4873009165e22899179f66be430c6c3e3f9841..ba1717b81d56b94e955e972cd0c517d593abd266 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -318,7 +318,8 @@ byte:: $(Wp_DIR)/share/why3/why3.conf
opt:: $(Wp_DIR)/share/why3/why3.conf
$(Wp_DIR)/share/why3/why3.conf: config.status $(Wp_DIR)/Makefile.in
- @echo Generation of the extra-config for why3
+ $(PRINT_MAKING) "extra-config for why3"
+ $(RM) $@
@printf "[prover_modifiers]\n" >> $@
@printf "name=\"Coq\"\n" >> $@
@printf "option=\"-Q $(FRAMAC_DATADIR)/wp/why3 ''\"\n" >> $@
@@ -329,7 +330,7 @@ $(Wp_DIR)/share/why3/why3.conf: config.status $(Wp_DIR)/Makefile.in
@printf "\n" >> $@
@printf "[editor_modifiers proofgeneral-coq]\n" >> $@
@printf "option=\"--eval \\\\\"(setq coq-load-path (cons '(\\\\\\\\\\\\\"$(FRAMAC_DATADIR)/wp/why3\\\\\\\\\\\\\" \\\\\\\\\\\\\"\\\\\\\\\\\\\") coq-load-path))\\\\\"\"\n" >> $@
- @chmod u-w $@
+ $(CHMOD_RO) $@
# --------------------------------------------------------------------------
# --- Installation ---
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 38e73ded32b279bd105fbbd4848bc61e7ea326b5..61230201355a42ea080a7dcd676971d9832c62cf 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -323,6 +323,13 @@ end
(* --- Assembling Goal --- *)
(* -------------------------------------------------------------------------- *)
+let sanitize_expl fmt title =
+ for i = 0 to String.length title - 1 do
+ match title.[i] with
+ | '\n' | '\t' -> Format.pp_print_char fmt ' '
+ | c -> Format.pp_print_char fmt c
+ done
+
let assemble_goal ~id ~title ~theory ?axioms prop fmt =
(** Also create the directory *)
let goal = cluster ~id ~title () in
@@ -348,9 +355,9 @@ let assemble_goal ~id ~title ~theory ?axioms prop fmt =
engine#set_goal true ;
engine#global
begin fun () ->
- v#printf "@[<hv 2>goal %s[@expl:%s]:@ %a@]@\n@\n"
+ v#printf "@[<hv 2>goal %s[@expl:%a]:@ %a@]@\n@\n"
why3_goal_name
- title
+ sanitize_expl title
engine#pp_prop (F.e_prop prop) ;
end ;
engine#set_goal false ;
diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise
index b20a057439a25d8d78b9cebdd31242a7f6e83f47..3fcbca6757345103c83d94f888ffb987b29a2bd7 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];
---
diff --git a/tests/rte/array_index.c b/tests/rte/array_index.c
index 85c8c6bd1ddbf1a68b88992f3e5ca834aa44f37f..b976e42cce80e05920e1870208d858e4db473a18 100644
--- a/tests/rte/array_index.c
+++ b/tests/rte/array_index.c
@@ -44,4 +44,7 @@ void main(int i, int j, unsigned int k) {
s.t[k] = 0;
s.s.u[k] = 0;
s.v[k].t[c[k]] = 0;
+
+ int x;
+ int t[100 / sizeof(x)];
}
diff --git a/tests/rte/oracle/array_index.0.res.oracle b/tests/rte/oracle/array_index.0.res.oracle
index 6acdd373586e604dd2da7626f9e3051dfde58a75..5c3fb974325cbda6d9de1021b6dbb256232021df 100644
--- a/tests/rte/oracle/array_index.0.res.oracle
+++ b/tests/rte/oracle/array_index.0.res.oracle
@@ -20,6 +20,8 @@ ts s;
unsigned int c[10];
void main(int i, int j, unsigned int k)
{
+ int x;
+ int t_0[(unsigned int)100 / sizeof(x)];
t[0] = 0;
u[1] = 0;
v[2][3] = 0;
@@ -89,6 +91,8 @@ ts s;
unsigned int c[10];
void main(int i, int j, unsigned int k)
{
+ int x;
+ int t_0[(unsigned int)100 / sizeof(x)];
/*@ assert rte: index_bound: 0 ≤ 0; */
/*@ assert rte: index_bound: 0 < 10; */
t[0] = 0;
diff --git a/tests/rte/oracle/array_index.1.res.oracle b/tests/rte/oracle/array_index.1.res.oracle
index 31cf7a921b3d4ccc106b05db4eda7683c0acae49..79017aa000bce2cb6547667f2d43b6cf3088cdba 100644
--- a/tests/rte/oracle/array_index.1.res.oracle
+++ b/tests/rte/oracle/array_index.1.res.oracle
@@ -20,6 +20,8 @@ ts s;
unsigned int c[10];
void main(int i, int j, unsigned int k)
{
+ int x;
+ int t_0[(unsigned int)100 / sizeof(x)];
t[0] = 0;
u[1] = 0;
v[2][3] = 0;