Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
9fef4530
Commit
9fef4530
authored
4 years ago
by
Basile Desloges
Browse files
Options
Downloads
Patches
Plain Diff
[variadic] Print original functions in output
parent
41b68f17
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/variadic/register.ml
+38
-1
38 additions, 1 deletion
src/plugins/variadic/register.ml
with
38 additions
and
1 deletion
src/plugins/variadic/register.ml
+
38
−
1
View file @
9fef4530
...
@@ -20,8 +20,43 @@
...
@@ -20,8 +20,43 @@
(* *)
(* *)
(**************************************************************************)
(**************************************************************************)
open
Cil_types
let
category
=
File
.
register_code_transformation_category
"variadic"
let
category
=
File
.
register_code_transformation_category
"variadic"
(* Variadic will create prototype and specifications for some variadic
functions. Since only prototypes are created, the resulting source code isn't
compilable. This printer will print the original functions, with the replaced
prototypes in comments beside the instruction. *)
let
change_printer
=
let
first
=
ref
true
in
fun
()
->
if
!
first
then
begin
first
:=
false
;
let
module
Printer_class
(
X
:
Printer
.
PrinterClass
)
=
struct
class
printer
=
object
inherit
X
.
printer
as
super
method
!
instr
fmt
i
=
match
i
with
(* If the instruction calls a function that have been replaced,
then build an instruction with the old function. *)
|
Call
(
res
,
({
enode
=
Lval
(
Var
vi
,
o
)
}
as
fct
)
,
args
,
loc
)
when
Replacements
.
mem
vi
->
let
old_vi
=
Replacements
.
find
vi
in
let
old_vi
=
{
vi
with
vname
=
old_vi
.
vname
}
in
let
old_instr
=
Call
(
res
,
{
fct
with
enode
=
Lval
(
Var
old_vi
,
o
)
}
,
args
,
loc
)
in
Format
.
fprintf
fmt
"%a /* %s */"
super
#
instr
old_instr
vi
.
vname
(* Otherwise keep the instruction. *)
|
_
->
super
#
instr
fmt
i
end
end
in
Printer
.
update_printer
(
module
Printer_class
:
Printer
.
PrinterExtension
)
end
let
()
=
let
()
=
Cmdline
.
run_after_extended_stage
Cmdline
.
run_after_extended_stage
begin
fun
()
->
begin
fun
()
->
...
@@ -32,8 +67,10 @@ let () =
...
@@ -32,8 +67,10 @@ let () =
Cmdline
.
run_after_configuring_stage
Cmdline
.
run_after_configuring_stage
begin
fun
()
->
begin
fun
()
->
let
translate
file
=
let
translate
file
=
if
Options
.
Enabled
.
get
()
then
if
Options
.
Enabled
.
get
()
then
begin
change_printer
()
;
Translate
.
translate_variadics
file
Translate
.
translate_variadics
file
end
in
in
File
.
add_code_transformation_before_cleanup
category
translate
File
.
add_code_transformation_before_cleanup
category
translate
end
end
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment