Skip to content

Commit f305de6

Browse files
reukreuk
committed
Reformat doc comments in src
1 parent bca08dd commit f305de6

File tree

1,027 files changed

+6118
-61261
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,027 files changed

+6118
-61261
lines changed

‎src/analyses/ai.cpp

+15-216
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
/// \file
10+
/// Abstract Interpretation
11+
912
#include <cassert>
1013
#include <memory>
1114

@@ -16,18 +19,6 @@ Author: Daniel Kroening, [email protected]
1619

1720
#include "ai.h"
1821

19-
/*******************************************************************\
20-
21-
Function: ai_baset::output
22-
23-
Inputs:
24-
25-
Outputs:
26-
27-
Purpose:
28-
29-
\*******************************************************************/
30-
3122
void ai_baset::output(
3223
const namespacet &ns,
3324
const goto_functionst &goto_functions,
@@ -47,18 +38,6 @@ void ai_baset::output(
4738
}
4839
}
4940

50-
/*******************************************************************\
51-
52-
Function: ai_baset::output
53-
54-
Inputs:
55-
56-
Outputs:
57-
58-
Purpose:
59-
60-
\*******************************************************************/
61-
6241
void ai_baset::output(
6342
const namespacet &ns,
6443
const goto_programt &goto_program,
@@ -79,18 +58,9 @@ void ai_baset::output(
7958
}
8059
}
8160

82-
/*******************************************************************\
83-
84-
Function: ai_baset::output_json
85-
86-
Inputs: The namespace and goto_functions
87-
88-
Outputs: The JSON object
89-
90-
Purpose: Output the domains for the whole program as JSON
91-
92-
\*******************************************************************/
93-
61+
/// Output the domains for the whole program as JSON
62+
/// \par parameters: The namespace and goto_functions
63+
/// \return The JSON object
9464
jsont ai_baset::output_json(
9565
const namespacet &ns,
9666
const goto_functionst &goto_functions) const
@@ -113,18 +83,9 @@ jsont ai_baset::output_json(
11383
return result;
11484
}
11585

