Skip to content
Snippets Groups Projects
Commit 44196c3c authored by Michele Alberti's avatar Michele Alberti
Browse files

[Eva] Again on rebasing on new server API.

parent 602f9624
No related branches found
No related tags found
No related merge requests found
...@@ -25,11 +25,9 @@ open Data ...@@ -25,11 +25,9 @@ open Data
open Cil_types open Cil_types
module Md = Markdown module Md = Markdown
let chapter = `Plugin "Eva"
let package = let package =
Package.package Package.package
~plugin:"Eva" ~plugin:"eva"
~name:"eva" ~name:"eva"
~title:"Eva Values" ~title:"Eva Values"
~readme:"eva.md" ~readme:"eva.md"
...@@ -70,11 +68,10 @@ let get_after_value = ...@@ -70,11 +68,10 @@ let get_after_value =
(function Unchanged -> "unchanged" | Reduced eval -> get_value eval) (function Unchanged -> "unchanged" | Reduced eval -> get_value eval)
module CallStackId = module CallStackId =
Data.Index (Value_types.Callstack.Map) Data.Index
(Value_types.Callstack.Map)
(struct (struct
let page = page
let name = "eva-callstack-id" let name = "eva-callstack-id"
let descr = Md.plain "CallStack"
end) end)
(* This pretty-printer drops the toplevel kf, which is always the function (* This pretty-printer drops the toplevel kf, which is always the function
...@@ -129,12 +126,14 @@ module CallStack = struct ...@@ -129,12 +126,14 @@ module CallStack = struct
(val (val
(Record.publish (Record.publish
~package ~package
~name:"eva-callstack" ~name:"evaCallstack"
~descr:(Md.plain "CallStack") ~descr:(Md.plain "CallStack")
record) : Record.S with type r = record) record) : Record.S with type r = record)
type t = Value_types.callstack option type t = Value_types.callstack option
let jtype = R.jtype
let pp_callstack ~short = function let pp_callstack ~short = function
| None -> "all" | None -> "all"
| Some callstack -> | Some callstack ->
...@@ -205,7 +204,7 @@ let array = ...@@ -205,7 +204,7 @@ let array =
in in
States.register_array States.register_array
~package ~package
~name:"eva.values" ~name:"evaValues"
~descr:(Md.plain "Abstract values inferred by the Eva analysis") ~descr:(Md.plain "Abstract values inferred by the Eva analysis")
~key:(fun (cs, _) -> CallStack.key cs) ~key:(fun (cs, _) -> CallStack.key cs)
~iter ~iter
...@@ -351,7 +350,7 @@ let () = ...@@ -351,7 +350,7 @@ let () =
Server.Request.register Server.Request.register
~package ~package
~kind:`GET ~kind:`GET
~name:"eva.values.compute" ~name:"getEvaValues"
~descr:(Md.plain "Get the abstract values computed for an expression or lvalue") ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue")
~input:(module Kernel_ast.Marker) ~input:(module Kernel_ast.Marker)
~output:(module Junit) ~output:(module Junit)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment