← Back to branch summary

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

« back to all changes in this revision

Viewing changes to tests/slicing/ex_spec_interproc.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/ex_spec_interproc.ml
 
1
(* ledit bin/toplevel.top -deps tests/slicing/ex_spec_interproc.c
 
2
  #use "tests/slicing/select.ml";;
 
3
ou
 
4
  #use "tests/slicing/ex_spec_interproc.ml";;
 
5
 
 
6
*)
 
7
 
 
8
include LibSelect;;
 
9
 
 
10
(*--------------------------*)
 
11
(* find the kernel functions *)
 
12
let kf_g = Globals.Functions.find_def_by_name "g";;
 
13
let kf_f = Globals.Functions.find_def_by_name "f";;
 
14
let kf_main = Globals.Functions.find_def_by_name "main";;
 
15
 
 
16
(* add a request to select f result (output 0) in the project *)
 
17
let select_f_out0 project =
 
18
  let ff_f = !S.Slice.create project kf_f in
 
19
  let select = select_retres project kf_f in
 
20
    !S.Request.add_slice_selection_internal project ff_f select;
 
21
    print_requests project;
 
22
    ff_f
 
23
;;
 
24
 
 
25
 
 
26
(*===========================================================================*)
 
27
(* DEBUT DU TEST *)
 
28
(*===========================================================================*)
 
29
(* mode DontSliceCalls *)
 
30
Cmdline.Slicing.Mode.Calls.set 0;;
 
31
 
 
32
let project = mk_project ();;
 
33
let _ff_f = select_f_out0 project;;
 
34
!S.Request.apply_all_internal project; print_project project;;
 
35
extract_and_print project;;
 
36
 
 
37
(*===========================================================================*)
 
38
(* mode PropagateMarksOnly *)
 
39
Cmdline.Slicing.Mode.Calls.set 1;;
 
40
 
 
41
let project = mk_project ();;
 
42
let _ff_f = select_f_out0 project;;
 
43
!S.Request.apply_all_internal project; print_project project;;
 
44
extract_and_print project;;
 
45
 
 
46
(*===========================================================================*)
 
47
(* mode MinimizeNbCalls *)
 
48
Cmdline.Slicing.Mode.Calls.set 2;;
 
49
 
 
50
let project = mk_project ();;
 
51
 
 
52
(* slice 'f' to compute its result (output 0) and propagate to 'g' *)
 
53
let ff_f = select_f_out0 project;;
 
54
!S.Request.apply_all_internal project; print_project project;;
 
55
 
 
56
(* call 'f' slice in 'main' *)
 
57
let ff_main = !S.Slice.create project kf_main;;
 
58
!S.Request.add_call_slice project ~caller:ff_main ~to_call:ff_f;;
 
59
!S.Request.apply_all_internal project; print_project project;
 
60
 
 
61
extract_and_print project;;
 
62
 
 
63
(*---------------------------------------------- *)
 
64
(* test remove_slice and select_stmt_computation *)
 
65
 
 
66
(* we remove ff_main : ff_f should not be called anymore *)
 
67
!S.Slice.remove project ff_main;;
 
68
print_project project;;
 
69
 
 
70
(* try to change ff_f to check that ff_main is not in its called_by anymore *)
 
71
(* select "a" before inst 14 (d++) *)
 
72
(* VP: initial value of 34 does not refer to d++ (was 30) 9 corresponds
 
73
   to d++. old ki 34 corresponds to return(X), new ki 13 *)
 
74
print_stmt project kf_f;;
 
75
let ki,_ = Kernel_function.find_from_sid 10(*34*) in (* d++ *)
 
76
let select = select_data_before_stmt "a" ki project kf_f in
 
77
  !S.Request.add_slice_selection_internal project ff_f select;;
 
78
print_requests project;;
 
79
!S.Request.apply_all_internal project; print_project project;;
 
80
 
 
81
(*===========================================================================*)
 
82
(* Test 'extract' when there are 2 slices for the same function *)
 
83
Cmdline.Slicing.Mode.Calls.set 2;;
 
84
let project = mk_project ();;
 
85
 
 
86
let ff_f_1 = !S.Slice.create project kf_f;;
 
87
let select = select_retres project kf_f in
 
88
  !S.Request.add_slice_selection_internal project ff_f_1 select;;
 
89
 
 
90
let ff_f_2 = !S.Slice.create project kf_f;;
 
91
let select = select_data "Z" project kf_f in
 
92
  !S.Request.add_slice_selection_internal project ff_f_2 select;;
 
93
 
 
94
!S.Request.apply_all_internal project;;
 
95
print_ff ff_f_2;;
 
96
 
 
97
extract_and_print project;;
 
98
(*===========================================================================*)
 
99
(* mode PreciseSlices *)
 
100
Cmdline.Slicing.Mode.Calls.set 3;;
 
101
 
 
102
let project = test_select_retres ~do_prop_to_callers:true "f" ;;
 
103
 
 
104
print_project project;;
 
105
(*===========================================================================*)