Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
f64db051
Commit
f64db051
authored
Dec 03, 2019
by
Julien Signoles
Browse files
[e-acsl:archi] better error message
parent
e76a0b77
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/src/libraries/functions.ml
View file @
f64db051
...
@@ -181,7 +181,7 @@ module Libc = struct
...
@@ -181,7 +181,7 @@ module Libc = struct
|
FLongDouble
->
"E"
(* [long double] *)
|
FLongDouble
->
"E"
(* [long double] *)
in
in
(* get a character representing a pointer type *)
(* get a character representing a pointer type *)
let
get_pkind_str
ty
=
match
ty
with
let
get_pkind_str
a
ty
=
match
ty
with
|
TInt
(
IChar
,_
)
|
TInt
(
ISChar
,_
)
->
"s"
(* [char*] *)
|
TInt
(
IChar
,_
)
|
TInt
(
ISChar
,_
)
->
"s"
(* [char*] *)
|
TInt
(
IUChar
,_
)
->
"S"
(* [unsigned char*] *)
|
TInt
(
IUChar
,_
)
->
"S"
(* [unsigned char*] *)
|
TInt
(
IShort
,_
)
->
"q"
(* [short*] *)
|
TInt
(
IShort
,_
)
->
"q"
(* [short*] *)
...
@@ -194,8 +194,9 @@ module Libc = struct
...
@@ -194,8 +194,9 @@ module Libc = struct
|
TInt
(
IULongLong
,_
)
->
"W"
(* [unsigned long int*] *)
|
TInt
(
IULongLong
,_
)
->
"W"
(* [unsigned long int*] *)
|
TVoid
_
->
"p"
(* [void*] *)
|
TVoid
_
->
"p"
(* [void*] *)
|
_
->
|
_
->
Options
.
fatal
"
U
nexpected argument type in printf: %a
@."
Options
.
fatal
"
u
nexpected argument type in printf:
type %a of arg
%a@."
Printer
.
pp_typ
ty
Printer
.
pp_typ
ty
Printer
.
pp_exp
a
in
in
let
exps
=
drop
(
printf_fmt_position
fn
)
args
in
let
exps
=
drop
(
printf_fmt_position
fn
)
args
in
let
param_str
=
let
param_str
=
...
@@ -203,7 +204,7 @@ module Libc = struct
...
@@ -203,7 +204,7 @@ module Libc = struct
(
fun
exp
acc
->
match
Cil
.
unrollType
(
Cil
.
typeOf
exp
)
with
(
fun
exp
acc
->
match
Cil
.
unrollType
(
Cil
.
typeOf
exp
)
with
|
TInt
(
k
,
_
)
->
get_ikind_str
k
^
acc
|
TInt
(
k
,
_
)
->
get_ikind_str
k
^
acc
|
TFloat
(
k
,
_
)
->
get_fkind_str
k
^
acc
|
TFloat
(
k
,
_
)
->
get_fkind_str
k
^
acc
|
TPtr
(
ty
,
_
)
->
get_pkind_str
(
Cil
.
unrollType
ty
)
^
acc
|
TPtr
(
ty
,
_
)
->
get_pkind_str
exp
(
Cil
.
unrollType
ty
)
^
acc
|
TVoid
_
|
TArray
_
|
TFun
_
|
TNamed
_
|
TComp
_
|
TEnum
_
|
TVoid
_
|
TArray
_
|
TFun
_
|
TNamed
_
|
TComp
_
|
TEnum
_
|
TBuiltin_va_list
_
->
assert
false
)
|
TBuiltin_va_list
_
->
assert
false
)
exps
exps
...
@@ -244,3 +245,9 @@ let instrument kf =
...
@@ -244,3 +245,9 @@ let instrument kf =
Options
.
Instrument
.
mem
gen_kf
Options
.
Instrument
.
mem
gen_kf
with
Not_found
->
with
Not_found
->
false
))
false
))
(*
Local Variables:
compile-command: "make -C ../../../../.."
End:
*)
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