diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts index c4748c158dba36d3d436d3d9b26f33489c284f56..4ab597b11ad1ae7227d7a33953b6571395258dc8 100644 --- a/ivette/src/frama-c/kernel/api/ast/index.ts +++ b/ivette/src/frama-c/kernel/api/ast/index.ts @@ -468,4 +468,20 @@ export const parseExpr: Server.GetRequest< marker >= parseExpr_internal; +const parseLval_internal: Server.GetRequest< + { term: string, stmt: marker }, + marker + > = { + kind: Server.RqKind.GET, + name: 'kernel.ast.parseLval', + input: Json.jObject({ term: Json.jString, stmt: jMarker,}), + output: jMarker, + signals: [], +}; +/** Parse a C lvalue and returns the associated marker */ +export const parseLval: Server.GetRequest< + { term: string, stmt: marker }, + marker + >= parseLval_internal; + /* ------------------------------------- */ diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index df5fc860bc5bbaad1dc850a7101a8f5cf9797303..35526a1bf7419ae8a48ca9f2cde992083ede6c05 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -839,20 +839,31 @@ let () = (* --- Build a marker from an ACSL term --- *) (* -------------------------------------------------------------------------- *) -let build_marker ~stmt ~term = - let env = - let open Logic_typing in - Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label - in - try - let kf = Kernel_function.find_englobing_kf stmt in - let term = Logic_parse_string.term ~env kf term in - let exp = Logic_to_c.term_to_exp term in - Some (Printer_tag.PExp (Some kf, Kstmt stmt, exp)) - with Not_found - | Logic_parse_string.Error _ - | Logic_parse_string.Unbound _ - | Logic_to_c.No_conversion -> None (* TODO: return an error message. *) +let parse_expr env kf stmt term = + let term = Logic_parse_string.term ~env kf term in + let exp = Logic_to_c.term_to_exp term in + Printer_tag.PExp (Some kf, Kstmt stmt, exp) + +let parse_lval env kf stmt term = + let term = Logic_parse_string.term_lval ~env kf term in + let lval = Logic_to_c.term_lval_to_lval term in + Printer_tag.PLval (Some kf, Kstmt stmt, lval) + +let build_marker parse marker term = + match Printer_tag.ki_of_localizable marker with + | Kglobal -> Data.failure "No statement at selection point" + | Kstmt stmt -> + let env = + let open Logic_typing in + Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label + in + try + let kf = Kernel_function.find_englobing_kf stmt in + parse env kf stmt term + with Not_found + | Logic_parse_string.Error _ + | Logic_parse_string.Unbound _ + | Logic_to_c.No_conversion -> Data.failure "Invalid term" let () = let module Md = Markdown in @@ -866,13 +877,20 @@ let () = Request.register_sig ~package s ~kind:`GET ~name:"parseExpr" ~descr:(Md.plain "Parse a C expression and returns the associated marker") - begin fun rq () -> - match Printer_tag.ki_of_localizable @@ get_marker rq with - | Kglobal -> Data.failure "No statement at selection point" - | Kstmt stmt -> - match build_marker ~stmt ~term:(get_term rq) with - | None -> Data.failure "Invalid expression" - | Some tag -> tag - end + (fun rq () -> build_marker parse_expr (get_marker rq) (get_term rq)) + +let () = + let module Md = Markdown in + let s = Request.signature ~output:(module Marker) () in + let get_marker = Request.param s ~name:"stmt" + ~descr:(Md.plain "Marker position from where to localize the term") + (module Marker) in + let get_term = Request.param s ~name:"term" + ~descr:(Md.plain "ACSL term to parse") + (module Data.Jstring) in + Request.register_sig ~package s + ~kind:`GET ~name:"parseLval" + ~descr:(Md.plain "Parse a C lvalue and returns the associated marker") + (fun rq () -> build_marker parse_lval (get_marker rq) (get_term rq)) (* -------------------------------------------------------------------------- *)