diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml index 492448adcb8216565f38f17365eb3a5a68382ef4..0c708c5b34cf2cfd2ec36a8347569b834d3753a7 100644 --- a/src/plugins/value/api/values_request.ml +++ b/src/plugins/value/api/values_request.ml @@ -25,11 +25,9 @@ open Data open Cil_types module Md = Markdown -let chapter = `Plugin "Eva" - let package = Package.package - ~plugin:"Eva" + ~plugin:"eva" ~name:"eva" ~title:"Eva Values" ~readme:"eva.md" @@ -70,11 +68,10 @@ let get_after_value = (function Unchanged -> "unchanged" | Reduced eval -> get_value eval) module CallStackId = - Data.Index (Value_types.Callstack.Map) + Data.Index + (Value_types.Callstack.Map) (struct - let page = page let name = "eva-callstack-id" - let descr = Md.plain "CallStack" end) (* This pretty-printer drops the toplevel kf, which is always the function @@ -129,12 +126,14 @@ module CallStack = struct (val (Record.publish ~package - ~name:"eva-callstack" + ~name:"evaCallstack" ~descr:(Md.plain "CallStack") record) : Record.S with type r = record) type t = Value_types.callstack option + let jtype = R.jtype + let pp_callstack ~short = function | None -> "all" | Some callstack -> @@ -205,7 +204,7 @@ let array = in States.register_array ~package - ~name:"eva.values" + ~name:"evaValues" ~descr:(Md.plain "Abstract values inferred by the Eva analysis") ~key:(fun (cs, _) -> CallStack.key cs) ~iter @@ -351,7 +350,7 @@ let () = Server.Request.register ~package ~kind:`GET - ~name:"eva.values.compute" + ~name:"getEvaValues" ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue") ~input:(module Kernel_ast.Marker) ~output:(module Junit)