package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file path_analysis.ml

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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Aorai plug-in of Frama-C.                        *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*    INRIA (Institut National de Recherche en Informatique et en         *)
(*           Automatique)                                                 *)
(*    INSA  (Institut National des Sciences Appliquees)                   *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Automaton_ast

let voisins (_,trans_l) st =
  List.fold_left
    (fun vl tr -> if tr.start.nums=st.nums then (tr.stop,1)::vl else vl)
    []
    trans_l

let empty () = [] ;;
let is_empty heap = (List.length heap)=0 ;;
let add (length,(st,path)) heap = (length,(st,path))::heap ;;
let extract_min heap =
  let (min,h) =
    List.fold_left
      (fun ((lmin,min),h) (lcur,cur) ->
         if lmin<=lcur then
           ((lmin,min),(lcur,cur)::h)
         else
           ((lcur,cur),(lmin,min)::h)
      )
      ((List.hd heap),[])
      (List.tl heap)
  in
  (min,h)



(* Source : wikipedia*)

(* l'adjacence est donnee sous la forme d'une fonction : adj v est la liste des voisins de v,
   avec leur distance ; la fonction suivante cherche le plus court chemin de v1 a v2 *)
let dijkstra (adj: 'a -> ('a * int) list) (v1:'a) (v2:'a) =
  let visited = Hashtbl.create 97 in
  let rec loop h =
    if is_empty h then raise Not_found;
    let (w,(v,p)),h = extract_min h in
    if v = v2 then
      List.rev p, w
    else
      let h =
        if not (Hashtbl.mem visited v) then begin
          Hashtbl.add visited v ();
          List.fold_left (fun h (e,d) -> add (w+d, (e, e::p)) h) h (adj v)
        end else
          h
      in
      loop h
  in
  loop (add (0,(v1,[])) (empty()))

(** since Nitrogen-20111001 *)
let get_transitions_of_state st (_,tr) =
  List.fold_left
    (fun acc tr ->
       if tr.start.nums = st.nums then tr::acc else acc)
    [] tr

let get_edges st1 st2 (_,tr) =
  List.find_all
    (fun tr -> tr.start.nums = st1.nums && tr.stop.nums = st2.nums)
    tr

let get_init_states (st,_) = List.filter (fun x -> x.init = Bool3.True) st

let at_most_one_path (states,transitions as auto) st1 st2 =
  try
    let path,_ = dijkstra (voisins auto) st1 st2 in
    match path with
    | [] | [ _ ] -> true
    | x::y::_ ->
      let (trans1,trans2) =
        List.partition
          (fun t -> t.start.nums = x.nums && t.stop.nums = y.nums)
          transitions
      in
      let transitions = (List.tl trans1) @ trans2 in
      let auto = states, transitions in
      ignore (dijkstra (voisins auto) st1 st2);
      false
  with Not_found -> true
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct