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
Deploy
Releases
Container Registry
Model registry
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
pub
frama-c
Commits
5d8fa139
Commit
5d8fa139
authored
4 years ago
by
Loïc Correnson
Browse files
Options
Downloads
Patches
Plain Diff
[server] kernel-main
parent
e5a13d37
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
src/plugins/server/Makefile.in
+5
-5
5 additions, 5 deletions
src/plugins/server/Makefile.in
src/plugins/server/kernel_main.ml
+40
-42
40 additions, 42 deletions
src/plugins/server/kernel_main.ml
src/plugins/server/states.ml
+1
-3
1 addition, 3 deletions
src/plugins/server/states.ml
with
46 additions
and
50 deletions
src/plugins/server/Makefile.in
+
5
−
5
View file @
5d8fa139
...
...
@@ -45,9 +45,9 @@ PLUGIN_CMO:= \
main request states
\
server_batch
\
kernel_main
\
kernel_project
\
kernel_ast
\
kernel_properties
#
kernel_project
\
#
kernel_ast
\
#
kernel_properties
PLUGIN_DISTRIBUTED
:=
$(
PLUGIN_ENABLE
)
PLUGIN_DISTRIB_EXTERNAL
:=
Makefile.in configure.ac configure
...
...
@@ -84,8 +84,8 @@ SERVER_API= \
package.mli server_doc.mli
\
syntax.mli data.mli request.mli states.mli
\
kernel_main.mli
\
kernel_ast.mli
\
kernel_properties.mli
#
kernel_ast.mli
\
#
kernel_properties.mli
define
Capitalize
$(
shell
printf
"%s%s"
\
...
...
This diff is collapsed.
Click to expand it.
src/plugins/server/kernel_main.ml
+
40
−
42
View file @
5d8fa139
...
...
@@ -21,34 +21,34 @@
(**************************************************************************)
open
Data
module
Sy
=
Syntax
module
Md
=
Markdown
module
Pkg
=
Package
module
Senv
=
Server_parameters
(* -------------------------------------------------------------------------- *)
(* --- Frama-C Kernel Services --- *)
(* -------------------------------------------------------------------------- *)
let
page
=
Server_doc
.
page
`Kernel
~
title
:
"Kernel Services"
~
file
name
:
"kernel
.md
"
()
let
pa
cka
ge
=
Pkg
.
package
~
title
:
"Kernel Services"
~
name
:
"kernel"
()
(* -------------------------------------------------------------------------- *)
(* --- Config --- *)
(* -------------------------------------------------------------------------- *)
let
()
=
let
get_config
=
Request
.
signature
~
page
~
kind
:
`GET
~
name
:
"kernel.getConfig"
~
descr
:
(
Md
.
plain
"Frama-C Kernel configuration"
)
~
input
:
(
module
Junit
)
()
in
let
signature
=
Request
.
signature
~
input
:
(
module
Junit
)
()
in
let
result
name
descr
=
Request
.
result
get_config
~
name
~
descr
:
(
Md
.
plain
descr
)
(
module
Jstring
)
in
Request
.
result
signature
~
name
~
descr
:
(
Md
.
plain
descr
)
(
module
Jstring
)
in
let
set_version
=
result
"version"
"Frama-C version"
in
let
set_datadir
=
result
"datadir"
"Shared directory (FRAMAC_SHARE)"
in
let
set_libdir
=
result
"libdir"
"Lib directory (FRAMAC_LIB)"
in
let
set_pluginpath
=
Request
.
result
get_config
let
set_pluginpath
=
Request
.
result
signature
~
name
:
"pluginpath"
~
descr
:
(
Md
.
plain
"Plugin directories (FRAMAC_PLUGIN)"
)
(
module
Jstring
.
Jlist
)
in
Request
.
register_sig
get_config
Request
.
register_sig
~
package
~
kind
:
`GET
~
name
:
"getConfig"
~
descr
:
(
Md
.
plain
"Frama-C Kernel configuration"
)
signature
begin
fun
rq
()
->
set_version
rq
Fc_config
.
version
;
set_datadir
rq
Fc_config
.
datadir
;
...
...
@@ -61,18 +61,13 @@ let () =
(* -------------------------------------------------------------------------- *)
let
()
=
let
signature
=
Request
.
signature
~
page
~
kind
:
`SET
~
name
:
"kernel.load"
~
descr
:
(
Md
.
plain
"Load a save file"
)
~
input
:
(
module
Jstring
)
~
output
:
(
module
Jstring
.
Joption
)
()
in
let
load
_rq
file
=
try
Project
.
load_all
(
Filepath
.
Normalized
.
of_string
file
);
None
with
Project
.
IOError
err
->
Some
err
in
Request
.
register_sig
signature
load
Request
.
register
~
package
~
kind
:
`SET
~
name
:
"load"
~
descr
:
(
Md
.
plain
"Load a save file. Returns an error, if not successfull."
)
~
input
:
(
module
Jstring
)
~
output
:
(
module
Jstring
.
Joption
)
(
fun
file
->
try
Project
.
load_all
(
Filepath
.
Normalized
.
of_string
file
);
None
with
Project
.
IOError
err
->
Some
err
)
(* -------------------------------------------------------------------------- *)
(* --- File Positions --- *)
...
...
@@ -82,15 +77,14 @@ module LogSource = Collection
(
struct
type
t
=
Filepath
.
position
let
synopsis
=
Sy
.
record
[
"dir"
,
Sy
.
string
;
"base"
,
Sy
.
string
;
"file"
,
Sy
.
string
;
"line"
,
Sy
.
int
]
let
syntax
=
Sy
.
publish
~
page
:
Data
.
page
~
name
:
"source"
~
synopsis
let
jtype
=
Pkg
.
datatype
~
package
~
name
:
"source"
~
descr
:
(
Md
.
plain
"Source file positions."
)
~
details
:
Md
.([
Block
[
Text
(
plain
"The file path is normalized, \
and the line number starts at one."
)]])
()
(
Jrecord
[
"dir"
,
Jstring
;
"base"
,
Jstring
;
"file"
,
Jstring
;
"line"
,
Jnumber
;
])
let
to_json
p
=
let
path
=
Filepath
.(
Normalized
.
to_pretty_string
p
.
pos_path
)
in
...
...
@@ -123,13 +117,10 @@ module LogSource = Collection
module
LogKind
=
Collection
(
struct
let
kinds
=
Enum
.
dictionary
~
page
~
name
:
"logkind"
~
title
:
"Log Kind"
~
descr
:
(
Md
.
plain
"Frama-C message category."
)
()
let
kinds
=
Enum
.
dictionary
()
let
t_kind
value
name
descr
=
Enum
.
tag
kinds
~
name
~
descr
:
(
Md
.
plain
descr
)
~
value
()
Enum
.
tag
~
name
~
descr
:
(
Md
.
plain
descr
)
~
value
kinds
let
t_error
=
t_kind
Log
.
Error
"ERROR"
"User Error"
let
t_warning
=
t_kind
Log
.
Warning
"WARNING"
"User Warning"
...
...
@@ -146,8 +137,10 @@ module LogKind = Collection
|
Log
.
Failure
->
t_failure
|
Log
.
Debug
->
t_debug
let
data
=
Enum
.
publish
kinds
~
tag
()
let
()
=
Request
.
dictionary
kinds
let
data
=
Request
.
dictionary
~
package
~
name
:
"logkind"
~
descr
:
(
Md
.
plain
"Log messages categories."
)
kinds
include
(
val
data
:
S
with
type
t
=
Log
.
kind
)
end
)
...
...
@@ -161,8 +154,7 @@ module LogEvent = Collection
type
rlog
let
jlog
:
rlog
Record
.
signature
=
Record
.
signature
~
page
~
name
:
"log"
~
descr
:
(
Md
.
plain
"Message event record."
)
()
let
jlog
:
rlog
Record
.
signature
=
Record
.
signature
()
let
kind
=
Record
.
field
jlog
~
name
:
"kind"
~
descr
:
(
Md
.
plain
"Message kind"
)
(
module
LogKind
)
...
...
@@ -175,10 +167,14 @@ module LogEvent = Collection
let
source
=
Record
.
option
jlog
~
name
:
"source"
~
descr
:
(
Md
.
plain
"Source file position"
)
(
module
LogSource
)
module
R
=
(
val
(
Record
.
publish
jlog
)
:
Record
.
S
with
type
r
=
rlog
)
let
data
=
Record
.
publish
~
package
~
name
:
"log"
~
descr
:
(
Md
.
plain
"Message event record."
)
jlog
module
R
:
Record
.
S
with
type
r
=
rlog
=
(
val
data
)
type
t
=
Log
.
event
let
syntax
=
R
.
syntax
let
jtype
=
R
.
jtype
let
to_json
evt
=
R
.
default
|>
...
...
@@ -236,14 +232,16 @@ let () =
(* --- Log Requests --- *)
(* -------------------------------------------------------------------------- *)
(* TODO:LC: shall have an array here. *)
let
()
=
Request
.
register
~
page
~
kind
:
`SET
~
name
:
"
kernel.
setLogs"
~
pa
cka
ge
~
kind
:
`SET
~
name
:
"setLogs"
~
descr
:
(
Md
.
plain
"Turn logs monitoring on/off"
)
~
input
:
(
module
Jbool
)
~
output
:
(
module
Junit
)
set_monitoring
let
()
=
Request
.
register
~
page
~
kind
:
`GET
~
name
:
"
kernel.
getLogs"
~
pa
cka
ge
~
kind
:
`GET
~
name
:
"getLogs"
~
descr
:
(
Md
.
plain
"Flush the last emitted logs since last call (max 100)"
)
~
input
:
(
module
Junit
)
~
output
:
(
module
LogEvent
.
Jlist
)
begin
fun
()
->
...
...
This diff is collapsed.
Click to expand it.
src/plugins/server/states.ml
+
1
−
3
View file @
5d8fa139
...
...
@@ -71,7 +71,6 @@ let register_state (type a) ~package ~name ~descr
let
open
Markdown
in
let
module
D
=
(
val
data
)
in
let
href
=
link
~
name
()
in
let
descr
=
Markdown
.
par
descr
in
let
()
=
Package
.
declare
~
package
~
name
~
descr
D_state
in
let
signal
=
Request
.
signal
...
...
@@ -268,7 +267,6 @@ let register_array ~package ~name ~descr ~key
model
=
let
open
Markdown
in
let
href
=
link
~
name
()
in
let
descr
=
Markdown
.
par
descr
in
let
columns
=
List
.
rev
!
model
in
let
fields
=
Package
.{
fd_name
=
"key"
;
...
...
@@ -281,7 +279,7 @@ let register_array ~package ~name ~descr ~key
~
descr
:
(
plain
"Signal for array"
@
href
)
in
let
row
=
Package
.
declare_id
~
package
~
name
:
(
name
^
"Row"
)
~
descr
:
(
par
(
plain
"Data rows for array"
@
href
)
)
~
descr
:
(
plain
"Data rows for array"
@
href
)
(
D_record
fields
)
in
let
getter
=
List
.
map
Package
.(
fun
(
fd
,
to_js
)
->
fd
.
fd_name
,
to_js
)
columns
in
...
...
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