116-
/*******************************************************************\
117-
118-
Function: ai_baset::output_json
119-
120-
Inputs: The namespace, goto_program and it's identifier
121-
122-
Outputs: The JSON object
123-
124-
Purpose: Output the domains for a single function as JSON
125-
126-
\*******************************************************************/
127-
86+
/// Output the domains for a single function as JSON
87+
/// \par parameters: The namespace, goto_program and it's identifier
88+
/// \return The JSON object
12889
jsont ai_baset::output_json(
12990
const namespacet &ns,
13091
const goto_programt &goto_program,
@@ -152,18 +113,9 @@ jsont ai_baset::output_json(
152113
return contents;
153114
}
154115

155-
/*******************************************************************\
156-
157-
Function: ai_baset::output_xml
158-
159-
Inputs: The namespace and goto_functions
160-
161-
Outputs: The XML object
162-
163-
Purpose: Output the domains for the whole program as XML
164-
165-
\*******************************************************************/
166-
116+
/// Output the domains for the whole program as XML
117+
/// \par parameters: The namespace and goto_functions
118+
/// \return The XML object
167119
xmlt ai_baset::output_xml(
168120
const namespacet &ns,
169121
const goto_functionst &goto_functions) const
@@ -189,18 +141,9 @@ xmlt ai_baset::output_xml(
189141
return program;
190142
}
191143

192-
/*******************************************************************\
193-
194-
Function: ai_baset::output_xml
195-
196-
Inputs: The namespace, goto_program and it's identifier
197-
198-
Outputs: The XML object
199-
200-
Purpose: Output the domains for a single function as XML
201-
202-
\*******************************************************************/
203-
144+
/// Output the domains for a single function as XML
145+
/// \par parameters: The namespace, goto_program and it's identifier
146+
/// \return The XML object
204147
xmlt ai_baset::output_xml(
205148
const namespacet &ns,
206149
const goto_programt &goto_program,
@@ -231,18 +174,6 @@ xmlt ai_baset::output_xml(
231174
return function_body;
232175
}
233176

234-
/*******************************************************************\
235-
236-
Function: ai_baset::entry_state
237-
238-
Inputs:
239-
240-
Outputs:
241-
242-
Purpose:
243-
244-
\*******************************************************************/
245-
246177
void ai_baset::entry_state(const goto_functionst &goto_functions)
247178
{
248179
// find the 'entry function'
@@ -254,53 +185,17 @@ void ai_baset::entry_state(const goto_functionst &goto_functions)
254185
entry_state(f_it->second.body);
255186
}
256187

257-
/*******************************************************************\
258-
259-
Function: ai_baset::entry_state
260-
261-
Inputs:
262-
263-
Outputs:
264-
265-
Purpose:
266-
267-
\*******************************************************************/
268-
269188
void ai_baset::entry_state(const goto_programt &goto_program)
270189
{
271190
// The first instruction of 'goto_program' is the entry point
272191
get_state(goto_program.instructions.begin()).make_entry();
273192
}
274193

275-
/*******************************************************************\
276-
277-
Function: ai_baset::initialize
278-
279-
Inputs:
280-
281-
Outputs:
282-
283-
Purpose:
284-
285-
\*******************************************************************/
286-
287194
void ai_baset::initialize(const goto_functionst::goto_functiont &goto_function)
288195
{
289196
initialize(goto_function.body);
290197
}
291198

292-
/*******************************************************************\
293-
294-
Function: ai_baset::initialize
295-
296-
Inputs:
297-
298-
Outputs:
299-
300-
Purpose:
301-
302-
\*******************************************************************/
303-
304199
void ai_baset::initialize(const goto_programt &goto_program)
305200
{
306201
// we mark everything as unreachable as starting point
@@ -309,36 +204,12 @@ void ai_baset::initialize(const goto_programt &goto_program)
309204
get_state(i_it).make_bottom();
310205
}
311206

312-
/*******************************************************************\
313-
314-
Function: ai_baset::initialize
315-
316-
Inputs:
317-
318-
Outputs:
319-
320-
Purpose:
321-
322-
\*******************************************************************/
323-
324207
void ai_baset::initialize(const goto_functionst &goto_functions)
325208
{
326209
forall_goto_functions(it, goto_functions)
327210
initialize(it->second);
328211
}
329212

330-
/*******************************************************************\
331-
332-
Function: ai_baset::get_next
333-
334-
Inputs:
335-
336-
Outputs:
337-
338-
Purpose:
339-
340-
\*******************************************************************/
341-
342213
ai_baset::locationt ai_baset::get_next(
343214
working_sett &working_set)
344215
{
@@ -351,18 +222,6 @@ ai_baset::locationt ai_baset::get_next(
351222
return l;
352223
}
353224

354-
/*******************************************************************\
355-
356-
Function: ai_baset::fixedpoint
357-
358-
Inputs:
359-
360-
Outputs:
361-
362-
Purpose:
363-
364-
\*******************************************************************/
365-
366225
bool ai_baset::fixedpoint(
367226
const goto_programt &goto_program,
368227
const goto_functionst &goto_functions,
@@ -389,18 +248,6 @@ bool ai_baset::fixedpoint(
389248
return new_data;
390249
}
391250

392-
/*******************************************************************\
393-
394-
Function: ai_baset::visit
395-
396-
Inputs:
397-
398-
Outputs:
399-
400-
Purpose:
401-
402-
\*******************************************************************/
403-
404251
bool ai_baset::visit(
405252
locationt l,
406253
working_sett &working_set,
@@ -459,18 +306,6 @@ bool ai_baset::visit(
459306
return new_data;
460307
}
461308

462-
/*******************************************************************\
463-
464-
Function: ai_baset::do_function_call
465-
466-
Inputs:
467-
468-
Outputs:
469-
470-
Purpose:
471-
472-
\*******************************************************************/
473-
474309
bool ai_baset::do_function_call(
475310
locationt l_call, locationt l_return,
476311
const goto_functionst &goto_functions,
@@ -534,18 +369,6 @@ bool ai_baset::do_function_call(
534369
}
535370
}
536371

537-
/*******************************************************************\
538-
539-
Function: ai_baset::do_function_call_rec
540-
541-
Inputs:
542-
543-
Outputs:
544-
545-
Purpose:
546-
547-
\*******************************************************************/
548-
549372
bool ai_baset::do_function_call_rec(
550373
locationt l_call, locationt l_return,
551374
const exprt &function,
@@ -630,18 +453,6 @@ bool ai_baset::do_function_call_rec(
630453
return new_data;
631454
}
632455

633-
/*******************************************************************\
634-
635-
Function: ai_baset::sequential_fixedpoint
636-
637-
Inputs:
638-
639-
Outputs:
640-
641-
Purpose:
642-
643-
\*******************************************************************/
644-
645456
void ai_baset::sequential_fixedpoint(
646457
const goto_functionst &goto_functions,
647458
const namespacet &ns)
@@ -653,18 +464,6 @@ void ai_baset::sequential_fixedpoint(
653464
fixedpoint(f_it->second.body, goto_functions, ns);
654465
}
655466

656-
/*******************************************************************\
657-
658-
Function: ai_baset::concurrent_fixedpoint
659-
660-
Inputs:
661-
662-
Outputs:
663-
664-
Purpose:
665-
666-
\*******************************************************************/
667-
668467
void ai_baset::concurrent_fixedpoint(
669468
const goto_functionst &goto_functions,
670469
const namespacet &ns)

‎src/analyses/ai.h

+3
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
/// \file
10+
/// Abstract Interpretation
11+
912
#ifndef CPROVER_ANALYSES_AI_H
1013
#define CPROVER_ANALYSES_AI_H
1114

0 commit comments

Comments
 (0)