Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
844f6050
Commit
844f6050
authored
Dec 13, 2019
by
Julien Signoles
Browse files
[e-acsl] lint
parent
5492c6c5
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/src/code_generator/gmp.ml
View file @
844f6050
...
...
@@ -90,22 +90,22 @@ let init_set ~loc lv ev e =
with
|
Longlong
IULongLong
->
(
match
e
.
enode
with
|
Lval
elv
->
assert
(
Gmp_types
.
Z
.
is_t
(
Cil
.
typeOf
ev
));
let
call
=
Constructor
.
mk_lib_call
~
loc
"__gmpz_import"
[
ev
;
Cil
.
one
~
loc
;
Cil
.
one
~
loc
;
Cil
.
sizeOf
~
loc
(
TInt
(
IULongLong
,
[]
));
Cil
.
zero
~
loc
;
Cil
.
zero
~
loc
;
Cil
.
mkAddrOf
~
loc
elv
]
in
Cil
.
mkStmt
~
valid_sid
:
true
(
Block
(
Cil
.
mkBlock
[
init
~
loc
ev
;
call
]))
|
_
->
Error
.
not_yet
"unsigned long long expression requiring GMP"
)
|
Lval
elv
->
assert
(
Gmp_types
.
Z
.
is_t
(
Cil
.
typeOf
ev
));
let
call
=
Constructor
.
mk_lib_call
~
loc
"__gmpz_import"
[
ev
;
Cil
.
one
~
loc
;
Cil
.
one
~
loc
;
Cil
.
sizeOf
~
loc
(
TInt
(
IULongLong
,
[]
));
Cil
.
zero
~
loc
;
Cil
.
zero
~
loc
;
Cil
.
mkAddrOf
~
loc
elv
]
in
Cil
.
mkStmt
~
valid_sid
:
true
(
Block
(
Cil
.
mkBlock
[
init
~
loc
ev
;
call
]))
|
_
->
Error
.
not_yet
"unsigned long long expression requiring GMP"
)
|
Longlong
ILongLong
->
Error
.
not_yet
"long long requiring GMP"
...
...
src/plugins/e-acsl/src/libraries/misc.ml
View file @
844f6050
...
...
@@ -50,10 +50,10 @@ let is_fc_or_compiler_builtin vi =
Cil
.
is_builtin
vi
||
(
let
prefix_length
=
10
(* number of characters in "__builtin_" *)
in
String
.
length
vi
.
vname
>
prefix_length
&&
let
prefix
=
String
.
sub
vi
.
vname
0
prefix_length
in
Datatype
.
String
.
equal
prefix
"__builtin_"
)
String
.
length
vi
.
vname
>
prefix_length
&&
let
prefix
=
String
.
sub
vi
.
vname
0
prefix_length
in
Datatype
.
String
.
equal
prefix
"__builtin_"
)
(* ************************************************************************** *)
(** {2 Builders} *)
...
...
src/plugins/e-acsl/src/project_initializer/keep_status.ml
View file @
844f6050
...
...
@@ -68,7 +68,7 @@ let pretty_kind fmt k =
(* information attached to every kernel_function containing an annotation *)
type
kf_info
=
{
mutable
cpt
:
int
(* counter building the relationship between [push] and [must_translate] *)
;
(* counter building the relationship between [push] and [must_translate] *)
;
mutable
statuses
:
(
kind
*
bool
)
Datatype
.
Int
.
Map
.
t
(* map associating a property as an integer to its kind and status
([true] = proved) *)
}
...
...
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