← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/slicing/min_call.ml

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
tests/slicing/min_call.ml
 
1
(* ledit -h jnl bin/toplevel.top -deps  -lib-entry g -slice-callers \
 
2
                                 tests/slicing/min_call.c
 
3
 
 
4
*)
 
5
 
 
6
 
 
7
include LibSelect;;
 
8
 
 
9
Cmdline.Slicing.Mode.Calls.set 3;;
 
10
 
 
11
let kf_get = Globals.Functions.find_by_name "get";;
 
12
let kf_send = Globals.Functions.find_by_name "send";;
 
13
let kf_send_bis = Globals.Functions.find_by_name "send_bis";;
 
14
let kf_k = Globals.Functions.find_def_by_name "k";;
 
15
let kf_f = Globals.Functions.find_def_by_name "f";;
 
16
let kf_g = Globals.Functions.find_def_by_name "g";;
 
17
 
 
18
let top_mark = !Db.Slicing.Mark.make ~addr:true ~ctrl:true ~data:true ;;
 
19
 
 
20
let add_select_fun_calls project to_call =
 
21
  let selections = !Db.Slicing.Select.empty_selects () in
 
22
  let selections = !Db.Slicing.Select.select_func_calls_into selections
 
23
                                                          ~spare:false to_call
 
24
  in !Db.Slicing.Request.add_persistent_selection project selections
 
25
 
 
26
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 
27
(* Project1 :
 
28
* Select the call to [send_bis] in [k] as a persistent selection :
 
29
* this will create a fist slice for [k].
 
30
* Then create manually a second slice for [k] :
 
31
* the call to [send_bis] is visible as wished. *)
 
32
 
 
33
let project = mk_project();;
 
34
(*let pdg_k = !Db.Pdg.get kf_k;;*)
 
35
let calls = !Db.Pdg.find_call_stmts ~caller:kf_k(*pdg_k*) kf_send_bis;;
 
36
let sb_call = match calls with c::[] -> c | _ -> assert false;;
 
37
let mark = !S.Mark.make ~data:true ~addr:false ~ctrl:false;;
 
38
let select =
 
39
  !S.Select.select_stmt_internal kf_k sb_call mark;;
 
40
!S.Request.add_selection_internal project select ;;
 
41
!S.Request.apply_all_internal project;;
 
42
Format.printf "@[Project1 - result1 :@\n@]";;
 
43
extract_and_print project;;
 
44
 
 
45
let ff2_k = !S.Slice.create project kf_k;;
 
46
Format.printf "@[Project1 - result2 :@\n@]";;
 
47
!S.Project.pretty fmt project;;
 
48
extract_and_print project;;
 
49
 
 
50
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 
51
(* Project2 :
 
52
* same than project1, except that we use [select_min_call_internal].
 
53
* But as [send_bis] is an undefined function, this makes no difference.
 
54
*)
 
55
let project = mk_project();;
 
56
(*let pdg_k = !Db.Pdg.get kf_k;;*)
 
57
let calls = !Db.Pdg.find_call_stmts (*pdg_k*)~caller:kf_k kf_send_bis;;
 
58
let sb_call = match calls with c::[] -> c | _ -> assert false;;
 
59
let mark = !S.Mark.make ~data:true ~addr:false ~ctrl:false;;
 
60
let select =
 
61
  !S.Select.select_min_call_internal kf_k sb_call mark;;
 
62
!S.Request.add_selection_internal project select ;;
 
63
print_requests project;;
 
64
!S.Request.apply_all_internal project;;
 
65
Format.printf "@[Project3 - result :@\n@]";;
 
66
!S.Project.pretty fmt project;;
 
67
extract_and_print project;;
 
68
 
 
69
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 
70
(* Project3 :
 
71
* Select the calls to [k] to be visible in a minimal version.
 
72
* This builds an empty slice [k_1] for [k] and call it in [f] and [g].
 
73
* [f_1] is also called in [g_1] because it calls [k_1].
 
74
*)
 
75
 
 
76
let project = mk_project();;
 
77
add_select_fun_calls project kf_k;;
 
78
print_requests project;;
 
79
!S.Request.apply_next_internal project;;
 
80
print_requests project;;
 
81
!S.Request.apply_all_internal project;;
 
82
Format.printf "@[Project3 - result :@\n@]";;
 
83
!S.Project.pretty fmt project;;
 
84
extract_and_print project;;
 
85
 
 
86
 
 
87
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 
88
(* Project4 is CAS_1 from Patrick's 19th April 2007 mail.
 
89
* step 1 - select calls to send and apply : OK
 
90
* step 2 - (automatically done in step1)
 
91
* step 3 - select calls to send_bis and apply : TODO
 
92
* step 4 - (automatically done in step3)
 
93
*)
 
94
 
 
95
(*
 
96
let project = mk_project();;
 
97
 
 
98
add_select_fun_calls project kf_send;;
 
99
print_requests project;;
 
100
!S.Request.apply_next_internal project;;
 
101
print_requests project;;
 
102
!S.Request.apply_all_internal project;;
 
103
 
 
104
Format.printf "@[CAS 1 - step 1+2 - result :@\n@]";;
 
105
extract_and_print project;;
 
106
 
 
107
add_select_fun_calls project kf_send_bis;;
 
108
print_requests project;;
 
109
!S.Request.apply_all_internal project;;
 
110
 
 
111
Format.printf "@[CAS 1 - step 3+4 - result :@\n@]";;
 
112
!S.Project.pretty fmt project;;
 
113
extract_and_print project;;
 
114
*)
 
115
 
 
116
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
 
117
(* Project5 : same than the previous one,
 
118
* except that we create the two requests before applying.
 
119
* *)
 
120
 
 
121
(*
 
122
let project = mk_project();;
 
123
 
 
124
add_select_fun_calls project kf_send;;
 
125
add_select_fun_calls project kf_send_bis;;
 
126
print_requests project;;
 
127
 
 
128
Format.printf "@[Project 5 - result :@\n@]";;
 
129
!S.Project.pretty fmt project;;
 
130
extract_and_print project;;
 
131
*)
 
132
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)