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
Snippets
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Terraform modules
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
Charles Southerland
frama-c
Commits
4475d3ee
Commit
4475d3ee
authored
5 years ago
by
Julien Signoles
Browse files
Options
Downloads
Patches
Plain Diff
[translate] rename formal parameter 'sty' to 'strnum'
parent
be2028c5
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/e-acsl/translate.ml
+6
-6
6 additions, 6 deletions
src/plugins/e-acsl/translate.ml
with
6 additions
and
6 deletions
src/plugins/e-acsl/translate.ml
+
6
−
6
View file @
4475d3ee
...
@@ -69,7 +69,7 @@ type strnum =
...
@@ -69,7 +69,7 @@ type strnum =
|
C_number
(* integers AND floats) included *)
|
C_number
(* integers AND floats) included *)
(* convert [e] in a way that it is compatible with the given typing context. *)
(* convert [e] in a way that it is compatible with the given typing context. *)
let
add_cast
~
loc
?
name
env
ctx
st
y
t_opt
e
=
let
add_cast
~
loc
?
name
env
ctx
st
rnum
t_opt
e
=
let
mk_mpz
e
=
let
mk_mpz
e
=
let
_
,
e
,
env
=
Env
.
new_var
let
_
,
e
,
env
=
Env
.
new_var
~
loc
~
loc
...
@@ -81,7 +81,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
...
@@ -81,7 +81,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
in
in
e
,
env
e
,
env
in
in
let
e
,
env
=
match
st
y
with
let
e
,
env
=
match
st
rnum
with
|
Str_Z
->
mk_mpz
e
|
Str_Z
->
mk_mpz
e
|
Str_R
->
Real
.
mk_real
~
loc
?
name
e
env
t_opt
|
Str_R
->
Real
.
mk_real
~
loc
?
name
e
env
t_opt
|
C_number
->
e
,
env
|
C_number
->
e
,
env
...
@@ -103,9 +103,9 @@ let add_cast ~loc ?name env ctx sty t_opt e =
...
@@ -103,9 +103,9 @@ let add_cast ~loc ?name env ctx sty t_opt e =
also possible to get a non integralType (or Gmp.z_t) with a non-one in
also possible to get a non integralType (or Gmp.z_t) with a non-one in
the case of \null *)
the case of \null *)
let
e
=
let
e
=
if
Cil
.
isIntegralType
ty
||
st
y
=
Str_Z
then
if
Cil
.
isIntegralType
ty
||
st
rnum
=
Str_Z
then
e
e
else
if
not
(
Cil
.
isIntegralType
ty
)
&&
st
y
=
C_number
then
else
if
not
(
Cil
.
isIntegralType
ty
)
&&
st
rnum
=
C_number
then
Cil
.
mkCast
e
Cil
.
longType
(* \null *)
Cil
.
mkCast
e
Cil
.
longType
(* \null *)
else
(* Remaining: not (Cil.isIntegralType ty) && sty = StrR *)
else
(* Remaining: not (Cil.isIntegralType ty) && sty = StrR *)
assert
false
assert
false
...
@@ -116,7 +116,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
...
@@ -116,7 +116,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
else
Real
.
mk_real
~
loc
?
name
e
env
t_opt
else
Real
.
mk_real
~
loc
?
name
e
env
t_opt
else
else
(* handle a C-integer context *)
(* handle a C-integer context *)
if
Gmp
.
Z
.
is_t
ty
||
st
y
=
Str_Z
then
if
Gmp
.
Z
.
is_t
ty
||
st
rnum
=
Str_Z
then
(* we get an mpz, but it fits into a C integer: convert it *)
(* we get an mpz, but it fits into a C integer: convert it *)
let
fname
,
new_ty
=
let
fname
,
new_ty
=
if
Cil
.
isSignedInteger
ctx
then
if
Cil
.
isSignedInteger
ctx
then
...
@@ -134,7 +134,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
...
@@ -134,7 +134,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
(
fun
v
_
->
[
Misc
.
mk_call
~
loc
~
result
:
(
Cil
.
var
v
)
fname
[
e
]
])
(
fun
v
_
->
[
Misc
.
mk_call
~
loc
~
result
:
(
Cil
.
var
v
)
fname
[
e
]
])
in
in
e
,
env
e
,
env
else
if
Real
.
is_t
ty
||
st
y
=
Str_R
then
else
if
Real
.
is_t
ty
||
st
rnum
=
Str_R
then
Real
.
add_cast
~
loc
?
name
e
env
ctx
Real
.
add_cast
~
loc
?
name
e
env
ctx
else
else
Cil
.
mkCastT
~
force
:
false
~
e
~
oldt
:
ty
~
newt
:
ctx
,
env
Cil
.
mkCastT
~
force
:
false
~
e
~
oldt
:
ty
~
newt
:
ctx
,
env
...
...
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