diff --git a/ivette/src/dome/renderer/layout/forms.tsx b/ivette/src/dome/renderer/layout/forms.tsx
index 56b4e428a83ceb70da0e02277bb1505bdc26f31a..86183586e91b5cbd51902f9cbe389a1bc3430244 100644
--- a/ivette/src/dome/renderer/layout/forms.tsx
+++ b/ivette/src/dome/renderer/layout/forms.tsx
@@ -417,7 +417,7 @@ export interface PageProps extends FilterProps, Children {
export function Page(props: PageProps) {
const { className, style, children, ...filter } = props;
const { hidden, disabled } = useContext(filter);
- const css = Utils.classes('dome-xForm-grid', className);
+ const css = Utils.classes(className ?? 'dome-xForm-grid');
if (hidden) return null;
return (
<div className={css} style={style}>
@@ -598,7 +598,7 @@ export function Field(props: GenericFieldProps) {
>
{label}
</label>
- <div className={cssField}>
+ <div className={cssField} title={title}>
{children}
{WARNING}
</div>
diff --git a/ivette/src/frama-c/api/generated/kernel/ast/index.ts b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
index e6053cb2610892878eaa809c997d6c6064afa04d..89d14dc6e8599a29643125ac8fdd0c722e8ec1e1 100644
--- a/ivette/src/frama-c/api/generated/kernel/ast/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/ast/index.ts
@@ -53,14 +53,6 @@ import { jTextSafe } from 'frama-c/api/kernel/data';
import { tag } from 'frama-c/api/kernel/data';
//@ts-ignore
import { text } from 'frama-c/api/kernel/data';
-//@ts-ignore
-import { bySource } from 'frama-c/api/kernel/services';
-//@ts-ignore
-import { jSource } from 'frama-c/api/kernel/services';
-//@ts-ignore
-import { jSourceSafe } from 'frama-c/api/kernel/services';
-//@ts-ignore
-import { source } from 'frama-c/api/kernel/services';
const compute_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
@@ -77,6 +69,33 @@ export const changed: Server.Signal = {
name: 'kernel.ast.changed',
};
+/** Source file positions. */
+export type source =
+ { dir: string, base: string, file: string, line: number };
+
+/** Loose decoder for `source` */
+export const jSource: Json.Loose<source> =
+ Json.jObject({
+ dir: Json.jFail(Json.jString,'String expected'),
+ base: Json.jFail(Json.jString,'String expected'),
+ file: Json.jFail(Json.jString,'String expected'),
+ line: Json.jFail(Json.jNumber,'Number expected'),
+ });
+
+/** Safe decoder for `source` */
+export const jSourceSafe: Json.Safe<source> =
+ Json.jFail(jSource,'Source expected');
+
+/** Natural order for `source` */
+export const bySource: Compare.Order<source> =
+ Compare.byFields
+ <{ dir: string, base: string, file: string, line: number }>({
+ dir: Compare.string,
+ base: Compare.string,
+ file: Compare.string,
+ line: Compare.number,
+ });
+
/** Marker kind */
export enum markerKind {
/** Expression */
diff --git a/ivette/src/frama-c/api/generated/kernel/properties/index.ts b/ivette/src/frama-c/api/generated/kernel/properties/index.ts
index 6c5a7309f5003aeccd2b0cba0b173e9a7af87853..1379aced2c69b7e54f858187595db95f925a2968 100644
--- a/ivette/src/frama-c/api/generated/kernel/properties/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/properties/index.ts
@@ -38,21 +38,21 @@ import * as Server from 'frama-c/server';
import * as State from 'frama-c/states';
//@ts-ignore
-import { byTag } from 'frama-c/api/kernel/data';
+import { bySource } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { jTag } from 'frama-c/api/kernel/data';
+import { jSource } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { jTagSafe } from 'frama-c/api/kernel/data';
+import { jSourceSafe } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { tag } from 'frama-c/api/kernel/data';
+import { source } from 'frama-c/api/kernel/ast';
//@ts-ignore
-import { bySource } from 'frama-c/api/kernel/services';
+import { byTag } from 'frama-c/api/kernel/data';
//@ts-ignore
-import { jSource } from 'frama-c/api/kernel/services';
+import { jTag } from 'frama-c/api/kernel/data';
//@ts-ignore
-import { jSourceSafe } from 'frama-c/api/kernel/services';
+import { jTagSafe } from 'frama-c/api/kernel/data';
//@ts-ignore
-import { source } from 'frama-c/api/kernel/services';
+import { tag } from 'frama-c/api/kernel/data';
/** Property Kinds */
export enum propKind {
diff --git a/ivette/src/frama-c/api/generated/kernel/services/index.ts b/ivette/src/frama-c/api/generated/kernel/services/index.ts
index fa99770d45ee200b26aee47c0a16fff8b2bdfc42..d271d8fd722e44a281c5214cc56d93f47746cfc9 100644
--- a/ivette/src/frama-c/api/generated/kernel/services/index.ts
+++ b/ivette/src/frama-c/api/generated/kernel/services/index.ts
@@ -37,6 +37,22 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byMarker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { bySource } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jMarker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jMarkerSafe } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jSource } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jSourceSafe } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { marker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { source } from 'frama-c/api/kernel/ast';
//@ts-ignore
import { byTag } from 'frama-c/api/kernel/data';
//@ts-ignore
@@ -87,33 +103,6 @@ const save_internal: Server.SetRequest<string,string | undefined> = {
/** Save the current session. Returns an error, if not successfull. */
export const save: Server.SetRequest<string,string | undefined>= save_internal;
-/** Source file positions. */
-export type source =
- { dir: string, base: string, file: string, line: number };
-
-/** Loose decoder for `source` */
-export const jSource: Json.Loose<source> =
- Json.jObject({
- dir: Json.jFail(Json.jString,'String expected'),
- base: Json.jFail(Json.jString,'String expected'),
- file: Json.jFail(Json.jString,'String expected'),
- line: Json.jFail(Json.jNumber,'Number expected'),
- });
-
-/** Safe decoder for `source` */
-export const jSourceSafe: Json.Safe<source> =
- Json.jFail(jSource,'Source expected');
-
-/** Natural order for `source` */
-export const bySource: Compare.Order<source> =
- Compare.byFields
- <{ dir: string, base: string, file: string, line: number }>({
- dir: Compare.string,
- base: Compare.string,
- file: Compare.string,
- line: Compare.number,
- });
-
/** Log messages categories. */
export enum logkind {
/** User Error */
@@ -150,6 +139,108 @@ const logkindTags_internal: Server.GetRequest<null,tag[]> = {
/** Registered tags for the above type. */
export const logkindTags: Server.GetRequest<null,tag[]>= logkindTags_internal;
+/** Data for array rows [`message`](#message) */
+export interface messageData {
+ /** Entry identifier. */
+ key: Json.key<'#message'>;
+ /** Message kind */
+ kind: logkind;
+ /** Emitter plugin */
+ plugin: string;
+ /** Message text */
+ message: string;
+ /** Message category (only for debug or warning messages) */
+ category?: string;
+ /** Source file position */
+ source?: source;
+ /** Marker at the message position (if any) */
+ marker?: marker;
+ /** Function containing the message position (if any) */
+ fct?: Json.key<'#fct'>;
+}
+
+/** Loose decoder for `messageData` */
+export const jMessageData: Json.Loose<messageData> =
+ Json.jObject({
+ key: Json.jFail(Json.jKey<'#message'>('#message'),'#message expected'),
+ kind: jLogkindSafe,
+ plugin: Json.jFail(Json.jString,'String expected'),
+ message: Json.jFail(Json.jString,'String expected'),
+ category: Json.jString,
+ source: jSource,
+ marker: jMarker,
+ fct: Json.jKey<'#fct'>('#fct'),
+ });
+
+/** Safe decoder for `messageData` */
+export const jMessageDataSafe: Json.Safe<messageData> =
+ Json.jFail(jMessageData,'MessageData expected');
+
+/** Natural order for `messageData` */
+export const byMessageData: Compare.Order<messageData> =
+ Compare.byFields
+ <{ key: Json.key<'#message'>, kind: logkind, plugin: string,
+ message: string, category?: string, source?: source, marker?: marker,
+ fct?: Json.key<'#fct'> }>({
+ key: Compare.string,
+ kind: byLogkind,
+ plugin: Compare.alpha,
+ message: Compare.string,
+ category: Compare.defined(Compare.string),
+ source: Compare.defined(bySource),
+ marker: Compare.defined(byMarker),
+ fct: Compare.defined(Compare.string),
+ });
+
+/** Signal for array [`message`](#message) */
+export const signalMessage: Server.Signal = {
+ name: 'kernel.services.signalMessage',
+};
+
+const reloadMessage_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.services.reloadMessage',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Force full reload for array [`message`](#message) */
+export const reloadMessage: Server.GetRequest<null,null>= reloadMessage_internal;
+
+const fetchMessage_internal: Server.GetRequest<
+ number,
+ { pending: number, updated: messageData[], removed: Json.key<'#message'>[],
+ reload: boolean }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.services.fetchMessage',
+ input: Json.jNumber,
+ output: Json.jObject({
+ pending: Json.jFail(Json.jNumber,'Number expected'),
+ updated: Json.jList(jMessageData),
+ removed: Json.jList(Json.jKey<'#message'>('#message')),
+ reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+ }),
+ signals: [],
+};
+/** Data fetcher for array [`message`](#message) */
+export const fetchMessage: Server.GetRequest<
+ number,
+ { pending: number, updated: messageData[], removed: Json.key<'#message'>[],
+ reload: boolean }
+ >= fetchMessage_internal;
+
+const message_internal: State.Array<Json.key<'#message'>,messageData> = {
+ name: 'kernel.services.message',
+ getkey: ((d:messageData) => d.key),
+ signal: signalMessage,
+ fetch: fetchMessage,
+ reload: reloadMessage,
+ order: byMessageData,
+};
+/** Log messages */
+export const message: State.Array<Json.key<'#message'>,messageData> = message_internal;
+
/** Message event record. */
export interface log {
/** Message kind */
diff --git a/ivette/src/frama-c/index.tsx b/ivette/src/frama-c/index.tsx
index 491dd3599af16f3147a99385c529d25ced0e5525..e9433d25ad01fc9ae467b199c7328923b4e3ed2a 100644
--- a/ivette/src/frama-c/index.tsx
+++ b/ivette/src/frama-c/index.tsx
@@ -35,6 +35,7 @@ import ASTinfo from 'frama-c/kernel/ASTinfo';
import SourceCode from 'frama-c/kernel/SourceCode';
import Locations from 'frama-c/kernel/Locations';
import Properties from 'frama-c/kernel/Properties';
+import Messages from 'frama-c/kernel/Messages';
import 'frama-c/kernel/style.css';
@@ -83,6 +84,12 @@ Ivette.registerGroup({
title: 'Status of ASCL Properties',
children: <Properties />,
});
+ Ivette.registerComponent({
+ id: 'frama-c.messages',
+ label: 'Messages',
+ title: 'Messages emitted by Frama-C',
+ children: <Messages />,
+ });
});
/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/kernel/Messages.tsx b/ivette/src/frama-c/kernel/Messages.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..6a88a35d4d4c8fcc3a40917508cdcfd4c41b5a9a
--- /dev/null
+++ b/ivette/src/frama-c/kernel/Messages.tsx
@@ -0,0 +1,429 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+import * as React from 'react';
+import * as Dome from 'dome';
+import { TitleBar } from 'ivette';
+
+import { IconButton } from 'dome/controls/buttons';
+import { Label, Cell, Data } from 'dome/controls/labels';
+import { Icon } from 'dome/controls/icons';
+import { Scroll } from 'dome/layout/boxes';
+import { RSplit } from 'dome/layout/splitters';
+import * as Forms from 'dome/layout/forms';
+import * as Arrays from 'dome/table/arrays';
+import { Table, Column, Renderer } from 'dome/table/views';
+import * as Compare from 'dome/data/compare';
+
+import * as States from 'frama-c/states';
+import * as Ast from 'frama-c/api/kernel/ast';
+import * as Kernel from 'frama-c/api/kernel/services';
+
+type Message = Kernel.messageData;
+
+// --------------------------------------------------------------------------
+// --- Filters
+// --------------------------------------------------------------------------
+
+interface Search {
+ category?: string;
+ message?: string;
+}
+
+interface KindFilter {
+ result?: boolean;
+ feedback?: boolean;
+ debug?: boolean;
+ warning?: boolean;
+ error?: boolean;
+ failure?: boolean;
+}
+
+interface PluginFilter {
+ kernel?: boolean;
+ server?: boolean;
+ eva?: boolean;
+ wp?: boolean;
+ nonterm?: boolean;
+ others?: boolean;
+}
+
+interface Filter {
+ currentFct: boolean;
+ search: Search;
+ kind: KindFilter;
+ plugin: PluginFilter;
+}
+
+const defaultFilter: Filter = {
+ currentFct: false,
+ search: {},
+ kind: {
+ result: false,
+ feedback: false,
+ debug: false,
+ },
+ plugin: {},
+};
+
+function filterKind(filter: KindFilter, msg: Message) {
+ const hide =
+ (filter.result === false && msg.kind === 'RESULT')
+ || (filter.feedback === false && msg.kind === 'FEEDBACK')
+ || (filter.debug === false && msg.kind === 'DEBUG')
+ || (filter.warning === false && msg.kind === 'WARNING')
+ || (filter.error === false && msg.kind === 'ERROR')
+ || (filter.failure === false && msg.kind === 'FAILURE');
+ return !hide;
+}
+
+function filterPlugin(filter: PluginFilter, msg: Message) {
+ switch (msg.plugin) {
+ case 'kernel': return !(filter.kernel === false);
+ case 'server': return !(filter.server === false);
+ case 'eva': return !(filter.eva === false);
+ case 'wp': return !(filter.wp === false);
+ case 'nonterm': return !(filter.nonterm === false);
+ default: return !(filter.others === false);
+ }
+}
+
+function searchCategory(search: string | undefined, msg: string | undefined) {
+ if (!search || search.length < 2)
+ return true;
+ if (!msg)
+ return false;
+ const message = msg.toLowerCase();
+ const array = search.toLowerCase().split(' ');
+ let empty = true;
+ let show = false;
+ let hide = false;
+ array.forEach((str: string) => {
+ if (str.length > 1) {
+ if (str.charAt(0) === '-') {
+ if (message.includes(str.substring(1)))
+ hide = true;
+ }
+ else if (message.includes(str))
+ show = true;
+ else
+ empty = false;
+ }
+ });
+ return (empty || show) && !hide;
+}
+
+function searchString(search: string | undefined, msg: string) {
+ if (!search || search.length < 3)
+ return true;
+ if (search.charAt(0) === '"' && search.slice(-1) === '"') {
+ const exact = search.slice(1, -1);
+ return msg.includes(exact);
+ }
+ const message = msg.toLowerCase();
+ const array = search.toLowerCase().split(' ');
+ let show = true;
+ array.forEach((str: string) => {
+ if (str.length > 1 && !message.includes(str))
+ show = false;
+ });
+ return show;
+}
+
+function filterSearched(search: Search, msg: Message) {
+ return (searchString(search.message, msg.message) &&
+ searchCategory(search.category, msg.category));
+}
+
+function filterFunction(filter: Filter, kf: string | undefined, msg: Message) {
+ if (filter.currentFct)
+ return (kf === msg.fct);
+ return true;
+}
+
+function filterMessage(filter: Filter, kf: string | undefined, msg: Message) {
+ return (filterFunction(filter, kf, msg) &&
+ filterSearched(filter.search, msg) &&
+ filterKind(filter.kind, msg) &&
+ filterPlugin(filter.plugin, msg));
+}
+
+// --------------------------------------------------------------------------
+// --- Filters panel and ratio
+// --------------------------------------------------------------------------
+
+function MessageFilter(props: {filter: Forms.FieldState<Filter>}) {
+ const state = props.filter;
+ const search = Forms.useProperty(state, 'search');
+ const categoryState = Forms.useProperty(search, 'category');
+ const messageState = Forms.useProperty(search, 'message');
+
+ const kind = Forms.useProperty(state, 'kind');
+ function kindState(path: keyof KindFilter) {
+ return Forms.useDefault(Forms.useProperty(kind, path), true);
+ }
+
+ const plugin = Forms.useProperty(state, 'plugin');
+ function pluginState(path: keyof PluginFilter) {
+ return Forms.useDefault(Forms.useProperty(plugin, path), true);
+ }
+
+ return (
+ <Scroll>
+ <Forms.Page className="message-search">
+ <Forms.CheckboxField
+ label="Current function"
+ title="Only show messages emitted at the current function"
+ state={Forms.useProperty(state, 'currentFct')}
+ />
+ <Forms.Section
+ label="Search"
+ unfold
+ settings="ivette.messages.search"
+ >
+ <Forms.TextField
+ label="Category"
+ state={categoryState}
+ placeholder="Category"
+ title={'Search in message category.\n'
+ + 'Use -<name> to hide some categories.'}
+ />
+ <Forms.TextField
+ label="Message"
+ state={messageState}
+ placeholder="Message"
+ title={'Search in message text.\n'
+ + 'Case-insensitive by default.\n'
+ + 'Use "text" for an exact case-sensitive search.'}
+ />
+ </Forms.Section>
+ <Forms.Section
+ label="Kind"
+ unfold
+ settings="ivette.messages.filterKind"
+ >
+ <Forms.CheckboxField label="Result" state={kindState('result')} />
+ <Forms.CheckboxField label="Feedback" state={kindState('feedback')} />
+ <Forms.CheckboxField label="Debug" state={kindState('debug')} />
+ <Forms.CheckboxField label="Warning" state={kindState('warning')} />
+ <Forms.CheckboxField label="Error" state={kindState('error')} />
+ <Forms.CheckboxField label="Failure" state={kindState('failure')} />
+ </Forms.Section>
+ <Forms.Section
+ label="Emitter"
+ unfold
+ settings="ivette.messages.filterEmitter"
+ >
+ <Forms.CheckboxField label="Kernel" state={pluginState('kernel')} />
+ <Forms.CheckboxField label="Server" state={pluginState('server')} />
+ <Forms.CheckboxField label="Eva" state={pluginState('eva')} />
+ <Forms.CheckboxField label="WP" state={pluginState('wp')} />
+ <Forms.CheckboxField label="Nonterm" state={pluginState('nonterm')} />
+ <Forms.CheckboxField label="Others" state={pluginState('others')} />
+ </Forms.Section>
+ </Forms.Page>
+ </Scroll>
+ );
+}
+
+function FilterRatio({ model }: { model: Arrays.ArrayModel<any, any> }) {
+ const [filtered, total] = [model.getRowCount(), model.getTotalRowCount()];
+ const title = `${filtered} displayed messages / ${total} total messages`;
+ return (
+ <Label className="component-info" title={title}>
+ {filtered} / {total}
+ </Label>
+ );
+}
+
+// --------------------------------------------------------------------------
+// --- Messages Columns
+// --------------------------------------------------------------------------
+
+const renderKind: Renderer<Kernel.logkind> = (kind: Kernel.logkind) => {
+ const label = kind.toLocaleLowerCase();
+ let icon = '';
+ let color = 'black';
+ switch (kind) {
+ case 'RESULT': icon = 'ANGLE.RIGHT'; break;
+ case 'FEEDBACK': icon = 'CIRC.INFO'; break;
+ case 'DEBUG': icon = 'HELP'; break;
+ case 'WARNING': icon = 'ATTENTION'; color = '#C00000'; break;
+ case 'ERROR': case 'FAILURE': icon = 'WARNING'; color = '#C00000'; break;
+ }
+ return <Icon title={label} id={icon} fill={color} />;
+};
+
+const renderCell: Renderer<string> =
+ (text: string) => (<Cell title={text}>{text}</Cell>);
+
+const renderMessage: Renderer<string> =
+ (text: string) => (<Data title={text}> {text} </Data>);
+
+const renderDir: Renderer<Ast.source> =
+ (loc: Ast.source) => (<Cell label={loc.dir} title={loc.file} />);
+
+const renderFile: Renderer<Ast.source> =
+ (loc: Ast.source) => (
+ <Cell label={`${loc.base}:${loc.line}`} title={loc.file} />
+ );
+
+const MessageColumns = () => (
+ <>
+ <Column
+ id="kind"
+ title="Message kind"
+ label="Kind"
+ width={42}
+ align="center"
+ render={renderKind}
+ />
+ <Column
+ id="plugin"
+ label="Emitter"
+ title="Frama-C kernel or plugin"
+ width={75}
+ render={renderCell}
+ />
+ <Column
+ id="category"
+ label="Category"
+ title="Only for warning and debug messages"
+ width={120}
+ render={renderCell}
+ />
+ <Column
+ id="message"
+ label="Message"
+ fill
+ render={renderMessage}
+ />
+ <Column
+ id="fct"
+ label="Function"
+ width={120}
+ render={renderCell}
+ />
+ <Column
+ id="dir"
+ label="Directory"
+ width={240}
+ visible={false}
+ getter={(msg: Message) => msg?.source}
+ render={renderDir}
+ />
+ <Column
+ id="file"
+ label="File"
+ width={150}
+ getter={(msg: Message) => msg?.source}
+ render={renderFile}
+ />
+ <Column
+ id="key"
+ label="Id"
+ title="Message emission order"
+ width={42}
+ visible={false}
+ />
+ </>
+);
+
+// -------------------------------------------------------------------------
+// --- Mesages Table
+// -------------------------------------------------------------------------
+
+const bySource =
+ Compare.byFields<Ast.source>({ file: Compare.alpha, line: Compare.number });
+
+const byMessage: Compare.ByFields<Message> = {
+ key: Compare.lift(parseInt, Compare.bignum),
+ kind: Compare.structural,
+ plugin: Compare.string,
+ category: Compare.defined(Compare.string),
+ fct: Compare.defined(Compare.alpha),
+ source: Compare.defined(bySource),
+};
+
+export default function RenderMessages() {
+
+ const model = React.useMemo(() => (
+ new Arrays.CompactModel<string, Message>((msg: Message) => msg.key)
+ ), []);
+ const data = States.useSyncArray(Kernel.message).getArray();
+ model.setOrderingByFields(byMessage);
+
+ React.useEffect(() => {
+ model.removeAllData();
+ model.updateData(data);
+ model.reload();
+ }, [model, data]);
+
+ const filterState = Forms.useState<Filter>(defaultFilter);
+ const [selection, updateSelection] = States.useSelection();
+ const selectedFct = selection?.current?.fct;
+
+ React.useEffect(() => {
+ const [filter] = filterState;
+ model.setFilter((msg: Message) => filterMessage(filter, selectedFct, msg));
+ }, [model, filterState, selectedFct]);
+
+ const onMessageSelection = React.useCallback(
+ ({ fct, marker }: Message) => {
+ if (fct && marker) {
+ const location = { fct, marker };
+ updateSelection({ location });
+ }
+ }, [updateSelection],
+ );
+
+ const [showFilter, flipFilter] =
+ Dome.useFlipSettings('ivette.messages.showFilter', true);
+
+ return (
+ <>
+ <TitleBar>
+ <FilterRatio model={model} />
+ <IconButton
+ icon="CLIPBOARD"
+ selected={showFilter}
+ onClick={flipFilter}
+ title="Toggle filters panel"
+ />
+ </TitleBar>
+ <RSplit
+ settings="ivette.messages.filterSplit"
+ unfold={showFilter}
+ >
+ <Table<string, Message>
+ model={model}
+ sorting={model}
+ onSelection={onMessageSelection}
+ settings="ivette.messages.table"
+ >
+ <MessageColumns />
+ </Table>
+ <MessageFilter filter={filterState} />
+ </RSplit>
+ </>
+ );
+}
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 57f65e5d2f6ab5190a84b31ed932be0d5aade5c4..ca92fa637777ba381e9b2dd8c94b185ece5934a9 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -42,7 +42,7 @@ import { Scroll, Folder } from 'dome/layout/boxes';
import { RSplit } from 'dome/layout/splitters';
-import { source as SourceLoc } from 'frama-c/api/kernel/services';
+import * as Ast from 'frama-c/api/kernel/ast';
import { statusData } from 'frama-c/api/kernel/properties';
import * as Properties from 'frama-c/api/kernel/properties';
import * as Eva from 'frama-c/api/plugins/eva/general';
@@ -245,13 +245,13 @@ const renderNames: Renderer<string[]> =
return (label ? <Label label={label} /> : null);
};
-const renderDir: Renderer<SourceLoc> =
- (loc: SourceLoc) => (
+const renderDir: Renderer<Ast.source> =
+ (loc: Ast.source) => (
<Code className="code-column" label={loc.dir} title={loc.file} />
);
-const renderFile: Renderer<SourceLoc> =
- (loc: SourceLoc) => (
+const renderFile: Renderer<Ast.source> =
+ (loc: Ast.source) => (
<Code className="code-column" label={loc.base} title={loc.file} />
);
@@ -286,7 +286,7 @@ function ColumnTag<Row>(props: ColumnProps<Row, States.Tag>) {
// -------------------------------------------------------------------------
const bySource =
- Compare.byFields<SourceLoc>({ file: Compare.alpha, line: Compare.number });
+ Compare.byFields<Ast.source>({ file: Compare.alpha, line: Compare.number });
const byStatus =
Compare.byRank(
@@ -327,8 +327,8 @@ const byProperty: Compare.ByFields<Property> = {
taint: byTaint,
};
-const byDir = Compare.byFields<SourceLoc>({ dir: Compare.alpha });
-const byFile = Compare.byFields<SourceLoc>({ base: Compare.alpha });
+const byDir = Compare.byFields<Ast.source>({ dir: Compare.alpha });
+const byFile = Compare.byFields<Ast.source>({ base: Compare.alpha });
const byColumn: Arrays.ByColumns<Property> = {
dir: Compare.byFields<Property>({ source: byDir }),
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index e38461a97fa668b18180a6cc3cef2af45fb0bbe6..b635b6facafb4e03e68f036e3b61d139dbe154bc 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -33,8 +33,7 @@ import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { TitleBar } from 'ivette';
import * as Preferences from 'ivette/prefs';
-import { functions, markerInfo } from 'frama-c/api/kernel/ast';
-import { source } from 'frama-c/api/kernel/services';
+import { functions, markerInfo, source } from 'frama-c/api/kernel/ast';
import 'codemirror/addon/selection/active-line';
import 'codemirror/addon/dialog/dialog.css';
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index 04aacdc2e13f2fb6a72f6b6bc2eabbfa7d6decdf..0d546d7f4bee853711c6f7fe3a0869b03681fd84 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -50,3 +50,35 @@
}
/* -------------------------------------------------------------------------- */
+/* --- Globals --- */
+/* -------------------------------------------------------------------------- */
+
+.message-search {
+ padding: 4px 4px 4px 14px;
+}
+
+.message-search .dome-xForm-section {
+ margin-top: 6px ;
+ left: auto; /* Cancel dome left placement */
+}
+
+.message-search .dome-xForm-label {
+ display: none; /* Hide label, only use placeholder */
+}
+
+.message-search input::placeholder {
+ font-style: italic;
+}
+
+.message-search input {
+ vertical-align: middle;
+ margin: 2px 4px 2px 0px;
+}
+
+.message-search .dome-xForm-field {
+ margin: 0px 4px;
+ display: inline-block;
+ min-width: 80px;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/renderer/style.css b/ivette/src/renderer/style.css
index 3f56713b0c713f1385e5af163d3fa0b810ff8999..c210426cfccbb0b7b70c7e638c4a6bc3077225a9 100644
--- a/ivette/src/renderer/style.css
+++ b/ivette/src/renderer/style.css
@@ -10,7 +10,7 @@
}
.component-info {
- color: #888 ;
+ color: #555 ;
min-width: 50px;
padding-top: 4px;
font-size: smaller;
diff --git a/src/kernel_internals/runtime/messages.ml b/src/kernel_internals/runtime/messages.ml
index 391a0bec9a729f610780b121bbe132040b055064..e5b50b271e57ff5f7a29951169a2942731c7c94c 100644
--- a/src/kernel_internals/runtime/messages.ml
+++ b/src/kernel_internals/runtime/messages.ml
@@ -40,7 +40,7 @@ module DatatypeMessages =
end)
module Messages =
- State_builder.List_ref
+ State_builder.Queue
(DatatypeMessages)
(struct
let name = "Messages.message_table"
@@ -51,33 +51,33 @@ let () = Ast.add_monotonic_state Messages.self
let hooks = ref []
let add_message m =
begin
- Messages.set (m :: Messages.get ()) ;
+ Messages.add m;
List.iter (fun fn -> fn()) !hooks ;
end
let nb_errors () =
- Messages.fold_left
+ Messages.fold
(fun n e ->
match e.Log.evt_kind with
| Log.Error -> succ n
| _ -> n) 0
let nb_warnings () =
- Messages.fold_left
+ Messages.fold
(fun n e ->
match e.Log.evt_kind with
| Log.Warning -> succ n
| _ -> n) 0
-let nb_messages() = List.length (Messages.get ())
+let nb_messages = Messages.length
let self = Messages.self
-let iter f = List.iter f (List.rev (Messages.get ()))
+let iter = Messages.iter
+let fold = Messages.fold
let dump_messages () = iter Log.echo
-let () =
- Log.add_listener ~kind:[ Log.Error; Log.Warning ] add_message
+let () = Log.add_listener add_message
module OnceTable =
State_builder.Hashtbl
diff --git a/src/kernel_internals/runtime/messages.mli b/src/kernel_internals/runtime/messages.mli
index ecac858d28deae0e81b7f4ea69f838de0b7404fd..04f5927556afc7a20555ec6c52fdc1635c228625 100644
--- a/src/kernel_internals/runtime/messages.mli
+++ b/src/kernel_internals/runtime/messages.mli
@@ -20,13 +20,15 @@
(* *)
(**************************************************************************)
-(** Stored messages for persistence between sessions.
- Currently, only warning and error messages are stored. *)
+(** Stored messages for persistence between sessions. *)
val iter: (Log.event -> unit) -> unit
(** Iter over all stored messages. The messages are passed in emission order.
@modify Nitrogen-20111001 Messages are now passed in emission order. *)
+val fold: ('a -> Log.event -> 'a) -> 'a -> 'a
+(** Fold over all stored messages. The messages are passed in emission order. *)
+
val dump_messages: unit -> unit
(** Dump stored messages to standard channels *)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 4f07c37e14609ce2be24fba5135655a1404ab495..c8cc00fef641d915cefd64277a9f297d865f1fce 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -244,6 +244,212 @@ let loc_of_localizable = function
| None -> Location.unknown
| Some kf -> Kernel_function.get_location kf)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Find localizable at a Filepath.position --- *)
+(* -------------------------------------------------------------------------- *)
+
+let dkey = Kernel.register_category "pretty-source"
+
+module LineToLocalizable =
+ Datatype.Hashtbl(Datatype.Int.Hashtbl)(Datatype.Int)
+ (struct let module_name = "Pretty_source.LineToLocalizable" end)
+module FileToLines =
+ Datatype.Hashtbl(Datatype.Filepath.Hashtbl)(Datatype.Filepath)
+ (struct let module_name = "Pretty_source.FilesToLine" end)
+
+module MappingLineLocalizable = struct
+ module LineToLocalizableAux =
+ LineToLocalizable.Make( Datatype.Pair(Location)(Localizable))
+
+ include State_builder.Hashtbl(FileToLines)(LineToLocalizableAux)
+ (struct
+ let size = 5
+ let dependencies = [Ast.self]
+ let name = "Pretty_source.line_to_localizable"
+ end)
+end
+
+class pos_to_localizable =
+ object (self)
+ inherit Visitor.frama_c_inplace
+
+ (* used to keep track of conditional expressions, to add them to the
+ list of relevant localizables *)
+ val mutable insideIf = None
+
+ method add_range loc (localizable : localizable) =
+ if not (Location.equal loc Location.unknown) then (
+ let p1, p2 = loc in
+ if p1.Filepath.pos_path <> p2.Filepath.pos_path then
+ Kernel.debug ~once:true ~dkey
+ "Localizable over two files: %a and %a; %a"
+ Datatype.Filepath.pretty p1.Filepath.pos_path
+ Datatype.Filepath.pretty p2.Filepath.pos_path
+ Localizable.pretty localizable;
+ let file = p1.Filepath.pos_path in
+ let hfile =
+ try MappingLineLocalizable.find file
+ with Not_found ->
+ let h = LineToLocalizable.create 17 in
+ MappingLineLocalizable.add file h;
+ h
+ in
+ for i = p1.Filepath.pos_lnum to p2.Filepath.pos_lnum do
+ LineToLocalizable.add hfile i (loc, localizable);
+ done
+ );
+
+ method! vstmt_aux s =
+ (* we ignore Block statements, since they tend to overlap existing
+ ones which are more precise *)
+ let skip = match s.skind with
+ | Block _ -> true
+ | _ -> false
+ in
+ if not skip then
+ self#add_range (Stmt.loc s) (PStmt (Option.get self#current_kf, s));
+ begin
+ match s.skind with
+ | If (exp, _, _, _) ->
+ (* conditional expressions are treated in a special way *)
+ insideIf <- Some (Kstmt s);
+ ignore (Cil.visitCilExpr (self :> Cil.cilVisitor) exp);
+ insideIf <- None
+ | _ -> ()
+ end;
+ Cil.DoChildren
+
+ method! vexpr exp =
+ begin
+ match insideIf with
+ | Some ki ->
+ (* expressions inside conditionals have a special treatment *)
+ begin
+ match exp.enode with
+ | Lval lv ->
+ (* lvals must be generated differently from other expressions *)
+ self#add_range exp.eloc (PLval(self#current_kf, ki, lv))
+ | _ ->
+ self#add_range exp.eloc (PExp(self#current_kf, ki, exp))
+ end
+ | None -> ()
+ end;
+ Cil.DoChildren
+
+ method! vvdec vi =
+ if not vi.vglob && not vi.vtemp then
+ begin
+ match self#current_kf with
+ | None -> (* should not happen*) ()
+ | Some kf ->
+ self#add_range vi.vdecl (PVDecl (Some kf,self#current_kinstr,vi));
+ end;
+ Cil.DoChildren
+
+ method! vglob_aux g =
+ (match g with
+ | GFun ({ svar = vi }, loc) ->
+ self#add_range loc
+ (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
+ | GVar (vi, _, loc) ->
+ self#add_range loc (PVDecl (None, Kglobal, vi))
+ | GFunDecl (_, vi, loc) ->
+ self#add_range loc
+ (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
+ | GVarDecl (vi, loc) ->
+ self#add_range loc (PVDecl (None, Kglobal, vi))
+ | _ -> self#add_range (Global.loc g) (PGlobal g)
+ );
+ Cil.DoChildren
+ end
+
+(* Returns [true] if the column [col] is within location [loc]. *)
+let location_contains_col loc col =
+ let (pos_start, pos_end) = loc in
+ let (col_start, col_end) =
+ pos_start.Filepath.pos_cnum - pos_start.Filepath.pos_bol,
+ pos_end.Filepath.pos_cnum - pos_end.Filepath.pos_bol
+ in
+ col_start <= col && col <= col_end
+
+(* Applies several heuristics to try and match the best localizable to a
+ given location [loc]. The list [possible_locs] should contain all
+ localizables in a given line. If [possible_col] is [true], then we try
+ to take column information into account.
+ Some heuristics may return an empty list, in which case a fallback is
+ later used to return a better choice. *)
+let apply_location_heuristics precise_col possible_locs loc =
+ let col = loc.Filepath.pos_cnum - loc.Filepath.pos_bol in
+ Kernel.debug ~dkey
+ "apply_location_heuristics (precise_col:%b): loc: %a, col: %d@\n\
+ possible_locs:@ %a"
+ precise_col Location.pretty (loc, loc) col
+ (Pretty_utils.pp_list ~sep:"@\n"
+ (Pretty_utils.pp_pair ~sep:" :: " Location.pretty Localizable.pretty)) possible_locs;
+ (* Heuristic 1: we try to obtain a subset of localizables related to a given
+ position, or a given column if [precise_col] is true.
+ May result in an empty list. *)
+ let filter_locs l =
+ List.filter (fun (((pos_start, _) as loc'), _) ->
+ if precise_col then location_contains_col loc' col
+ else loc = pos_start
+ ) l
+ in
+ (* Heuristic 2: prioritize expressions if they are present.
+ May result in an empty list. *)
+ let exps l =
+ List.filter (fun (_, lz) -> match lz with | PExp _ -> true | _ -> false) l
+ in
+ (* Heuristic 3: when we have more than one match with the exact same location,
+ we pick the last one in the list. This will be the first statement that has
+ been encountered, and this criterion seems to work well with temporaries
+ introduced by Cil. *)
+ let last l = match List.rev l with [] -> None | (_, lz) :: _ -> Some lz in
+ (* Heuristic 4: when there are no exact locations, we will consider the
+ innermost ones, that is, those at the top of the list. *)
+ let innermost_in loc l =
+ List.filter (fun (loc', _) -> Location.equal loc loc') l
+ in
+ match possible_locs, filter_locs possible_locs with
+ | [], _ -> (* no possible localizables *) None
+ | _, (_ :: _ as exact) ->
+ (* one or more exact localizables; we prioritize expressions *)
+ begin
+ match exps exact with
+ | [] -> (* no expressions, just take the last localizable *) last exact
+ | exps -> (* take the last (usually only) expression *) last exps
+ end
+ | (loc', _) :: __, [] ->
+ (* No exact loc. We consider the innermost statements,
+ ie those at the top of the list *)
+ let filtered = innermost_in loc' possible_locs in
+ last filtered
+
+let loc_to_localizable ?(precise_col=false) loc =
+ if not (MappingLineLocalizable.is_computed ()) then (
+ let vis = new pos_to_localizable in
+ Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ());
+ MappingLineLocalizable.mark_as_computed ();
+ );
+ try
+ (* Find the mapping from this file to locs-by-line *)
+ let hfile = MappingLineLocalizable.find loc.Filepath.pos_path in
+ (* Find the localizable for this line *)
+ let all = LineToLocalizable.find_all hfile loc.Filepath.pos_lnum in
+ match apply_location_heuristics precise_col all loc with
+ | Some locz ->
+ Kernel.feedback ~dkey "loc: %a -> locz: %a"
+ Location.pretty (loc,loc) Localizable.pretty locz;
+ Some locz
+ | None ->
+ Kernel.feedback ~dkey "loc: %a -> NO locz" Location.pretty (loc,loc);
+ None
+ with
+ | Not_found ->
+ Kernel.debug ~once:true ~source:loc "no matching localizable found";
+ None
+
(* -------------------------------------------------------------------------- *)
(* --- Printer API --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index a35466dfc72390bf57d86673f670c26698ec962b..4f67fdebedb480a36d572efb7ad280d6b906aca2 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -62,6 +62,12 @@ val typ_of_localizable: localizable -> typ option
val loc_of_localizable : localizable -> location
(** Might return [Location.unknown] *)
+val loc_to_localizable: ?precise_col:bool -> Filepath.position -> localizable option
+(** return the (hopefully) most precise localizable that contains the given
+ Filepath.position. If [precise_col] is [true], takes the column number into
+ account (possibly a more precise, but costly, result).
+ @since Frama-C+dev *)
+
module type Tag =
sig
val create : localizable -> string
diff --git a/src/libraries/project/state_builder.ml b/src/libraries/project/state_builder.ml
index de29e89db7baedc1d085c6912ef392d2cd289ba7..1d3ef1c2275b159718d2ddc591276be89920acc0 100644
--- a/src/libraries/project/state_builder.ml
+++ b/src/libraries/project/state_builder.ml
@@ -880,7 +880,9 @@ module type Queue = sig
val self: State.t
val add: elt -> unit
val iter: (elt -> unit) -> unit
+ val fold: ('a -> elt -> 'a) -> 'a -> 'a
val is_empty: unit -> bool
+ val length: unit -> int
end
module Queue(Data: Datatype.S)(Info: Info) = struct
@@ -913,7 +915,9 @@ module Queue(Data: Datatype.S)(Info: Info) = struct
let add x = Queue.add x !state
let iter f = Queue.iter f !state
+ let fold f acc = Queue.fold f acc !state
let is_empty () = Queue.is_empty !state
+ let length () = Queue.length !state
end
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index 0815a483f3ebfb42e5a03b50d213519cb78c8e8d..bd94ad5e2bfd7874bb4f732a53e09629c823d2e3 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -378,7 +378,9 @@ module type Queue = sig
val self: State.t
val add: elt -> unit
val iter: (elt -> unit) -> unit
+ val fold: ('a -> elt -> 'a) -> 'a -> 'a
val is_empty: unit -> bool
+ val length: unit -> int
end
module Queue(Data: Datatype.S)(Info: Info) : Queue with type elt = Data.t
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 5a9c80fef4174e1a1d6a58cd30f9aacae8e72fd9..1d24782c859ce33e1d9fcfc0cddb12ccf74705e2 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1689,14 +1689,15 @@ class main_window () : main_window_extension_points =
ignore
(lower_notebook#insert_page ~pos:1
~tab_label:warnings_tab_label w);
- let text = Format.sprintf "Messages (%d)" (Messages.nb_messages ()) in
+ let nb_messages = Messages.nb_warnings () + Messages.nb_errors () in
+ let text = Format.sprintf "Messages (%d)" nb_messages in
let label = GtkMisc.Label.cast warnings_tab_label#as_widget in
GtkMisc.Label.set_text label text
in
let callback e _column =
Option.iter
(fun pos ->
- Option.iter self#scroll (Pretty_source.loc_to_localizable pos);
+ Option.iter self#scroll (Printer_tag.loc_to_localizable pos);
(* Note: the code below generates double scrolling:
the previous call to self#scroll causes the original source
viewer to scroll to the beginning of the function, and then
@@ -1710,8 +1711,13 @@ class main_window () : main_window_extension_points =
let display_warnings () =
outdated_warnings := false ;
Warning_manager.clear warning_manager;
- Messages.iter (fun event -> Warning_manager.append warning_manager event);
- let text = Format.sprintf "Messages (%d)" (Messages.nb_messages ()) in
+ Messages.iter
+ (fun event ->
+ match event.evt_kind with
+ | Warning | Error -> Warning_manager.append warning_manager event
+ | _ -> ());
+ let nb_messages = Messages.nb_warnings () + Messages.nb_errors () in
+ let text = Format.sprintf "Messages (%d)" nb_messages in
let label = GtkMisc.Label.cast warnings_tab_label#as_widget in
GtkMisc.Label.set_text label text
in
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index be4771062cbd89762597bd888bcae9a0465157c5..d6c84731ce88000100c3e31dced5e99ecc7baea2 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -276,7 +276,7 @@ let translate_history_elt old_helt =
Filepath.pos_cnum = old_loc.Filepath.pos_cnum;
}
in
- match Pretty_source.loc_to_localizable new_loc with
+ match Printer_tag.loc_to_localizable new_loc with
| None -> (** the line is unknown *)
Some (Global g)
| Some locali ->
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index c2aa878bbe0e137972f273c35595fa538914cab5..a2852f171ab24fd5be7ff777424b1242bec759f4 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -22,7 +22,6 @@
open Cil_types
open Gtk_helper
-open Cil_datatype
open Printer_tag
type localizable = Printer_tag.localizable =
@@ -41,8 +40,6 @@ type localizable = Printer_tag.localizable =
definitions. *)
| PIP of Property.t
-let dkey = Gui_parameters.register_category "pretty-source"
-
let kf_of_localizable = Printer_tag.kf_of_localizable
let ki_of_localizable = Printer_tag.ki_of_localizable
let varinfo_of_localizable = Printer_tag.varinfo_of_localizable
@@ -419,206 +416,6 @@ let display_source globals
(fun () -> GtkSignal.disconnect event_tag#as_tag id);
)
-
-module LineToLocalizable =
- Datatype.Hashtbl(Datatype.Int.Hashtbl)(Datatype.Int)
- (struct let module_name = "Pretty_source.LineToLocalizable" end)
-module FileToLines =
- Datatype.Hashtbl(Datatype.Filepath.Hashtbl)(Datatype.Filepath)
- (struct let module_name = "Pretty_source.FilesToLine" end)
-
-module MappingLineLocalizable = struct
- module LineToLocalizableAux =
- LineToLocalizable.Make( Datatype.Pair(Location)(Localizable))
-
- include State_builder.Hashtbl(FileToLines)(LineToLocalizableAux)
- (struct
- let size = 5
- let dependencies = [Ast.self]
- let name = "Pretty_source.line_to_localizable"
- end)
-end
-
-class pos_to_localizable =
- object (self)
- inherit Visitor.frama_c_inplace
-
- (* used to keep track of conditional expressions, to add them to the
- list of relevant localizables *)
- val mutable insideIf = None
-
- method add_range loc (localizable : localizable) =
- if not (Location.equal loc Location.unknown) then (
- let p1, p2 = loc in
- if p1.Filepath.pos_path <> p2.Filepath.pos_path then
- Gui_parameters.debug ~once:true
- "Localizable over two files: %a and %a; %a"
- Datatype.Filepath.pretty p1.Filepath.pos_path
- Datatype.Filepath.pretty p2.Filepath.pos_path
- Localizable.pretty localizable;
- let file = p1.Filepath.pos_path in
- let hfile =
- try MappingLineLocalizable.find file
- with Not_found ->
- let h = LineToLocalizable.create 17 in
- MappingLineLocalizable.add file h;
- h
- in
- for i = p1.Filepath.pos_lnum to p2.Filepath.pos_lnum do
- LineToLocalizable.add hfile i (loc, localizable);
- done
- );
-
- method! vstmt_aux s =
- (* we ignore Block statements, since they tend to overlap existing
- ones which are more precise *)
- let skip = match s.skind with
- | Block _ -> true
- | _ -> false
- in
- if not skip then
- self#add_range (Stmt.loc s) (PStmt (Option.get self#current_kf, s));
- begin
- match s.skind with
- | If (exp, _, _, _) ->
- (* conditional expressions are treated in a special way *)
- insideIf <- Some (Kstmt s);
- ignore (Cil.visitCilExpr (self :> Cil.cilVisitor) exp);
- insideIf <- None
- | _ -> ()
- end;
- Cil.DoChildren
-
- method! vexpr exp =
- begin
- match insideIf with
- | Some ki ->
- (* expressions inside conditionals have a special treatment *)
- begin
- match exp.enode with
- | Lval lv ->
- (* lvals must be generated differently from other expressions *)
- self#add_range exp.eloc (PLval(self#current_kf, ki, lv))
- | _ ->
- self#add_range exp.eloc (PExp(self#current_kf, ki, exp))
- end
- | None -> ()
- end;
- Cil.DoChildren
-
- method! vvdec vi =
- if not vi.vglob && not vi.vtemp then
- begin
- match self#current_kf with
- | None -> (* should not happen*) ()
- | Some kf ->
- self#add_range vi.vdecl (PVDecl (Some kf,self#current_kinstr,vi));
- end;
- Cil.DoChildren
-
- method! vglob_aux g =
- (match g with
- | GFun ({ svar = vi }, loc) ->
- self#add_range loc
- (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
- | GVar (vi, _, loc) ->
- self#add_range loc (PVDecl (None, Kglobal, vi))
- | GFunDecl (_, vi, loc) ->
- self#add_range loc
- (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
- | GVarDecl (vi, loc) ->
- self#add_range loc (PVDecl (None, Kglobal, vi))
- | _ -> self#add_range (Global.loc g) (PGlobal g)
- );
- Cil.DoChildren
- end
-
-(* Returns [true] if the column [col] is within location [loc]. *)
-let location_contains_col loc col =
- let (pos_start, pos_end) = loc in
- let (col_start, col_end) =
- pos_start.Filepath.pos_cnum - pos_start.Filepath.pos_bol,
- pos_end.Filepath.pos_cnum - pos_end.Filepath.pos_bol
- in
- col_start <= col && col <= col_end
-
-(* Applies several heuristics to try and match the best localizable to a
- given location [loc]. The list [possible_locs] should contain all
- localizables in a given line. If [possible_col] is [true], then we try
- to take column information into account.
- Some heuristics may return an empty list, in which case a fallback is
- later used to return a better choice. *)
-let apply_location_heuristics precise_col possible_locs loc =
- let col = loc.Filepath.pos_cnum - loc.Filepath.pos_bol in
- Gui_parameters.debug ~dkey
- "apply_location_heuristics (precise_col:%b): loc: %a, col: %d@\n\
- possible_locs:@ %a"
- precise_col Location.pretty (loc, loc) col
- (Pretty_utils.pp_list ~sep:"@\n"
- (Pretty_utils.pp_pair ~sep:" :: " Location.pretty Localizable.pretty)) possible_locs;
- (* Heuristic 1: we try to obtain a subset of localizables related to a given
- position, or a given column if [precise_col] is true.
- May result in an empty list. *)
- let filter_locs l =
- List.filter (fun (((pos_start, _) as loc'), _) ->
- if precise_col then location_contains_col loc' col
- else loc = pos_start
- ) l
- in
- (* Heuristic 2: prioritize expressions if they are present.
- May result in an empty list. *)
- let exps l =
- List.filter (fun (_, lz) -> match lz with | PExp _ -> true | _ -> false) l
- in
- (* Heuristic 3: when we have more than one match with the exact same location,
- we pick the last one in the list. This will be the first statement that has
- been encountered, and this criterion seems to work well with temporaries
- introduced by Cil. *)
- let last l = match List.rev l with [] -> None | (_, lz) :: _ -> Some lz in
- (* Heuristic 4: when there are no exact locations, we will consider the
- innermost ones, that is, those at the top of the list. *)
- let innermost_in loc l =
- List.filter (fun (loc', _) -> Location.equal loc loc') l
- in
- match possible_locs, filter_locs possible_locs with
- | [], _ -> (* no possible localizables *) None
- | _, (_ :: _ as exact) ->
- (* one or more exact localizables; we prioritize expressions *)
- begin
- match exps exact with
- | [] -> (* no expressions, just take the last localizable *) last exact
- | exps -> (* take the last (usually only) expression *) last exps
- end
- | (loc', _) :: __, [] ->
- (* No exact loc. We consider the innermost statements,
- ie those at the top of the list *)
- let filtered = innermost_in loc' possible_locs in
- last filtered
-
-let loc_to_localizable ?(precise_col=false) loc =
- if not (MappingLineLocalizable.is_computed ()) then (
- let vis = new pos_to_localizable in
- Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ());
- MappingLineLocalizable.mark_as_computed ();
- );
- try
- (* Find the mapping from this file to locs-by-line *)
- let hfile = MappingLineLocalizable.find loc.Filepath.pos_path in
- (* Find the localizable for this line *)
- let all = LineToLocalizable.find_all hfile loc.Filepath.pos_lnum in
- match apply_location_heuristics precise_col all loc with
- | Some locz ->
- Gui_parameters.feedback ~dkey "loc: %a -> locz: %a"
- Location.pretty (loc,loc) Localizable.pretty locz;
- Some locz
- | None ->
- Gui_parameters.feedback ~dkey "loc: %a -> NO locz" Location.pretty (loc,loc);
- None
- with
- | Not_found ->
- Gui_parameters.debug ~once:true ~source:loc "no matching localizable found";
- None
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index a3544e647fbcc811deb9e0ad65ed6c1d4df2d1a7..96e25243efbfb0c674d2ee01f824d76ad07334c0 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -88,13 +88,6 @@ val localizable_from_locs :
This function is inefficient as it iterates on all the current
[Locs.state]. *)
-val loc_to_localizable: ?precise_col:bool -> Filepath.position -> localizable option
-(** return the (hopefully) most precise localizable that contains the given
- Filepath.position. If [precise_col] is [true], takes the column number into
- account (possibly a more precise, but costly, result).
- @since Nitrogen-20111001 *)
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/source_manager.ml b/src/plugins/gui/source_manager.ml
index d3d250910729b73520a966bd85f8ccd21d627605..7a99892c460b56eb5ee6cbca2cb491a93cac4f6a 100644
--- a/src/plugins/gui/source_manager.ml
+++ b/src/plugins/gui/source_manager.ml
@@ -171,7 +171,7 @@ let load_file w ?title ~(filename : Datatype.Filepath.t) ?(line=(-1)) ~click_cb
Filepath.pos_bol = offset - col;
Filepath.pos_cnum = offset;} in
let localz =
- Pretty_source.loc_to_localizable ~precise_col:true pos
+ Printer_tag.loc_to_localizable ~precise_col:true pos
in
click_cb localz
with Not_found ->
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index 1c00c79b8609999042fe6023274499198ebf22bb..0736b25b9d0e2ff17b1d17b90d33a96e8a491810 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -43,9 +43,9 @@ PLUGIN_CMO:= \
data main request states \
server_doc \
server_batch \
+ kernel_ast \
kernel_main \
kernel_project \
- kernel_ast \
kernel_properties
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index dce3b62f90f59c0b486db460125a9c5a9f1b214e..7ce9dd03cc6ed5e4235edfdc1d544b0471ae871b 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -46,6 +46,52 @@ let ast_update_hook f =
let () = ast_update_hook (fun _ -> Request.emit changed_signal)
+(* -------------------------------------------------------------------------- *)
+(* --- File Positions --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Position =
+struct
+ type t = Filepath.position
+
+ let jtype = Data.declare ~package ~name:"source"
+ ~descr:(Md.plain "Source file positions.")
+ (Jrecord [
+ "dir", Jstring;
+ "base", Jstring;
+ "file", Jstring;
+ "line", Jnumber;
+ ])
+
+ let to_json p =
+ let path = Filepath.(Normalized.to_pretty_string p.pos_path) in
+ let file =
+ if Server_parameters.has_relative_filepath ()
+ then path
+ else (p.Filepath.pos_path :> string)
+ in
+ `Assoc [
+ "dir" , `String (Filename.dirname path) ;
+ "base" , `String (Filename.basename path) ;
+ "file" , `String file ;
+ "line" , `Int p.Filepath.pos_lnum ;
+ ]
+
+ let of_json js =
+ let fail () = failure_from_type_error "Invalid source format" js in
+ match js with
+ | `Assoc assoc ->
+ begin
+ match List.assoc "file" assoc, List.assoc "line" assoc with
+ | `String path, `Int line ->
+ Log.source ~file:(Filepath.Normalized.of_string path) ~line
+ | _, _ -> fail ()
+ | exception Not_found -> fail ()
+ end
+ | _ -> fail ()
+
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
@@ -207,7 +253,7 @@ struct
States.column
~name:"sloc"
~descr:(Md.plain "Source location")
- ~data:(module Kernel_main.LogSource)
+ ~data:(module Position)
~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag))
model
in
@@ -471,7 +517,7 @@ struct
States.column model
~name:"sloc"
~descr:(Md.plain "Source location")
- ~data:(module Kernel_main.LogSource)
+ ~data:(module Position)
~get:(fun kf -> fst (Kernel_function.get_location kf));
States.register_array model
~package ~key
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index aa917218f410d85d2ade7922da578687cffe8355..d85697dec6786bf566dabe44780959aa27ab7572 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -27,6 +27,8 @@
open Package
open Cil_types
+module Position : Data.S with type t = Filepath.position
+
module Kf : Data.S with type t = kernel_function
module Ki : Data.S with type t = kinstr
module Stmt : Data.S with type t = stmt
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 3c5fb34a4619c6ea96e51827dfdfbb1c63420ae0..dd00d78a8f55782fb857f39cfab1eb2129cb0204 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -84,51 +84,6 @@ let () =
try Project.save_all (Filepath.Normalized.of_string file); None
with Project.IOError err -> Some err)
-(* -------------------------------------------------------------------------- *)
-(* --- File Positions --- *)
-(* -------------------------------------------------------------------------- *)
-
-module LogSource =
-struct
- type t = Filepath.position
-
- let jtype = Data.declare ~package ~name:"source"
- ~descr:(Md.plain "Source file positions.")
- (Jrecord [
- "dir", Jstring;
- "base", Jstring;
- "file", Jstring;
- "line", Jnumber;
- ])
-
- let to_json p =
- let path = Filepath.(Normalized.to_pretty_string p.pos_path) in
- let file =
- if Server_parameters.has_relative_filepath ()
- then path
- else (p.Filepath.pos_path :> string)
- in
- `Assoc [
- "dir" , `String (Filename.dirname path) ;
- "base" , `String (Filename.basename path) ;
- "file" , `String file ;
- "line" , `Int p.Filepath.pos_lnum ;
- ]
-
- let of_json js =
- let fail () = failure_from_type_error "Invalid source format" js in
- match js with
- | `Assoc assoc ->
- begin
- match List.assoc "file" assoc, List.assoc "line" assoc with
- | `String path, `Int line ->
- Log.source ~file:(Filepath.Normalized.of_string path) ~line
- | _, _ -> fail ()
- | exception Not_found -> fail ()
- end
- | _ -> fail ()
-
-end
(* -------------------------------------------------------------------------- *)
(* --- Log Lind --- *)
@@ -166,6 +121,65 @@ struct
include (val data : S with type t = Log.kind)
end
+(* -------------------------------------------------------------------------- *)
+(* --- Synchronized array of log events --- *)
+(* -------------------------------------------------------------------------- *)
+
+let model = States.model ()
+
+let () = States.column model ~name:"kind"
+ ~descr:(Md.plain "Message kind")
+ ~data:(module LogKind)
+ ~get:(fun (evt, _) -> evt.Log.evt_kind)
+
+let () = States.column model ~name:"plugin"
+ ~descr:(Md.plain "Emitter plugin")
+ ~data:(module Jalpha)
+ ~get:(fun (evt, _) -> evt.Log.evt_plugin)
+
+let () = States.column model ~name:"message"
+ ~descr:(Md.plain "Message text")
+ ~data:(module Jstring)
+ ~get:(fun (evt, _) -> evt.Log.evt_message)
+
+let () = States.option model ~name:"category"
+ ~descr:(Md.plain "Message category (only for debug or warning messages)")
+ ~data:(module Jstring)
+ ~get:(fun (evt, _) -> evt.Log.evt_category)
+
+let () = States.option model ~name:"source"
+ ~descr:(Md.plain "Source file position")
+ ~data:(module Kernel_ast.Position)
+ ~get:(fun (evt, _) -> evt.Log.evt_source)
+
+let getMarker (evt, _id) =
+ Option.bind evt.Log.evt_source Printer_tag.loc_to_localizable
+
+let getFunction t =
+ Option.bind (getMarker t) Printer_tag.kf_of_localizable
+
+let () = States.option model ~name:"marker"
+ ~descr:(Md.plain "Marker at the message position (if any)")
+ ~data:(module Kernel_ast.Marker)
+ ~get:getMarker
+
+let () = States.option model ~name:"fct"
+ ~descr:(Md.plain "Function containing the message position (if any)")
+ ~data:(module Kernel_ast.Kf)
+ ~get:getFunction
+
+let iter f = ignore (Messages.fold (fun i evt -> f (evt, i); succ i) 0)
+
+let _array =
+ States.register_array
+ ~package
+ ~name:"message"
+ ~descr:(Md.plain "Log messages")
+ ~key:(fun (_evt, i) -> string_of_int i)
+ ~iter:iter
+ ~add_reload_hook:Messages.add_global_hook
+ model
+
(* -------------------------------------------------------------------------- *)
(* --- Log Events --- *)
(* -------------------------------------------------------------------------- *)
@@ -186,7 +200,7 @@ struct
let category = Record.option jlog ~name:"category"
~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring)
let source = Record.option jlog ~name:"source"
- ~descr:(Md.plain "Source file position") (module LogSource)
+ ~descr:(Md.plain "Source file position") (module Kernel_ast.Position)
let data = Record.publish ~package ~name:"log"
~descr:(Md.plain "Message event record.") jlog
diff --git a/src/plugins/server/kernel_main.mli b/src/plugins/server/kernel_main.mli
index ead76ffab68c5141d8c8c01a9db4bceb9d09a883..b8dd233dda0114f5408609e620b4c97c80429cc5 100644
--- a/src/plugins/server/kernel_main.mli
+++ b/src/plugins/server/kernel_main.mli
@@ -24,7 +24,6 @@
(** Kernel Services *)
(* -------------------------------------------------------------------------- *)
-module LogSource : Data.S with type t = Filepath.position
module LogEvent : Data.S with type t = Log.event
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 534bee463c92d8665d56f5b438d6ca7a5851f08f..4e91e13653b2d5171d6fa710f32f87523dccea77 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -24,7 +24,6 @@ module Md = Markdown
module Pkg = Package
open Data
-open Kernel_main
open Kernel_ast
let package = Pkg.package ~title:"Property Services" ~name:"properties" ()
@@ -297,7 +296,7 @@ let () = States.column model ~name:"kinstr"
let () = States.column model ~name:"source"
~descr:(Md.plain "Position")
- ~data:(module LogSource)
+ ~data:(module Kernel_ast.Position)
~get:(fun ip -> Property.location ip |> fst)
let () = States.column model ~name:"alarm"