source: Deliverables/D5.1/cost-plug-in/plugin/help/mailinglisthelp @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 6.9 KB
Line 
1
2
3>I can't understand the difference between the GFun node and the kernel_function. sspec can't be completely irrelevant, I presume.
4
5Well, for most practical purposes, sspec is irrelevant. It is only used
6in freshly type-checked AST, until Frama-C's internal tables are
7properly filled. It's not a stage where plug-ins intervene much (in
8fact, there isn't any hook to do so).
9
10> The only thing changing is indeed the vspec, but it changes with regards to what is in the function itself, we need to process the body (with vglob_aux) in order to get "what to put" in the postcondition (with vspec).
11
12OK, then you're right, it makes sense to use vglob_aux to do that.
13
14>
15> So we need to also override vglob_aux.
16> The thing is, we don't know the specific order in which these two (vglob_aux and vspec) are gonna be called.
17
18the spec is somehow a child of the function, thus vspec is called after
19vglob_aux (on the other hand, an action in ChangeDoChildrenPost for
20vspec will be performed before an action in ChangeDoChildrenPost for
21vglob_aux)
22
23> Isn't there an easier way to use Visitor.current_kf and set_current_kf, to link the generated GFun node, with the associated kernel_function?
24
25Unfortunately no: current_kf always refer to original function being
26visited. In fact, since the visitor can return more than
27one global (or for that matter, to turn a decl into def or vice-versa),
28it is not really possible to have a current_kf for the new function in
29the general case. Only the original one is meaningful.
30
31--
32Virgile Prevosto
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51Hello! Me again!
52>
53> Right, so everything works, thank you so much for your help!
54> But when we use
55> ? Cil.d_global Format.std_formatter annotatedFun ;
56> It prints, on the std_out, exactly what we want, the ensure clause is right where we need it.
57>
58> But there's nothing in the outed file, it doesn't change the GFun nodes into Annotated GFun nodes (adding an ensure clause).
59> The colored parts are of interest...
60> ___________________________________________
61> ? method vglob_aux g=
62> ??? begin match g with
63> ????? | GFun (oldFundec,location1) ->
64> ????? (*...other things here...*)
65> ??? ? let newFundec = ??? ??
66> ??? ??? {oldFundec with sspec = newSpecc} in
67> ??? ? let annotatedFun = GFun (newFundec,location1)
68> ??? ? in
69> ??? ?? Cil.d_global Format.std_formatter annotatedFun ; (*shows an annotated fun*)
70> ???? (*? ChangeDoChildrenPost ( [annotatedFun], fun x -> x)? didn't work either*)
71> ??? ?? ChangeToPost( [annotatedFun], fun x -> x)???? (*Doesn't seem to be working...*)
72> ????? | _ ->? JustCopy
73> ??? end
74> ?____________________________________________ ???
75>
76> In case ChangeToPost wasn't the problem, here's how we do the copy afterwards,
77> In another .ml, we apply CerCo, it passes to cost, here, a Cabs.file, the name of the incrementation function, and the global var to be incremented.
78>
79
80in Frama-C, the sspec field is not relevant: it's the spec field in the
81associated kernel_function that reflects the real annotation (the dev's
82manual for more information). If the only thing that you're changing in
83GFun is the specification, I guess that DoChildren on GFun and
84overriding vspec is the easiest way to obtain what you want: the
85generic visitor itself will take care of putting the new spec in the
86appropriate place.
87
88Note however that vspec is visited from 3 places
89- function prototypes (without a corresponding def)
90- function definitions
91- statement contract
92
93You can discriminate between the three with self#current_func (None for
94prototype) and self#current_statement (None for function definition
95(and prototype of course)).
96
97All definitions and prototypes have a specification, that can be empty,
98so vspec will be called for each definition (it is called from a
99GVarDecl iff there's no corresponding GFun to avoid visiting the same
100spec twice).
101
102Hope this helps,
103--
104E tutto per oggi, a la prossima volta.
105Virgile
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138As Patrick said, File.pretty_ast is your friend. You have to give as
139argument your project and a formatter corresponding to the file you want
140to create (or to set option -ocode programatically).
141
142More generally, you can use Project.set_current (resp. Project.on) to
143change the current project globally (resp. locally): then any function
144is applied on the given project.
145
146Here is a small exemple which duplicates the current project and pretty
147print the AST of the new project in "my_file.i".
148
149===
150let main () =
151   let prj =
152     (* just duplicate the current project *)
153     File.create_project_from_visitor
154       "my_project"
155       (fun prj -> new Visitor.frama_c_copy prj)
156   in
157   Project.on
158     prj
159     (fun p ->
160       Parameters.CodeOutput.set "my_file.i";
161       (* no argument given to File.pretty_ast:
162          implicitely printed the AST of project [prj]
163          into file "my_file.i". *)
164       File.pretty_ast ())
165     ()
166
167let () = Db.Main.extend main
168===
169
170> We tried without putting the annotatedFun in a list, it resulted in an
171> error, and we cannot figure out why.
172> The guide says that the visit action replaces the node with the given
173> node. the GFun we matched upon was a node, annotatedFun is a node,
174> [annotatedFun] is a list. Why is that?
175
176The guide is right for most nodes, but there is at least one exception ;-).
177
178The method vglob_aux has type global -> global list Cil.visitAction.
179Thus you are to put a list. The reason is that you might insert some new
180globals into the AST.
181
182Do not hesitate to have a look at the kernel API
183(http://frama-c.com/download/frama-c-Carbon-20110201_api.tar.gz) to get
184the exact expected type of a function.
185
186> [1] For this, we use Logic_const.tvar which takes, at some point, a
187> logic_var.
188>
189> and logic_var = {
190> mutable lv_name : string; (** name of the variable. *)
191> mutable lv_id : int; (** unique identifier *)
192> mutable lv_type : logic_type; (** type of the variable. *)
193> mutable lv_origin : varinfo option (** when the logic variable stems from a
194> C variable, set to the original C variable.
195> *)
196> }
197>
198> At some point in the commented area over the identified_term type, in
199> the Cil_types.mli, we read
200> Use [Logic_const.new_location] to generate a new id. *)
201> But this method isn't in the Logic_const module, nor anywhere else in
202> the source of the Carbon version.
203
204That is a documentation error which can be reported to our BTS
205(bts.frama-c.com).
206
207> How can we set up the lv_id? Having no options, we used
208> Logic_const.fresh_term_id (); is that okay?
209
210Not really: that not the expected counter there.
211
212The simplest way to create a new logic variable is to call function
213Cil_const.make_logic_var and let it to choose a valid id.
214
215Smart constructors for AST nodes are in one of the following modules:
216Cil, Cil_const, Logic_const or Logic_utils. I agree that it is not
217always easy to find what you are searching in the API.
218
219Hope this helps,
220Julien Signoles
221--
222Ing?nieur-Chercheur
223CEA LIST, Laboratoire de S?ret? des Logiciels
224point courrier 94, 91191 Gif-Sur-Yvette Cedex
225tel:(+33)1.69.08.71.82  fax:(+33)1.69.08.83.95
Note: See TracBrowser for help on using the repository browser.