package frama-c
Platform dedicated to the analysis of source code written in C
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
SSylvain Chiron
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
BBenjamin Jorge
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
KKilyan Le Gallic
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
CCécile Ruet-Cros
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
frama-c-31.0-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567
doc/src/frama-c-server.core/server_batch.ml.html
Source file server_batch.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
(**************************************************************************) (* *) (* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) (* Only Compiled when package Zmq is installed *) (* No interface, registered via side-effects *) (* -------------------------------------------------------------------------- *) (* --- ZeroMQ Server Options --- *) (* -------------------------------------------------------------------------- *) module Senv = Server_parameters let batch_group = Senv.add_group "Protocol BATCH" let () = Parameter_customize.set_group batch_group module Batch = Senv.String_list (struct let option_name = "-server-batch" let arg_name = "file.json,..." let help = "Executes all requests in each <file.json>, and save the \ associated results in <file.out.json>." end) let () = Parameter_customize.set_group batch_group let () = Parameter_customize.do_not_save () module BatchOutputDir = Senv.Empty_string (struct let option_name = "-server-batch-output-dir" let arg_name = "path" let help = "Outputs the results of -server-batch in <path> instead of the input \ directory." end) let () = Server_doc.protocol ~title:"Batch Protocol" ~readme:"server_batch.md" (* -------------------------------------------------------------------------- *) (* --- Execute JSON --- *) (* -------------------------------------------------------------------------- *) module Js = Yojson.Basic module Ju = Yojson.Basic.Util let pretty = Js.pretty_print ~std:false let execute_command js = let request = Ju.member "request" js |> Ju.to_string in let id = Ju.member "id" js in let data = Ju.member "data" js in match Main.find request with | None -> Senv.error "[batch] %a: request %S not found" pretty id request ; `Assoc [ "id" , id ; "error" , `String "request not found" ] | Some (kind,handler) -> try Senv.feedback "[%a] %s" Main.pp_kind kind request ; `Assoc [ "id" , id ; "data" , handler data ] with Data.InputError(msg) -> Senv.error "[%s] %s@." request msg ; `Assoc [ "id" , id ; "error" , `String msg ; "at" , js ] let rec execute_batch js = match js with | `Null -> `Null | `List js -> `List (List.map execute_batch js) | js -> try execute_command js with Ju.Type_error(msg,js) -> Senv.error "[batch] incorrect encoding:@\n%s@\n@[<hov 2>At: %a@]@." msg pretty js ; `Null (* -------------------------------------------------------------------------- *) (* --- Execute the Scripts --- *) (* -------------------------------------------------------------------------- *) let execute () = begin let files = Batch.get () in Batch.clear () ; (* clear in any case *) List.iter begin fun file -> Senv.feedback "Script %S" file ; let response = try execute_batch (Js.from_file file) with Yojson.Json_error msg -> Senv.error "[batch] error in JSON file:@\n%s@." msg; `Null in let output = Filename.remove_extension file ^ ".out.json" in let output = match BatchOutputDir.get () with | "" -> output | dir -> Filename.(dir ^ dir_sep ^ basename output) in Senv.feedback "Output %S" output ; let out = open_out output in Js.pretty_to_channel out response ; output_char out '\n'; close_out out end files end (* -------------------------------------------------------------------------- *) (* --- Run the Server from the Command line --- *) (* -------------------------------------------------------------------------- *) let () = Boot.Main.extend execute (* -------------------------------------------------------------------------- *)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>