1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
open Cil
open Cil_types
class check =
object(self)
inherit Visitor.frama_c_inplace
val current_loop = Stack.create ()
method vstmt_aux s =
let res =
match s.skind with
| Loop _ -> Stack.push s current_loop;
ChangeDoChildrenPost
(s,
fun s -> ignore (Stack.pop current_loop); s)
| _ -> DoChildren
in
let has_loop =
try
Some
(Kernel_function.find_enclosing_loop (Extlib.the self#current_kf) s)
with Not_found -> None
in
(match has_loop with
| Some s -> assert (s == Stack.top current_loop)
| None -> assert (Stack.is_empty current_loop));
res
end
let run () =
Visitor.visitFramacFileSameGlobals (new check) (Ast.get());
Kernel.result "Script done"
let () = Db.Main.extend run
|
