~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to src/value/state_set.ml

• browse files at revision 1
• compare with another revision
• download diff
• download tarball
• view history from revision 1

Show diffs side-by-side

added

removed

src/value/state_set.ml

 

1

(**************************************************************************)

 

2

(*                                                                        *)

 

3

(*  This file is part of Frama-C.                                         *)

 

4

(*                                                                        *)

 

5

(*  Copyright (C) 2007-2008                                               *)

 

6

(*    CEA (Commissariat � l'�nergie Atomique)                             *)

 

7

(*                                                                        *)

 

8

(*  you can redistribute it and/or modify it under the terms of the GNU   *)

 

9

(*  Lesser General Public License as published by the Free Software       *)

 

10

(*  Foundation, version 2.1.                                              *)

 

11

(*                                                                        *)

 

12

(*  It is distributed in the hope that it will be useful,                 *)

 

13

(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)

 

14

(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)

 

15

(*  GNU Lesser General Public License for more details.                   *)

 

16

(*                                                                        *)

 

17

(*  See the GNU Lesser General Public License version 2.1                 *)

 

18

(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)

 

19

(*                                                                        *)

 

20

(**************************************************************************)

 

21

 

 

22

(* $Id: state_set.ml,v 1.7 2008/04/01 09:25:22 uid568 Exp $ *)

 

23

 

 

24

type t = Relations_type.Model.t list

 

25

let fold = List.fold_right

 

26

let iter = List.iter

 

27

let exists = List.exists

 

28

let for_all = List.for_all

 

29

let filter = List.filter

 

30

let is_empty l = l =[]

 

31

let empty = []

 

32

let elements e = e

 

33

let length s = List.length s

 

34

 

 

35

exception Unchanged

 

36

let pretty fmt set =

 

37

  List.iter

 

38

    (fun state ->

 

39

       Format.fprintf fmt "set contains %a@\n"

 

40

         Relations_type.Model.pretty state)

 

41

    set

 

42

 

 

43

let rec length_at_most_n l n =

 

44

  if n < 0 

 

45

  then false

 

46

  else match l with

 

47

    [] -> true

 

48

  | _ :: t -> length_at_most_n t (pred n)

 

49

      

 

50

let add_exn v s =

 

51

(*  let len = List.length s in if len >= 3 then

 

52

      Format.printf "State_set:%4d@." (List.length s); *)

 

53

  if length_at_most_n s 50

 

54

  then begin

 

55

      if (not (Relations_type.Model.is_reachable v)) ||

 

56

        List.exists

 

57

        (fun e -> Relations_type.Model.is_included v e)

 

58

        s

 

59

      then raise Unchanged

 

60

      else

 

61

        let s =

 

62

          List.filter

 

63

            (fun e -> not (Relations_type.Model.is_included e v))

 

64

            s

 

65

        in

 

66

        v::s

 

67

    end

 

68

  else begin

 

69

      if Relations_type.Model.is_reachable v then v :: s else raise Unchanged 

 

70

    end

 

71

 

 

72

 

 

73

 

 

74

let merge_into a b =

 

75

  let unchanged = ref true in

 

76

  let f acc e =

 

77

    try

 

78

      let r = add_exn e acc in

 

79

      unchanged := false;

 

80

      r

 

81

    with Unchanged ->

 

82

      acc

 

83

  in

 

84

  let result = List.fold_left f b a in

 

85

  if !unchanged then raise Unchanged;

 

86

  result

 

87

 

 

88

let add v s =

 

89

  try

 

90

    add_exn v s

 

91

  with Unchanged -> s

 

92

 

 

93

let singleton v = add v []

 

94

 

 

95

let cardinal = List.length

 

96

 

 

97

let join l =

 

98

  List.fold_left Relations_type.Model.join Relations_type.Model.bottom l

 

99

 

 

100

(*

 

101

Local Variables:

 

102

compile-command: "LC_ALL=C make -C ../.. -j"

 

103

End:

 

104

*)

 

105

 

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1