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
c377a505
Commit
c377a505
authored
Dec 17, 2019
by
Michele Alberti
Browse files
Make frama-c typecheck, and pass the basic tests.
parent
302497ad
Changes
14
Hide whitespace changes
Inline
Side-by-side
src/kernel_services/ast_queries/file.ml
View file @
c377a505
...
...
@@ -1639,7 +1639,7 @@ let init_from_cmdline () =
let
files
=
Kernel
.
Files
.
get
()
in
if
files
=
[]
&&
not
!
Config
.
is_gui
then
Kernel
.
warning
"no input file."
;
let
files
=
List
.
map
(
fun
s
->
from_filename
s
)
files
List
.
map
(
fun
f
->
from_filename
(
Filepath
.
Normalized
.
to_pretty_string
f
)
)
files
in
try
init_from_c_files
files
;
...
...
src/kernel_services/cmdline_parameters/cmdline.ml
View file @
c377a505
...
...
@@ -726,7 +726,7 @@ let add_aliases orig ~plugin ~group stage aliases =
let
replace_option_setting
=
Plugin
.
replace_option_setting
module
On_Files
=
Hook
.
Build
(
struct
type
t
=
string
list
end
)
module
On_Files
=
Hook
.
Build
(
struct
type
t
=
Filepath
.
Normalized
.
t
list
end
)
let
use_cmdline_files
=
On_Files
.
extend
let
set_files
used_loading
l
=
...
...
@@ -746,7 +746,7 @@ let set_files used_loading l =
"ignoring source files specified on the command line \
while loading a global initial context."
else
begin
On_Files
.
apply
l
;
On_Files
.
apply
(
List
.
map
Filepath
.
Normalized
.
of_string
l
)
;
After_setting
.
apply
l
end
...
...
src/kernel_services/cmdline_parameters/cmdline.mli
View file @
c377a505
...
...
@@ -227,7 +227,7 @@ val nb_given_options: unit -> int
Should not be called before the end of the command line parsing.
@since Beryllium-20090601-beta1 *)
val
use_cmdline_files
:
(
string
list
->
unit
)
->
unit
val
use_cmdline_files
:
(
Datatype
.
Filepath
.
t
list
->
unit
)
->
unit
(** What to do with the list of files put on the command lines.
@since Beryllium-20090601-beta1 *)
...
...
src/kernel_services/cmdline_parameters/parameter_builder.ml
View file @
c377a505
...
...
@@ -1210,14 +1210,21 @@ struct
module
Filepath_list
(
X
:
sig
include
Parameter_sig
.
Input_with_arg
val
existence
:
Fc_Filepath
.
existence
val
existence
:
Fc_Filepath
.
existence
end
)
=
Make_list
(
struct
include
Datatype
.
Filepath
let
of_string
s
=
Datatype
.
Filepath
.
of_string
~
existence
:
X
.
existence
s
let
to_string
=
Fc_Filepath
.
Normalized
.
to_pretty_string
let
of_singleton_string
=
no_element_of_string
let
of_string
s
=
try
of_string
~
existence
:
X
.
existence
s
with
|
Fc_Filepath
.
No_file
->
cannot_build
(
Format
.
sprintf
"file not found: '%s'"
s
)
|
Fc_Filepath
.
File_exists
->
cannot_build
(
Format
.
sprintf
"file already exists: '%s'"
s
)
end
)
(
struct
include
X
...
...
src/kernel_services/plugin_entry_points/kernel.ml
View file @
c377a505
...
...
@@ -247,6 +247,17 @@ module String_list(X: Input_with_arg) =
include
X
end
)
module
Filepath_list
(
X
:
sig
include
Input_with_arg
val
existence
:
Filepath
.
existence
end
)
=
P
.
Filepath_list
(
struct
let
()
=
Parameter_customize
.
set_module_name
X
.
module_name
include
X
end
)
module
Kernel_function_set
(
X
:
Input_with_arg
)
=
P
.
Kernel_function_set
(
struct
...
...
@@ -1216,12 +1227,13 @@ module Files = struct
let
()
=
Parameter_customize
.
is_invisible
()
let
()
=
Parameter_customize
.
no_category
()
include
String
_list
include
Filepath
_list
(
struct
let
option_name
=
""
let
module_name
=
"Files"
let
arg_name
=
""
let
help
=
""
let
existence
=
Filepath
.
Must_exist
end
)
let
()
=
Cmdline
.
use_cmdline_files
set
...
...
src/kernel_services/plugin_entry_points/kernel.mli
View file @
c377a505
...
...
@@ -423,7 +423,7 @@ module RemoveExn: Parameter_sig.Bool
(** Behavior of option "-remove-exn" *)
(** Analyzed files *)
module
Files
:
Parameter_sig
.
String
_list
module
Files
:
Parameter_sig
.
Filepath
_list
(** List of files to analyse *)
module
Orig_name
:
Parameter_sig
.
Bool
...
...
src/plugins/aorai/aorai_register.ml
View file @
c377a505
...
...
@@ -164,7 +164,7 @@ let init_file_names () =
c_file
:=
(
match
Kernel
.
Files
.
get
()
with
|
[]
->
"dummy.i"
|
f
::
_
->
f
);
|
f
::
_
->
Filepath
.
Normalized
.
to_pretty_string
f
);
if
(
!
c_file
=
""
)
then
dispErr
": invalid C file name"
!
c_file
;
if
(
not
(
Sys
.
file_exists
!
c_file
))
then
dispErr
"not found"
!
c_file
;
...
...
@@ -258,7 +258,7 @@ let output () =
printverb
"Finished.
\n
"
;
(* Some test traces. *)
Data_for_aorai
.
debug_computed_state
()
;
if
!
generatesCFile
then
Kernel
.
Files
.
set
[
!
output_c_file
]
if
!
generatesCFile
then
Kernel
.
Files
.
set
[
Datatype
.
Filepath
.
of_string
!
output_c_file
]
let
work
()
=
let
file
=
Ast
.
get
()
in
...
...
src/plugins/e-acsl/src/main.ml
View file @
c377a505
...
...
@@ -82,7 +82,7 @@ let unmemoized_extend_ast () =
in
Project
.
on
prj
(
fun
()
->
Kernel
.
Files
.
set
[
tmpfile
];
Kernel
.
Files
.
set
[
Datatype
.
Filepath
.
of_string
tmpfile
];
extend
()
)
()
;
Some
prj
...
...
src/plugins/e-acsl/tests/print.ml
View file @
c377a505
...
...
@@ -28,9 +28,8 @@ module Printer_extension(X:Printer.PrinterClass) = struct
method
!
global
fmt
g
=
let
loc
,
_
=
Cil_datatype
.
Global
.
loc
g
in
let
file
=
loc
.
Filepath
.
pos_path
in
if
file
=
Datatype
.
Filepath
.
dummy
||
List
.
exists
(
fun
s
->
Datatype
.
Filepath
.
of_string
s
=
file
)
(
Kernel
.
Files
.
get
()
)
if
file
=
Datatype
.
Filepath
.
dummy
||
List
.
exists
(
fun
s
->
s
=
file
)
(
Kernel
.
Files
.
get
()
)
then
super
#
global
fmt
g
end
...
...
src/plugins/gui/file_manager.ml
View file @
c377a505
...
...
@@ -23,9 +23,9 @@
let
add_files
(
host_window
:
Design
.
main_window_extension_points
)
=
Gtk_helper
.
source_files_chooser
(
host_window
:>
Gtk_helper
.
source_files_chooser_host
)
(
Kernel
.
Files
.
get
()
)
(
List
.
map
Filepath
.
Normalized
.
to_pretty_string
(
Kernel
.
Files
.
get
()
)
)
(
fun
filenames
->
Kernel
.
Files
.
set
filenames
;
Kernel
.
Files
.
set
(
List
.
map
Datatype
.
Filepath
.
of_string
filenames
)
;
if
Ast
.
is_computed
()
then
Gui_parameters
.
warning
"Input files unchanged. Ignored."
else
begin
...
...
src/plugins/gui/project_manager.ml
View file @
c377a505
...
...
@@ -52,7 +52,7 @@ let new_project main_ui =
(
fun
filenames
->
let
project
=
Project
.
create
"interactive"
in
let
init
()
=
Kernel
.
Files
.
set
filenames
;
Kernel
.
Files
.
set
(
List
.
map
Datatype
.
Filepath
.
of_string
filenames
)
;
File
.
init_from_cmdline
()
in
Project
.
on
project
init
()
;
...
...
src/plugins/markdown-report/md_gen.ml
View file @
c377a505
...
...
@@ -175,6 +175,7 @@ let section_stubs env =
let
get_files
()
=
let
dir_table
=
Datatype
.
String
.
Hashtbl
.
create
17
in
let
add_entry
f
=
let
f
=
Filepath
.
Normalized
.
to_pretty_string
f
in
let
dir
=
Filename
.
dirname
f
in
let
base
=
Filename
.
basename
f
in
let
suf
=
...
...
src/plugins/markdown-report/sarif_gen.ml
View file @
c377a505
...
...
@@ -143,8 +143,11 @@ let gen_statuses () =
let
gen_files
()
=
let
add_src_file
f
=
let
key
=
Filename
.
chop_extension
(
Filename
.
basename
f
)
in
let
fileLocation
=
FileLocation
.
create
~
uri
:
(
Filepath
.
normalize
f
)
()
in
let
key
=
let
fname
=
Filepath
.
Normalized
.
to_pretty_string
f
in
Filename
.
chop_extension
(
Filename
.
basename
fname
)
in
let
fileLocation
=
FileLocation
.
create
~
uri
:
(
f
:>
string
)
()
in
let
roles
=
[
Role
.
analysisTarget
]
in
let
mimeType
=
"text/x-csrc"
in
key
,
File
.
create
~
fileLocation
~
roles
~
mimeType
()
...
...
tests/spec/Extend.ml
View file @
c377a505
...
...
@@ -127,7 +127,7 @@ let run () =
File
.
pretty_ast
~
fmt
()
;
let
prj
=
Project
.
create
"reparsing"
in
Project
.
on
prj
add_builtin
()
;
Project
.
on
prj
Kernel
.
Files
.
add
my_file
;
Project
.
on
prj
Kernel
.
Files
.
add
(
Datatype
.
Filepath
.
of_string
my_file
)
;
Kernel
.
feedback
"Reparsing file"
;
(* Avoid having a temporary name in the oracle. *)
Kernel
.
Verbose
.
set
0
;
...
...
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