diff --git a/Changelog b/Changelog index 500b14a66b345db189acc38a851bef80a279b305..b26eccb84dcbd1b45dc282e85df27739e89d53d8 100644 --- a/Changelog +++ b/Changelog @@ -21,6 +21,7 @@ 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; */ 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/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;