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
120
Issues
120
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
4bfbb32a
Commit
4bfbb32a
authored
Mar 25, 2019
by
Raphael Rieu-Helft
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
C extraction: use the syntax literal driver entries for number constants
parent
5e540a79
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
30 additions
and
29 deletions
+30
-29
drivers/c.drv
drivers/c.drv
+6
-6
src/mlw/cprinter.ml
src/mlw/cprinter.ml
+24
-23
No files found.
drivers/c.drv
View file @
4bfbb32a
...
...
@@ -23,7 +23,7 @@ end
module mach.int.Int32
syntax type int32 "int32_t"
syntax literal int32 "%
d
"
syntax literal int32 "%
c
"
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
...
...
@@ -49,7 +49,7 @@ end
module mach.int.UInt32
syntax literal uint32 "
0x%8x
U"
syntax literal uint32 "
%c
U"
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
...
...
@@ -181,7 +181,7 @@ struct __lsld32_result
struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
"
syntax literal uint32 "
0x%8x
U"
syntax literal uint32 "
%c
U"
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
...
...
@@ -223,7 +223,7 @@ end
module mach.int.Int64
syntax type int64 "int64_t"
syntax literal int64 "
%dL
"
syntax literal int64 "
INT64_C(%c)
"
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
...
...
@@ -250,7 +250,7 @@ end
module mach.int.UInt64
syntax literal uint64 "
0x%16xUL
"
syntax literal uint64 "
UINT64_C(%c)
"
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
...
...
@@ -505,7 +505,7 @@ static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
return result;
}
"
syntax literal uint64 "
0x%16xUL
"
syntax literal uint64 "
UINT64_C(%c)
"
syntax val uint64_max "0xffffffffffffffffUL" prec 0
...
...
src/mlw/cprinter.ml
View file @
4bfbb32a
...
...
@@ -925,29 +925,30 @@ module MLToC = struct
([]
,
expr_or_return
env
e
)
|
Mltree
.
Econst
ic
->
let
open
Number
in
let
print
fmt
ic
=
let
n
=
ic
.
il_int
in
let
n
=
if
BigInt
.
lt
n
BigInt
.
zero
then
BigInt
.
to_string
n
if
BigInt
.
lt
n
BigInt
.
zero
then
Format
.
fprintf
fmt
"-%a"
(
print_in_base
10
None
)
(
BigInt
.
abs
n
)
else
match
ic
.
il_kind
with
|
ILitHex
->
Format
.
asprintf
"0x%a"
(
print_in_base
16
None
)
n
|
ILitOct
->
Format
.
asprintf
"0%a"
(
print_in_base
8
None
)
n
|
_
->
BigInt
.
to_string
n
in
let
suf
=
match
e
.
e_ity
with
|
ILitHex
->
Format
.
fprintf
fmt
"0x%a"
(
print_in_base
16
None
)
n
|
ILitOct
->
Format
.
fprintf
fmt
"0%a"
(
print_in_base
8
None
)
n
|
_
->
(* default to base 10 *)
Format
.
fprintf
fmt
"%a"
(
print_in_base
10
None
)
n
in
let
s
=
match
e
.
e_ity
with
|
I
i
->
begin
match
(
ty_of_ity
i
)
.
ty_node
with
|
Tyapp
({
ts_def
=
Range
{
ir_lower
=
l
;
ir_upper
=
h
}}
,_
)
->
let
open
BigInt
in
let
unsigned
=
eq
l
zero
in
if
(
le
min32
l
)
&&
(
le
h
max32
)
then
""
else
if
unsigned
&&
(
le
h
maxu32
)
then
"u"
else
if
(
le
min64
l
)
&&
(
le
h
max64
)
then
"l"
else
if
unsigned
&&
(
le
h
maxu64
)
then
"ul"
else
raise
(
Unsupported
"unknown number format"
)
|
_
->
raise
(
Unsupported
"non-range integer constant"
)
end
let
ts
=
match
(
ty_of_ity
i
)
with
|
{
ty_node
=
Tyapp
(
ts
,
[]
)
}
->
ts
|
_
->
assert
false
in
begin
match
query_syntax
info
.
literal
ts
.
ts_name
with
|
Some
st
->
Format
.
asprintf
"%a"
(
syntax_range_literal
~
cb
:
(
Some
print
)
st
)
ic
|
_
->
let
s
=
ts
.
ts_name
.
id_string
in
raise
(
Unsupported
(
"unspecified number format for type "
^
s
))
end
|
_
->
assert
false
in
let
e
=
C
.(
Econst
(
Cint
(
n
^
suf
)
))
in
let
e
=
C
.(
Econst
(
Cint
s
))
in
([]
,
expr_or_return
env
e
)
|
Eapp
(
rs
,
el
)
when
is_struct_constructor
info
rs
...
...
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