From d12915079fa7f8a2980951f9fe978a2138d81cf7 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 16 Mar 2020 10:06:17 +0100
Subject: [PATCH] [eacsl:analyses] Add tracking of jumps from switch to case
statements
---
src/plugins/e-acsl/src/analyses/exit_points.ml | 13 ++++++++++---
1 file changed, 10 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/exit_points.ml b/src/plugins/e-acsl/src/analyses/exit_points.ml
index d2de4ede3a5..f774c12460f 100644
--- a/src/plugins/e-acsl/src/analyses/exit_points.ml
+++ b/src/plugins/e-acsl/src/analyses/exit_points.ml
@@ -58,7 +58,8 @@ module SLocals = Build_env(struct type t = Varinfo.Set.t end)
done for consistency, so all required information is stored uniformly. *)
module Exits = Build_env(struct type t = stmt end)
-(* Map labelled statements back to gotos which lead to them *)
+(* Map labelled statements back to gotos which lead to them and case statements
+ back to the corresponding switch *)
module LJumps = Build_env(struct type t = stmt end)
let clear () =
@@ -117,11 +118,17 @@ class jump_context = object (_)
| [] -> ()
| _ :: _ -> SLocals.add stmt (unify_sets locals)
in
- match stmt.skind with
- | Loop _ | Switch _ ->
+ let handle_jumps stmt =
SLocals.add stmt (unify_sets locals);
Stack.push stmt jumps;
Cil.DoChildrenPost (fun st -> ignore(Stack.pop jumps); st)
+ in
+ match stmt.skind with
+ | Loop _ ->
+ handle_jumps stmt
+ | Switch (_, _, case_stmts, _) ->
+ List.iter (fun s -> LJumps.add s stmt) case_stmts;
+ handle_jumps stmt
| Break _ | Continue _ ->
Exits.add stmt (Stack.top jumps);
SLocals.add stmt (unify_sets locals);
--
GitLab