Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
121
Issues
121
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
a59e4ad6
Commit
a59e4ad6
authored
Nov 02, 2016
by
Raphaël Rieu-Helft
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add C AST to the printer
parent
1c9adfcf
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
70 additions
and
0 deletions
+70
-0
src/mlw/cprinter.ml
src/mlw/cprinter.ml
+70
-0
No files found.
src/mlw/cprinter.ml
View file @
a59e4ad6
open
Ident
module
C
=
struct
type
ty
=
|
Tvoid
|
Tsyntax
of
string
(* ints, floats, doubles, chars are here *)
|
Tptr
of
ty
|
Tarray
of
ty
*
expr
|
Tstruct
of
ident
*
(
ident
*
ty
)
list
|
Tunion
of
ident
*
(
ident
*
ty
)
list
|
Tproto
of
proto
|
Tnamed
of
ident
(* alias from typedef *)
(* enum, const could be added *)
(* int x=2, *y ... *)
and
names
=
ty
*
(
ident
*
expr
)
list
(* names with a single declaration *)
and
name
=
ty
*
ident
*
expr
(* return type, parameter list. Variadic functions not handled. *)
and
proto
=
ty
*
(
ty
*
ident
)
list
and
binop
=
Band
|
Bor
|
Beq
|
Bne
|
Bassign
(* += and co. maybe to add *)
and
unop
=
Unot
|
Ustar
|
Uaddr
(* (pre|post)(incr|decr) maybe to add *)
and
expr
=
|
Enothing
|
Eunop
of
unop
*
expr
|
Ebinop
of
binop
*
expr
*
expr
|
Eternary
of
expr
*
expr
*
expr
(* c ? then : else *)
|
Ecast
of
ty
*
expr
|
Ecall
of
expr
*
expr
list
|
Econst
of
constant
|
Evar
of
string
|
Esize_expr
of
expr
|
Esize_type
of
ty
|
Eindex
of
expr
*
expr
(* Array access *)
|
Edot
of
expr
*
string
(* Field access with dot *)
|
Earrow
of
expr
*
string
(* Pointer access with arrow *)
and
constant
=
|
Cint
of
string
|
Cfloat
of
string
|
Cchar
of
string
|
Cstring
of
string
|
Ccompound
of
expr
list
type
stmt
=
|
Snop
|
Sexpr
of
expr
|
Sblock
of
body
|
Sseq
of
stmt
*
stmt
|
Sif
of
expr
*
stmt
*
stmt
|
Swhile
of
expr
*
stmt
|
Sfor
of
expr
*
expr
*
expr
*
stmt
|
Sbreak
|
Sreturn
of
expr
and
definition
=
|
Dfun
of
name
*
body
|
Ddecl
of
names
|
Dtypedef
of
ty
*
ident
|
Dstructural
of
names
(* struct, union... *)
and
body
=
definition
list
*
stmt
type
file
=
definition
list
end
let
fg
?
fname
m
=
let
n
=
m
.
Pmodule
.
mod_theory
.
Theory
.
th_name
.
Ident
.
id_string
in
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment